sbv 7.2 → 7.3
raw patch · 18 files changed
+1667/−58 lines, 18 files
Files
- CHANGES.md +9/−2
- Data/SBV/Control/Utils.hs +9/−4
- Data/SBV/Core/Symbolic.hs +17/−23
- Data/SBV/SMT/SMTLib2.hs +26/−13
- Data/SBV/SMT/Utils.hs +7/−5
- SBVTestSuite/GoldFiles/queryArrays1.gold +43/−0
- SBVTestSuite/GoldFiles/queryArrays2.gold +546/−0
- SBVTestSuite/GoldFiles/queryArrays3.gold +291/−0
- SBVTestSuite/GoldFiles/queryArrays4.gold +557/−0
- SBVTestSuite/GoldFiles/queryArrays5.gold +41/−0
- SBVTestSuite/GoldFiles/query_badOption.gold +0/−1
- SBVTestSuite/SBVDocTest.hs +7/−5
- SBVTestSuite/SBVHLint.hs +5/−2
- SBVTestSuite/SBVTest.hs +2/−0
- SBVTestSuite/TestSuite/Arrays/Query.hs +103/−0
- SBVTestSuite/TestSuite/Queries/BadOption.hs +1/−1
- SBVTestSuite/Utils/SBVTestFramework.hs +1/−1
- sbv.cabal +2/−1
CHANGES.md view
@@ -1,8 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.2, 2017-08-29+* Latest Hackage released version: 7.3, 2017-09-06 +### Version 7.3, 2017-09-06++ * Query mode: Add support for arrays in query mode. Thanks to Brad Hardy for+ providing the use-case and debugging help.++ * Query mode: Add support for tables. (As used by 'select' calls.)+ ### Version 7.2, 2017-08-29 * Reworked implementation of shifts and rotates: When a signed quantity was@@ -40,7 +47,7 @@ * Fix a bug in the implementation of `svSetBit`. Thanks to Robert Dockins for the report. -### Version 7.0, Released 2017-07-19+### Version 7.0, 2017-07-19 * NB. SBV now requires GHC >= 8.0.1 to compile. If you are stuck with an older version of GHC, please get in contact.
Data/SBV/Control/Utils.hs view
@@ -40,7 +40,8 @@ import Data.Int import Data.Word -import qualified Data.Map as Map+import qualified Data.Map as Map+import qualified Data.IntMap as IMap import Control.Monad (unless) import Control.Monad.State.Lazy (get, liftIO)@@ -121,14 +122,18 @@ syncUpSolver :: IncState -> Query () syncUpSolver is = do cfg <- getConfig- ls <- io $ do let swapc ((_, a), b) = (b, a)+ ls <- io $ do let swap (a, b) = (b, a)+ swapc ((_, a), b) = (b, a) cmp (a, _) (b, _) = a `compare` b+ arrange (i, (at, rt, es)) = ((i, at, rt), es) inps <- reverse <$> readIORef (rNewInps is) ks <- readIORef (rNewKinds is) cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rNewConsts is)+ arrs <- IMap.toAscList <$> readIORef (rNewArrs is)+ tbls <- (map arrange . sortBy cmp . map swap . Map.toList) <$> readIORef (rNewTbls is) as <- readIORef (rNewAsgns is)- return $ toIncSMTLib cfg inps ks cnsts as cfg- mapM_ (send True) (mergeSExpr ls)+ return $ toIncSMTLib cfg inps ks cnsts arrs tbls as cfg+ mapM_ (send True) $ mergeSExpr ls -- | Retrieve the query context getQueryState :: Query QueryState
Data/SBV/Core/Symbolic.hs view
@@ -512,6 +512,8 @@ data IncState = IncState { rNewInps :: IORef [NamedSymVar] -- always existential! , rNewKinds :: IORef KindSet , rNewConsts :: IORef CnstMap+ , rNewArrs :: IORef ArrayMap+ , rNewTbls :: IORef TableMap , rNewAsgns :: IORef SBVPgm } @@ -521,10 +523,14 @@ is <- newIORef [] ks <- newIORef Set.empty nc <- newIORef Map.empty+ am <- newIORef IMap.empty+ tm <- newIORef Map.empty pgm <- newIORef (SBVPgm S.empty) return IncState { rNewInps = is , rNewKinds = ks , rNewConsts = nc+ , rNewArrs = am+ , rNewTbls = tm , rNewAsgns = pgm } @@ -757,13 +763,9 @@ tblMap <- readIORef (rtblMap st) case key `Map.lookup` tblMap of Just i -> return i- _ -> do let i = Map.size tblMap- modifyState st rtblMap (Map.insert key i)- $ noInteractive [ "Creation of a new table:"- , " Index kind: " ++ show at- , " Value kind: " ++ show rt- , " Elements : " ++ unwords (map show elts)- ]+ _ -> do let i = Map.size tblMap+ upd = Map.insert key i+ modifyState st rtblMap upd $ modifyIncState st rNewTbls upd return i -- | Create a new expression; hash-cons as necessary@@ -1066,11 +1068,9 @@ addr <- svToSW st a val <- svToSW st b amap <- readIORef (rArrayMap st)- let j = IMap.size amap- j `seq` modifyState st rArrayMap (IMap.insert j ("array_" ++ show j, ainfo, ArrayMutate arr addr val))- (noInteractive [ "An array update:"- , " Array info: " ++ show ainfo- ])+ let j = IMap.size amap+ upd = IMap.insert j ("array_" ++ show j, ainfo, ArrayMutate arr addr val)+ j `seq` modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd return j -- | Merge two given arrays on the symbolic condition@@ -1082,11 +1082,9 @@ bi <- uncacheAI b st ts <- svToSW st t amap <- readIORef (rArrayMap st)- let k = IMap.size amap- k `seq` modifyState st rArrayMap (IMap.insert k ("array_" ++ show k, ainfo, ArrayMerge ts ai bi))- (noInteractive [ "An array merge:"- , " Array info: " ++ show ainfo- ])+ let k = IMap.size amap+ upd = IMap.insert k ("array_" ++ show k, ainfo, ArrayMerge ts ai bi)+ k `seq` modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd return k -- | Create a named new array, with an optional initial value@@ -1096,12 +1094,8 @@ amap <- liftIO $ readIORef $ rArrayMap st let i = IMap.size amap nm = mkNm i- actx <- liftIO $ return ArrayFree- liftIO $ modifyState st rArrayMap (IMap.insert i (nm, ainfo, actx))- $ noInteractive [ "A new array creation:"- , " Array info: " ++ show ainfo- , " Named : " ++ show nm- ]+ upd = IMap.insert i (nm, ainfo, ArrayFree)+ liftIO $ modifyState st rArrayMap upd $ modifyIncState st rNewArrs upd return $ SArr ainfo $ cache $ const $ return i -- | Compare two arrays for equality
Data/SBV/SMT/SMTLib2.hs view
@@ -239,26 +239,39 @@ body [_] i = show i body (c:cs) i = "(ite (= x " ++ c ++ ") " ++ show i ++ " " ++ body cs (i+1) ++ ")" --- | Things we do not support in interactive mode, at least for now!-noInteractive :: [String] -> a-noInteractive ss = error $ unlines $ ""- : "*** Data.SBV: Unsupported interactive/query mode feature."- : map ("*** " ++) ss- ++ ["*** Data.SBV: Please report this as a feature request!"]- -- | Convert in a query context cvtInc :: SMTLibIncConverter [String]-cvtInc inps ks consts (SBVPgm asgnsSeq) cfg = concatMap declSort [(s, dt) | KUserSort s dt <- Set.toList ks]- ++ map (declConst cfg) consts- ++ map declInp inps- ++ map (declDef cfg skolemMap tableMap) (F.toList asgnsSeq)+cvtInc inps ks consts arrs tbls (SBVPgm asgnsSeq) cfg =+ -- sorts+ concatMap declSort [(s, dt) | KUserSort s dt <- Set.toList ks]+ -- constants+ ++ map (declConst cfg) consts+ -- inputs+ ++ map declInp inps+ -- arrays+ ++ concat arrayConstants+ -- tables+ ++ concatMap constTable allTables+ -- expressions+ ++ map (declDef cfg skolemMap tableMap) (F.toList asgnsSeq)+ -- delayed equalities+ ++ concatMap asrt arrayDelayeds where -- NB. The below setting of skolemMap to empty is OK, since we do -- not support queries in the context of skolemized variables skolemMap = M.empty- tableMap = noInteractive ["Programs with constant tabled data"] + rm = roundingMode cfg+ declInp (s, _) = "(declare-fun " ++ show s ++ " () " ++ swType s ++ ")" + (arrayConstants, arrayDelayeds) = unzip $ map (declArray False (map fst consts) skolemMap) arrs++ allTables = [(t, either id id (genTableData rm skolemMap (False, []) (map fst consts) t)) | t <- tbls]+ tableMap = IM.fromList $ map mkTable allTables+ where mkTable (((t, _, _), _), _) = (t, "table" ++ show t)++ asrt = map (\s -> "(assert " ++ s ++ ")")+ declDef :: SMTConfig -> SkolemMap -> TableMap -> (SW, SBVExpr) -> String declDef cfg skolemMap tableMap (s, expr) = case expr of@@ -369,7 +382,7 @@ getTable :: TableMap -> Int -> String getTable m i | Just tn <- i `IM.lookup` m = tn- | True = error $ "SBV.SMTLib2: Cannot locate table " ++ show i+ | True = "table" ++ show i -- constant tables are always named this way cvtExp :: SolverCapabilities -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String cvtExp caps rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr
Data/SBV/SMT/Utils.hs view
@@ -44,11 +44,13 @@ -> a -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)-type SMTLibIncConverter a = [NamedSymVar] -- ^ inputs- -> Set.Set Kind -- ^ Newly registered kinds- -> [(SW, CW)] -- ^ constants- -> SBVPgm -- ^ assignments- -> SMTConfig -- ^ configuration+type SMTLibIncConverter a = [NamedSymVar] -- ^ inputs+ -> Set.Set Kind -- ^ Newly registered kinds+ -> [(SW, CW)] -- ^ constants+ -> [(Int, ArrayInfo)] -- ^ newly created arrays+ -> [((Int, Kind, Kind), [SW])] -- ^ newly created tables+ -> SBVPgm -- ^ assignments+ -> SMTConfig -- ^ configuration -> a -- | Create an annotated term with the given name
+ SBVTestSuite/GoldFiles/queryArrays1.gold view
@@ -0,0 +1,43 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_ABV)+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a1"+[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "a2"+[GOOD] (declare-fun s3 () (_ BitVec 8)) ; tracks user variable "v1"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] (declare-fun array_0 () (Array (_ BitVec 8) (_ BitVec 8)))+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (distinct s0 s1))+[GOOD] (assert s2)+[GOOD] (declare-fun array_1 () (Array (_ BitVec 8) (_ BitVec 8)))+[GOOD] (define-fun s4 () (_ BitVec 8) (select array_1 s0))+[GOOD] (define-fun s5 () Bool (= s3 s4))+[GOOD] (assert (= array_1 (store array_0 s0 s3)))+[GOOD] (assert s5)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #x00))+[SEND] (get-value (s1))+[RECV] ((s1 #xff))+[SEND] (get-value (s3))+[RECV] ((s3 #x00))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:(0,255,0)+DONE!
+ SBVTestSuite/GoldFiles/queryArrays2.gold view
@@ -0,0 +1,546 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_UFBV) ; NB. User specified.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "i"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (assert s_1)+[GOOD] (define-fun s1 () (_ BitVec 8) #x00)+[GOOD] (define-fun s2 () (_ BitVec 8) #x01)+[GOOD] (define-fun s3 () (_ BitVec 8) #x02)+[GOOD] (define-fun s4 () (_ BitVec 8) #x03)+[GOOD] (define-fun s5 () (_ BitVec 8) #x04)+[GOOD] (define-fun s6 () (_ BitVec 8) #x05)+[GOOD] (define-fun s7 () (_ BitVec 8) #x06)+[GOOD] (define-fun s8 () (_ BitVec 8) #x07)+[GOOD] (define-fun s9 () (_ BitVec 8) #x08)+[GOOD] (define-fun s10 () (_ BitVec 8) #x09)+[GOOD] (define-fun s11 () (_ BitVec 8) #x0a)+[GOOD] (define-fun s12 () (_ BitVec 8) #x0b)+[GOOD] (define-fun s13 () (_ BitVec 8) #x0c)+[GOOD] (define-fun s14 () (_ BitVec 8) #x0d)+[GOOD] (define-fun s15 () (_ BitVec 8) #x0e)+[GOOD] (define-fun s16 () (_ BitVec 8) #x0f)+[GOOD] (define-fun s17 () (_ BitVec 8) #x10)+[GOOD] (define-fun s18 () (_ BitVec 8) #x11)+[GOOD] (define-fun s19 () (_ BitVec 8) #x12)+[GOOD] (define-fun s20 () (_ BitVec 8) #x13)+[GOOD] (define-fun s21 () (_ BitVec 8) #x14)+[GOOD] (define-fun s22 () (_ BitVec 8) #x15)+[GOOD] (define-fun s23 () (_ BitVec 8) #x16)+[GOOD] (define-fun s24 () (_ BitVec 8) #x17)+[GOOD] (define-fun s25 () (_ BitVec 8) #x18)+[GOOD] (define-fun s26 () (_ BitVec 8) #x19)+[GOOD] (define-fun s27 () (_ BitVec 8) #x1a)+[GOOD] (define-fun s28 () (_ BitVec 8) #x1b)+[GOOD] (define-fun s29 () (_ BitVec 8) #x1c)+[GOOD] (define-fun s30 () (_ BitVec 8) #x1d)+[GOOD] (define-fun s31 () (_ BitVec 8) #x1e)+[GOOD] (define-fun s32 () (_ BitVec 8) #x1f)+[GOOD] (define-fun s33 () (_ BitVec 8) #x20)+[GOOD] (define-fun s34 () (_ BitVec 8) #x21)+[GOOD] (define-fun s35 () (_ BitVec 8) #x22)+[GOOD] (define-fun s36 () (_ BitVec 8) #x23)+[GOOD] (define-fun s37 () (_ BitVec 8) #x24)+[GOOD] (define-fun s38 () (_ BitVec 8) #x25)+[GOOD] (define-fun s39 () (_ BitVec 8) #x26)+[GOOD] (define-fun s40 () (_ BitVec 8) #x27)+[GOOD] (define-fun s41 () (_ BitVec 8) #x28)+[GOOD] (define-fun s42 () (_ BitVec 8) #x29)+[GOOD] (define-fun s43 () (_ BitVec 8) #x2a)+[GOOD] (define-fun s44 () (_ BitVec 8) #x2b)+[GOOD] (define-fun s45 () (_ BitVec 8) #x2c)+[GOOD] (define-fun s46 () (_ BitVec 8) #x2d)+[GOOD] (define-fun s47 () (_ BitVec 8) #x2e)+[GOOD] (define-fun s48 () (_ BitVec 8) #x2f)+[GOOD] (define-fun s49 () (_ BitVec 8) #x30)+[GOOD] (define-fun s50 () (_ BitVec 8) #x31)+[GOOD] (define-fun s51 () (_ BitVec 8) #x32)+[GOOD] (define-fun s52 () (_ BitVec 8) #x33)+[GOOD] (define-fun s53 () (_ BitVec 8) #x34)+[GOOD] (define-fun s54 () (_ BitVec 8) #x35)+[GOOD] (define-fun s55 () (_ BitVec 8) #x36)+[GOOD] (define-fun s56 () (_ BitVec 8) #x37)+[GOOD] (define-fun s57 () (_ BitVec 8) #x38)+[GOOD] (define-fun s58 () (_ BitVec 8) #x39)+[GOOD] (define-fun s59 () (_ BitVec 8) #x3a)+[GOOD] (define-fun s60 () (_ BitVec 8) #x3b)+[GOOD] (define-fun s61 () (_ BitVec 8) #x3c)+[GOOD] (define-fun s62 () (_ BitVec 8) #x3d)+[GOOD] (define-fun s63 () (_ BitVec 8) #x3e)+[GOOD] (define-fun s64 () (_ BitVec 8) #x3f)+[GOOD] (define-fun s65 () (_ BitVec 8) #x40)+[GOOD] (define-fun s66 () (_ BitVec 8) #x41)+[GOOD] (define-fun s67 () (_ BitVec 8) #x42)+[GOOD] (define-fun s68 () (_ BitVec 8) #x43)+[GOOD] (define-fun s69 () (_ BitVec 8) #x44)+[GOOD] (define-fun s70 () (_ BitVec 8) #x45)+[GOOD] (define-fun s71 () (_ BitVec 8) #x46)+[GOOD] (define-fun s72 () (_ BitVec 8) #x47)+[GOOD] (define-fun s73 () (_ BitVec 8) #x48)+[GOOD] (define-fun s74 () (_ BitVec 8) #x49)+[GOOD] (define-fun s75 () (_ BitVec 8) #x4a)+[GOOD] (define-fun s76 () (_ BitVec 8) #x4b)+[GOOD] (define-fun s77 () (_ BitVec 8) #x4c)+[GOOD] (define-fun s78 () (_ BitVec 8) #x4d)+[GOOD] (define-fun s79 () (_ BitVec 8) #x4e)+[GOOD] (define-fun s80 () (_ BitVec 8) #x4f)+[GOOD] (define-fun s81 () (_ BitVec 8) #x50)+[GOOD] (define-fun s82 () (_ BitVec 8) #x51)+[GOOD] (define-fun s83 () (_ BitVec 8) #x52)+[GOOD] (define-fun s84 () (_ BitVec 8) #x53)+[GOOD] (define-fun s85 () (_ BitVec 8) #x54)+[GOOD] (define-fun s86 () (_ BitVec 8) #x55)+[GOOD] (define-fun s87 () (_ BitVec 8) #x56)+[GOOD] (define-fun s88 () (_ BitVec 8) #x57)+[GOOD] (define-fun s89 () (_ BitVec 8) #x58)+[GOOD] (define-fun s90 () (_ BitVec 8) #x59)+[GOOD] (define-fun s91 () (_ BitVec 8) #x5a)+[GOOD] (define-fun s92 () (_ BitVec 8) #x5b)+[GOOD] (define-fun s93 () (_ BitVec 8) #x5c)+[GOOD] (define-fun s94 () (_ BitVec 8) #x5d)+[GOOD] (define-fun s95 () (_ BitVec 8) #x5e)+[GOOD] (define-fun s96 () (_ BitVec 8) #x5f)+[GOOD] (define-fun s97 () (_ BitVec 8) #x60)+[GOOD] (define-fun s98 () (_ BitVec 8) #x61)+[GOOD] (define-fun s99 () (_ BitVec 8) #x62)+[GOOD] (define-fun s100 () (_ BitVec 8) #x63)+[GOOD] (define-fun s101 () (_ BitVec 8) #x64)+[GOOD] (define-fun s102 () (_ BitVec 8) #x65)+[GOOD] (define-fun s103 () (_ BitVec 8) #x66)+[GOOD] (define-fun s104 () (_ BitVec 8) #x67)+[GOOD] (define-fun s105 () (_ BitVec 8) #x68)+[GOOD] (define-fun s106 () (_ BitVec 8) #x69)+[GOOD] (define-fun s107 () (_ BitVec 8) #x6a)+[GOOD] (define-fun s108 () (_ BitVec 8) #x6b)+[GOOD] (define-fun s109 () (_ BitVec 8) #x6c)+[GOOD] (define-fun s110 () (_ BitVec 8) #x6d)+[GOOD] (define-fun s111 () (_ BitVec 8) #x6e)+[GOOD] (define-fun s112 () (_ BitVec 8) #x6f)+[GOOD] (define-fun s113 () (_ BitVec 8) #x70)+[GOOD] (define-fun s114 () (_ BitVec 8) #x71)+[GOOD] (define-fun s115 () (_ BitVec 8) #x72)+[GOOD] (define-fun s116 () (_ BitVec 8) #x73)+[GOOD] (define-fun s117 () (_ BitVec 8) #x74)+[GOOD] (define-fun s118 () (_ BitVec 8) #x75)+[GOOD] (define-fun s119 () (_ BitVec 8) #x76)+[GOOD] (define-fun s120 () (_ BitVec 8) #x77)+[GOOD] (define-fun s121 () (_ BitVec 8) #x78)+[GOOD] (define-fun s122 () (_ BitVec 8) #x79)+[GOOD] (define-fun s123 () (_ BitVec 8) #x7a)+[GOOD] (define-fun s124 () (_ BitVec 8) #x7b)+[GOOD] (define-fun s125 () (_ BitVec 8) #x7c)+[GOOD] (define-fun s126 () (_ BitVec 8) #x7d)+[GOOD] (define-fun s127 () (_ BitVec 8) #x7e)+[GOOD] (define-fun s128 () (_ BitVec 8) #x7f)+[GOOD] (define-fun s129 () (_ BitVec 8) #x80)+[GOOD] (define-fun s130 () (_ BitVec 8) #x81)+[GOOD] (define-fun s131 () (_ BitVec 8) #x82)+[GOOD] (define-fun s132 () (_ BitVec 8) #x83)+[GOOD] (define-fun s133 () (_ BitVec 8) #x84)+[GOOD] (define-fun s134 () (_ BitVec 8) #x85)+[GOOD] (define-fun s135 () (_ BitVec 8) #x86)+[GOOD] (define-fun s136 () (_ BitVec 8) #x87)+[GOOD] (define-fun s137 () (_ BitVec 8) #x88)+[GOOD] (define-fun s138 () (_ BitVec 8) #x89)+[GOOD] (define-fun s139 () (_ BitVec 8) #x8a)+[GOOD] (define-fun s140 () (_ BitVec 8) #x8b)+[GOOD] (define-fun s141 () (_ BitVec 8) #x8c)+[GOOD] (define-fun s142 () (_ BitVec 8) #x8d)+[GOOD] (define-fun s143 () (_ BitVec 8) #x8e)+[GOOD] (define-fun s144 () (_ BitVec 8) #x8f)+[GOOD] (define-fun s145 () (_ BitVec 8) #x90)+[GOOD] (define-fun s146 () (_ BitVec 8) #x91)+[GOOD] (define-fun s147 () (_ BitVec 8) #x92)+[GOOD] (define-fun s148 () (_ BitVec 8) #x93)+[GOOD] (define-fun s149 () (_ BitVec 8) #x94)+[GOOD] (define-fun s150 () (_ BitVec 8) #x95)+[GOOD] (define-fun s151 () (_ BitVec 8) #x96)+[GOOD] (define-fun s152 () (_ BitVec 8) #x97)+[GOOD] (define-fun s153 () (_ BitVec 8) #x98)+[GOOD] (define-fun s154 () (_ BitVec 8) #x99)+[GOOD] (define-fun s155 () (_ BitVec 8) #x9a)+[GOOD] (define-fun s156 () (_ BitVec 8) #x9b)+[GOOD] (define-fun s157 () (_ BitVec 8) #x9c)+[GOOD] (define-fun s158 () (_ BitVec 8) #x9d)+[GOOD] (define-fun s159 () (_ BitVec 8) #x9e)+[GOOD] (define-fun s160 () (_ BitVec 8) #x9f)+[GOOD] (define-fun s161 () (_ BitVec 8) #xa0)+[GOOD] (define-fun s162 () (_ BitVec 8) #xa1)+[GOOD] (define-fun s163 () (_ BitVec 8) #xa2)+[GOOD] (define-fun s164 () (_ BitVec 8) #xa3)+[GOOD] (define-fun s165 () (_ BitVec 8) #xa4)+[GOOD] (define-fun s166 () (_ BitVec 8) #xa5)+[GOOD] (define-fun s167 () (_ BitVec 8) #xa6)+[GOOD] (define-fun s168 () (_ BitVec 8) #xa7)+[GOOD] (define-fun s169 () (_ BitVec 8) #xa8)+[GOOD] (define-fun s170 () (_ BitVec 8) #xa9)+[GOOD] (define-fun s171 () (_ BitVec 8) #xaa)+[GOOD] (define-fun s172 () (_ BitVec 8) #xab)+[GOOD] (define-fun s173 () (_ BitVec 8) #xac)+[GOOD] (define-fun s174 () (_ BitVec 8) #xad)+[GOOD] (define-fun s175 () (_ BitVec 8) #xae)+[GOOD] (define-fun s176 () (_ BitVec 8) #xaf)+[GOOD] (define-fun s177 () (_ BitVec 8) #xb0)+[GOOD] (define-fun s178 () (_ BitVec 8) #xb1)+[GOOD] (define-fun s179 () (_ BitVec 8) #xb2)+[GOOD] (define-fun s180 () (_ BitVec 8) #xb3)+[GOOD] (define-fun s181 () (_ BitVec 8) #xb4)+[GOOD] (define-fun s182 () (_ BitVec 8) #xb5)+[GOOD] (define-fun s183 () (_ BitVec 8) #xb6)+[GOOD] (define-fun s184 () (_ BitVec 8) #xb7)+[GOOD] (define-fun s185 () (_ BitVec 8) #xb8)+[GOOD] (define-fun s186 () (_ BitVec 8) #xb9)+[GOOD] (define-fun s187 () (_ BitVec 8) #xba)+[GOOD] (define-fun s188 () (_ BitVec 8) #xbb)+[GOOD] (define-fun s189 () (_ BitVec 8) #xbc)+[GOOD] (define-fun s190 () (_ BitVec 8) #xbd)+[GOOD] (define-fun s191 () (_ BitVec 8) #xbe)+[GOOD] (define-fun s192 () (_ BitVec 8) #xbf)+[GOOD] (define-fun s193 () (_ BitVec 8) #xc0)+[GOOD] (define-fun s194 () (_ BitVec 8) #xc1)+[GOOD] (define-fun s195 () (_ BitVec 8) #xc2)+[GOOD] (define-fun s196 () (_ BitVec 8) #xc3)+[GOOD] (define-fun s197 () (_ BitVec 8) #xc4)+[GOOD] (define-fun s198 () (_ BitVec 8) #xc5)+[GOOD] (define-fun s199 () (_ BitVec 8) #xc6)+[GOOD] (define-fun s200 () (_ BitVec 8) #xc7)+[GOOD] (define-fun s201 () (_ BitVec 8) #xc8)+[GOOD] (define-fun s202 () (_ BitVec 8) #xc9)+[GOOD] (define-fun s203 () (_ BitVec 8) #xca)+[GOOD] (define-fun s204 () (_ BitVec 8) #xcb)+[GOOD] (define-fun s205 () (_ BitVec 8) #xcc)+[GOOD] (define-fun s206 () (_ BitVec 8) #xcd)+[GOOD] (define-fun s207 () (_ BitVec 8) #xce)+[GOOD] (define-fun s208 () (_ BitVec 8) #xcf)+[GOOD] (define-fun s209 () (_ BitVec 8) #xd0)+[GOOD] (define-fun s210 () (_ BitVec 8) #xd1)+[GOOD] (define-fun s211 () (_ BitVec 8) #xd2)+[GOOD] (define-fun s212 () (_ BitVec 8) #xd3)+[GOOD] (define-fun s213 () (_ BitVec 8) #xd4)+[GOOD] (define-fun s214 () (_ BitVec 8) #xd5)+[GOOD] (define-fun s215 () (_ BitVec 8) #xd6)+[GOOD] (define-fun s216 () (_ BitVec 8) #xd7)+[GOOD] (define-fun s217 () (_ BitVec 8) #xd8)+[GOOD] (define-fun s218 () (_ BitVec 8) #xd9)+[GOOD] (define-fun s219 () (_ BitVec 8) #xda)+[GOOD] (define-fun s220 () (_ BitVec 8) #xdb)+[GOOD] (define-fun s221 () (_ BitVec 8) #xdc)+[GOOD] (define-fun s222 () (_ BitVec 8) #xdd)+[GOOD] (define-fun s223 () (_ BitVec 8) #xde)+[GOOD] (define-fun s224 () (_ BitVec 8) #xdf)+[GOOD] (define-fun s225 () (_ BitVec 8) #xe0)+[GOOD] (define-fun s226 () (_ BitVec 8) #xe1)+[GOOD] (define-fun s227 () (_ BitVec 8) #xe2)+[GOOD] (define-fun s228 () (_ BitVec 8) #xe3)+[GOOD] (define-fun s229 () (_ BitVec 8) #xe4)+[GOOD] (define-fun s230 () (_ BitVec 8) #xe5)+[GOOD] (define-fun s231 () (_ BitVec 8) #xe6)+[GOOD] (define-fun s232 () (_ BitVec 8) #xe7)+[GOOD] (define-fun s233 () (_ BitVec 8) #xe8)+[GOOD] (define-fun s234 () (_ BitVec 8) #xe9)+[GOOD] (define-fun s235 () (_ BitVec 8) #xea)+[GOOD] (define-fun s236 () (_ BitVec 8) #xeb)+[GOOD] (define-fun s237 () (_ BitVec 8) #xec)+[GOOD] (define-fun s238 () (_ BitVec 8) #xed)+[GOOD] (define-fun s239 () (_ BitVec 8) #xee)+[GOOD] (define-fun s240 () (_ BitVec 8) #xef)+[GOOD] (define-fun s241 () (_ BitVec 8) #xf0)+[GOOD] (define-fun s242 () (_ BitVec 8) #xf1)+[GOOD] (define-fun s243 () (_ BitVec 8) #xf2)+[GOOD] (define-fun s244 () (_ BitVec 8) #xf3)+[GOOD] (define-fun s245 () (_ BitVec 8) #xf4)+[GOOD] (define-fun s246 () (_ BitVec 8) #xf5)+[GOOD] (define-fun s247 () (_ BitVec 8) #xf6)+[GOOD] (define-fun s248 () (_ BitVec 8) #xf7)+[GOOD] (define-fun s249 () (_ BitVec 8) #xf8)+[GOOD] (define-fun s250 () (_ BitVec 8) #xf9)+[GOOD] (define-fun s251 () (_ BitVec 8) #xfa)+[GOOD] (define-fun s252 () (_ BitVec 8) #xfb)+[GOOD] (define-fun s253 () (_ BitVec 8) #xfc)+[GOOD] (define-fun s254 () (_ BitVec 8) #xfd)+[GOOD] (define-fun s255 () (_ BitVec 8) #xfe)+[GOOD] (define-fun s256 () (_ BitVec 8) #xff)+[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))+[GOOD] (assert (= (table0 #x00) s1))+[GOOD] (assert (= (table0 #x01) s2))+[GOOD] (assert (= (table0 #x02) s3))+[GOOD] (assert (= (table0 #x03) s4))+[GOOD] (assert (= (table0 #x04) s5))+[GOOD] (assert (= (table0 #x05) s6))+[GOOD] (assert (= (table0 #x06) s7))+[GOOD] (assert (= (table0 #x07) s8))+[GOOD] (assert (= (table0 #x08) s9))+[GOOD] (assert (= (table0 #x09) s10))+[GOOD] (assert (= (table0 #x0a) s11))+[GOOD] (assert (= (table0 #x0b) s12))+[GOOD] (assert (= (table0 #x0c) s13))+[GOOD] (assert (= (table0 #x0d) s14))+[GOOD] (assert (= (table0 #x0e) s15))+[GOOD] (assert (= (table0 #x0f) s16))+[GOOD] (assert (= (table0 #x10) s17))+[GOOD] (assert (= (table0 #x11) s18))+[GOOD] (assert (= (table0 #x12) s19))+[GOOD] (assert (= (table0 #x13) s20))+[GOOD] (assert (= (table0 #x14) s21))+[GOOD] (assert (= (table0 #x15) s22))+[GOOD] (assert (= (table0 #x16) s23))+[GOOD] (assert (= (table0 #x17) s24))+[GOOD] (assert (= (table0 #x18) s25))+[GOOD] (assert (= (table0 #x19) s26))+[GOOD] (assert (= (table0 #x1a) s27))+[GOOD] (assert (= (table0 #x1b) s28))+[GOOD] (assert (= (table0 #x1c) s29))+[GOOD] (assert (= (table0 #x1d) s30))+[GOOD] (assert (= (table0 #x1e) s31))+[GOOD] (assert (= (table0 #x1f) s32))+[GOOD] (assert (= (table0 #x20) s33))+[GOOD] (assert (= (table0 #x21) s34))+[GOOD] (assert (= (table0 #x22) s35))+[GOOD] (assert (= (table0 #x23) s36))+[GOOD] (assert (= (table0 #x24) s37))+[GOOD] (assert (= (table0 #x25) s38))+[GOOD] (assert (= (table0 #x26) s39))+[GOOD] (assert (= (table0 #x27) s40))+[GOOD] (assert (= (table0 #x28) s41))+[GOOD] (assert (= (table0 #x29) s42))+[GOOD] (assert (= (table0 #x2a) s43))+[GOOD] (assert (= (table0 #x2b) s44))+[GOOD] (assert (= (table0 #x2c) s45))+[GOOD] (assert (= (table0 #x2d) s46))+[GOOD] (assert (= (table0 #x2e) s47))+[GOOD] (assert (= (table0 #x2f) s48))+[GOOD] (assert (= (table0 #x30) s49))+[GOOD] (assert (= (table0 #x31) s50))+[GOOD] (assert (= (table0 #x32) s51))+[GOOD] (assert (= (table0 #x33) s52))+[GOOD] (assert (= (table0 #x34) s53))+[GOOD] (assert (= (table0 #x35) s54))+[GOOD] (assert (= (table0 #x36) s55))+[GOOD] (assert (= (table0 #x37) s56))+[GOOD] (assert (= (table0 #x38) s57))+[GOOD] (assert (= (table0 #x39) s58))+[GOOD] (assert (= (table0 #x3a) s59))+[GOOD] (assert (= (table0 #x3b) s60))+[GOOD] (assert (= (table0 #x3c) s61))+[GOOD] (assert (= (table0 #x3d) s62))+[GOOD] (assert (= (table0 #x3e) s63))+[GOOD] (assert (= (table0 #x3f) s64))+[GOOD] (assert (= (table0 #x40) s65))+[GOOD] (assert (= (table0 #x41) s66))+[GOOD] (assert (= (table0 #x42) s67))+[GOOD] (assert (= (table0 #x43) s68))+[GOOD] (assert (= (table0 #x44) s69))+[GOOD] (assert (= (table0 #x45) s70))+[GOOD] (assert (= (table0 #x46) s71))+[GOOD] (assert (= (table0 #x47) s72))+[GOOD] (assert (= (table0 #x48) s73))+[GOOD] (assert (= (table0 #x49) s74))+[GOOD] (assert (= (table0 #x4a) s75))+[GOOD] (assert (= (table0 #x4b) s76))+[GOOD] (assert (= (table0 #x4c) s77))+[GOOD] (assert (= (table0 #x4d) s78))+[GOOD] (assert (= (table0 #x4e) s79))+[GOOD] (assert (= (table0 #x4f) s80))+[GOOD] (assert (= (table0 #x50) s81))+[GOOD] (assert (= (table0 #x51) s82))+[GOOD] (assert (= (table0 #x52) s83))+[GOOD] (assert (= (table0 #x53) s84))+[GOOD] (assert (= (table0 #x54) s85))+[GOOD] (assert (= (table0 #x55) s86))+[GOOD] (assert (= (table0 #x56) s87))+[GOOD] (assert (= (table0 #x57) s88))+[GOOD] (assert (= (table0 #x58) s89))+[GOOD] (assert (= (table0 #x59) s90))+[GOOD] (assert (= (table0 #x5a) s91))+[GOOD] (assert (= (table0 #x5b) s92))+[GOOD] (assert (= (table0 #x5c) s93))+[GOOD] (assert (= (table0 #x5d) s94))+[GOOD] (assert (= (table0 #x5e) s95))+[GOOD] (assert (= (table0 #x5f) s96))+[GOOD] (assert (= (table0 #x60) s97))+[GOOD] (assert (= (table0 #x61) s98))+[GOOD] (assert (= (table0 #x62) s99))+[GOOD] (assert (= (table0 #x63) s100))+[GOOD] (assert (= (table0 #x64) s101))+[GOOD] (assert (= (table0 #x65) s102))+[GOOD] (assert (= (table0 #x66) s103))+[GOOD] (assert (= (table0 #x67) s104))+[GOOD] (assert (= (table0 #x68) s105))+[GOOD] (assert (= (table0 #x69) s106))+[GOOD] (assert (= (table0 #x6a) s107))+[GOOD] (assert (= (table0 #x6b) s108))+[GOOD] (assert (= (table0 #x6c) s109))+[GOOD] (assert (= (table0 #x6d) s110))+[GOOD] (assert (= (table0 #x6e) s111))+[GOOD] (assert (= (table0 #x6f) s112))+[GOOD] (assert (= (table0 #x70) s113))+[GOOD] (assert (= (table0 #x71) s114))+[GOOD] (assert (= (table0 #x72) s115))+[GOOD] (assert (= (table0 #x73) s116))+[GOOD] (assert (= (table0 #x74) s117))+[GOOD] (assert (= (table0 #x75) s118))+[GOOD] (assert (= (table0 #x76) s119))+[GOOD] (assert (= (table0 #x77) s120))+[GOOD] (assert (= (table0 #x78) s121))+[GOOD] (assert (= (table0 #x79) s122))+[GOOD] (assert (= (table0 #x7a) s123))+[GOOD] (assert (= (table0 #x7b) s124))+[GOOD] (assert (= (table0 #x7c) s125))+[GOOD] (assert (= (table0 #x7d) s126))+[GOOD] (assert (= (table0 #x7e) s127))+[GOOD] (assert (= (table0 #x7f) s128))+[GOOD] (assert (= (table0 #x80) s129))+[GOOD] (assert (= (table0 #x81) s130))+[GOOD] (assert (= (table0 #x82) s131))+[GOOD] (assert (= (table0 #x83) s132))+[GOOD] (assert (= (table0 #x84) s133))+[GOOD] (assert (= (table0 #x85) s134))+[GOOD] (assert (= (table0 #x86) s135))+[GOOD] (assert (= (table0 #x87) s136))+[GOOD] (assert (= (table0 #x88) s137))+[GOOD] (assert (= (table0 #x89) s138))+[GOOD] (assert (= (table0 #x8a) s139))+[GOOD] (assert (= (table0 #x8b) s140))+[GOOD] (assert (= (table0 #x8c) s141))+[GOOD] (assert (= (table0 #x8d) s142))+[GOOD] (assert (= (table0 #x8e) s143))+[GOOD] (assert (= (table0 #x8f) s144))+[GOOD] (assert (= (table0 #x90) s145))+[GOOD] (assert (= (table0 #x91) s146))+[GOOD] (assert (= (table0 #x92) s147))+[GOOD] (assert (= (table0 #x93) s148))+[GOOD] (assert (= (table0 #x94) s149))+[GOOD] (assert (= (table0 #x95) s150))+[GOOD] (assert (= (table0 #x96) s151))+[GOOD] (assert (= (table0 #x97) s152))+[GOOD] (assert (= (table0 #x98) s153))+[GOOD] (assert (= (table0 #x99) s154))+[GOOD] (assert (= (table0 #x9a) s155))+[GOOD] (assert (= (table0 #x9b) s156))+[GOOD] (assert (= (table0 #x9c) s157))+[GOOD] (assert (= (table0 #x9d) s158))+[GOOD] (assert (= (table0 #x9e) s159))+[GOOD] (assert (= (table0 #x9f) s160))+[GOOD] (assert (= (table0 #xa0) s161))+[GOOD] (assert (= (table0 #xa1) s162))+[GOOD] (assert (= (table0 #xa2) s163))+[GOOD] (assert (= (table0 #xa3) s164))+[GOOD] (assert (= (table0 #xa4) s165))+[GOOD] (assert (= (table0 #xa5) s166))+[GOOD] (assert (= (table0 #xa6) s167))+[GOOD] (assert (= (table0 #xa7) s168))+[GOOD] (assert (= (table0 #xa8) s169))+[GOOD] (assert (= (table0 #xa9) s170))+[GOOD] (assert (= (table0 #xaa) s171))+[GOOD] (assert (= (table0 #xab) s172))+[GOOD] (assert (= (table0 #xac) s173))+[GOOD] (assert (= (table0 #xad) s174))+[GOOD] (assert (= (table0 #xae) s175))+[GOOD] (assert (= (table0 #xaf) s176))+[GOOD] (assert (= (table0 #xb0) s177))+[GOOD] (assert (= (table0 #xb1) s178))+[GOOD] (assert (= (table0 #xb2) s179))+[GOOD] (assert (= (table0 #xb3) s180))+[GOOD] (assert (= (table0 #xb4) s181))+[GOOD] (assert (= (table0 #xb5) s182))+[GOOD] (assert (= (table0 #xb6) s183))+[GOOD] (assert (= (table0 #xb7) s184))+[GOOD] (assert (= (table0 #xb8) s185))+[GOOD] (assert (= (table0 #xb9) s186))+[GOOD] (assert (= (table0 #xba) s187))+[GOOD] (assert (= (table0 #xbb) s188))+[GOOD] (assert (= (table0 #xbc) s189))+[GOOD] (assert (= (table0 #xbd) s190))+[GOOD] (assert (= (table0 #xbe) s191))+[GOOD] (assert (= (table0 #xbf) s192))+[GOOD] (assert (= (table0 #xc0) s193))+[GOOD] (assert (= (table0 #xc1) s194))+[GOOD] (assert (= (table0 #xc2) s195))+[GOOD] (assert (= (table0 #xc3) s196))+[GOOD] (assert (= (table0 #xc4) s197))+[GOOD] (assert (= (table0 #xc5) s198))+[GOOD] (assert (= (table0 #xc6) s199))+[GOOD] (assert (= (table0 #xc7) s200))+[GOOD] (assert (= (table0 #xc8) s201))+[GOOD] (assert (= (table0 #xc9) s202))+[GOOD] (assert (= (table0 #xca) s203))+[GOOD] (assert (= (table0 #xcb) s204))+[GOOD] (assert (= (table0 #xcc) s205))+[GOOD] (assert (= (table0 #xcd) s206))+[GOOD] (assert (= (table0 #xce) s207))+[GOOD] (assert (= (table0 #xcf) s208))+[GOOD] (assert (= (table0 #xd0) s209))+[GOOD] (assert (= (table0 #xd1) s210))+[GOOD] (assert (= (table0 #xd2) s211))+[GOOD] (assert (= (table0 #xd3) s212))+[GOOD] (assert (= (table0 #xd4) s213))+[GOOD] (assert (= (table0 #xd5) s214))+[GOOD] (assert (= (table0 #xd6) s215))+[GOOD] (assert (= (table0 #xd7) s216))+[GOOD] (assert (= (table0 #xd8) s217))+[GOOD] (assert (= (table0 #xd9) s218))+[GOOD] (assert (= (table0 #xda) s219))+[GOOD] (assert (= (table0 #xdb) s220))+[GOOD] (assert (= (table0 #xdc) s221))+[GOOD] (assert (= (table0 #xdd) s222))+[GOOD] (assert (= (table0 #xde) s223))+[GOOD] (assert (= (table0 #xdf) s224))+[GOOD] (assert (= (table0 #xe0) s225))+[GOOD] (assert (= (table0 #xe1) s226))+[GOOD] (assert (= (table0 #xe2) s227))+[GOOD] (assert (= (table0 #xe3) s228))+[GOOD] (assert (= (table0 #xe4) s229))+[GOOD] (assert (= (table0 #xe5) s230))+[GOOD] (assert (= (table0 #xe6) s231))+[GOOD] (assert (= (table0 #xe7) s232))+[GOOD] (assert (= (table0 #xe8) s233))+[GOOD] (assert (= (table0 #xe9) s234))+[GOOD] (assert (= (table0 #xea) s235))+[GOOD] (assert (= (table0 #xeb) s236))+[GOOD] (assert (= (table0 #xec) s237))+[GOOD] (assert (= (table0 #xed) s238))+[GOOD] (assert (= (table0 #xee) s239))+[GOOD] (assert (= (table0 #xef) s240))+[GOOD] (assert (= (table0 #xf0) s241))+[GOOD] (assert (= (table0 #xf1) s242))+[GOOD] (assert (= (table0 #xf2) s243))+[GOOD] (assert (= (table0 #xf3) s244))+[GOOD] (assert (= (table0 #xf4) s245))+[GOOD] (assert (= (table0 #xf5) s246))+[GOOD] (assert (= (table0 #xf6) s247))+[GOOD] (assert (= (table0 #xf7) s248))+[GOOD] (assert (= (table0 #xf8) s249))+[GOOD] (assert (= (table0 #xf9) s250))+[GOOD] (assert (= (table0 #xfa) s251))+[GOOD] (assert (= (table0 #xfb) s252))+[GOOD] (assert (= (table0 #xfc) s253))+[GOOD] (assert (= (table0 #xfd) s254))+[GOOD] (assert (= (table0 #xfe) s255))+[GOOD] (assert (= (table0 #xff) s256))+[GOOD] (define-fun s257 () (_ BitVec 8) (table0 s0))+[GOOD] (define-fun s258 () Bool (= s0 s257))+[GOOD] (assert s258)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #x00))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:0+DONE!
+ SBVTestSuite/GoldFiles/queryArrays3.gold view
@@ -0,0 +1,291 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_UFBV) ; NB. User specified.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "i"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (assert s_1)+[GOOD] (define-fun s1 () (_ BitVec 8) #x00)+[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))+[GOOD] (assert (= (table0 #x00) s0))+[GOOD] (assert (= (table0 #x01) s0))+[GOOD] (assert (= (table0 #x02) s0))+[GOOD] (assert (= (table0 #x03) s0))+[GOOD] (assert (= (table0 #x04) s0))+[GOOD] (assert (= (table0 #x05) s0))+[GOOD] (assert (= (table0 #x06) s0))+[GOOD] (assert (= (table0 #x07) s0))+[GOOD] (assert (= (table0 #x08) s0))+[GOOD] (assert (= (table0 #x09) s0))+[GOOD] (assert (= (table0 #x0a) s0))+[GOOD] (assert (= (table0 #x0b) s0))+[GOOD] (assert (= (table0 #x0c) s0))+[GOOD] (assert (= (table0 #x0d) s0))+[GOOD] (assert (= (table0 #x0e) s0))+[GOOD] (assert (= (table0 #x0f) s0))+[GOOD] (assert (= (table0 #x10) s0))+[GOOD] (assert (= (table0 #x11) s0))+[GOOD] (assert (= (table0 #x12) s0))+[GOOD] (assert (= (table0 #x13) s0))+[GOOD] (assert (= (table0 #x14) s0))+[GOOD] (assert (= (table0 #x15) s0))+[GOOD] (assert (= (table0 #x16) s0))+[GOOD] (assert (= (table0 #x17) s0))+[GOOD] (assert (= (table0 #x18) s0))+[GOOD] (assert (= (table0 #x19) s0))+[GOOD] (assert (= (table0 #x1a) s0))+[GOOD] (assert (= (table0 #x1b) s0))+[GOOD] (assert (= (table0 #x1c) s0))+[GOOD] (assert (= (table0 #x1d) s0))+[GOOD] (assert (= (table0 #x1e) s0))+[GOOD] (assert (= (table0 #x1f) s0))+[GOOD] (assert (= (table0 #x20) s0))+[GOOD] (assert (= (table0 #x21) s0))+[GOOD] (assert (= (table0 #x22) s0))+[GOOD] (assert (= (table0 #x23) s0))+[GOOD] (assert (= (table0 #x24) s0))+[GOOD] (assert (= (table0 #x25) s0))+[GOOD] (assert (= (table0 #x26) s0))+[GOOD] (assert (= (table0 #x27) s0))+[GOOD] (assert (= (table0 #x28) s0))+[GOOD] (assert (= (table0 #x29) s0))+[GOOD] (assert (= (table0 #x2a) s0))+[GOOD] (assert (= (table0 #x2b) s0))+[GOOD] (assert (= (table0 #x2c) s0))+[GOOD] (assert (= (table0 #x2d) s0))+[GOOD] (assert (= (table0 #x2e) s0))+[GOOD] (assert (= (table0 #x2f) s0))+[GOOD] (assert (= (table0 #x30) s0))+[GOOD] (assert (= (table0 #x31) s0))+[GOOD] (assert (= (table0 #x32) s0))+[GOOD] (assert (= (table0 #x33) s0))+[GOOD] (assert (= (table0 #x34) s0))+[GOOD] (assert (= (table0 #x35) s0))+[GOOD] (assert (= (table0 #x36) s0))+[GOOD] (assert (= (table0 #x37) s0))+[GOOD] (assert (= (table0 #x38) s0))+[GOOD] (assert (= (table0 #x39) s0))+[GOOD] (assert (= (table0 #x3a) s0))+[GOOD] (assert (= (table0 #x3b) s0))+[GOOD] (assert (= (table0 #x3c) s0))+[GOOD] (assert (= (table0 #x3d) s0))+[GOOD] (assert (= (table0 #x3e) s0))+[GOOD] (assert (= (table0 #x3f) s0))+[GOOD] (assert (= (table0 #x40) s0))+[GOOD] (assert (= (table0 #x41) s0))+[GOOD] (assert (= (table0 #x42) s0))+[GOOD] (assert (= (table0 #x43) s0))+[GOOD] (assert (= (table0 #x44) s0))+[GOOD] (assert (= (table0 #x45) s0))+[GOOD] (assert (= (table0 #x46) s0))+[GOOD] (assert (= (table0 #x47) s0))+[GOOD] (assert (= (table0 #x48) s0))+[GOOD] (assert (= (table0 #x49) s0))+[GOOD] (assert (= (table0 #x4a) s0))+[GOOD] (assert (= (table0 #x4b) s0))+[GOOD] (assert (= (table0 #x4c) s0))+[GOOD] (assert (= (table0 #x4d) s0))+[GOOD] (assert (= (table0 #x4e) s0))+[GOOD] (assert (= (table0 #x4f) s0))+[GOOD] (assert (= (table0 #x50) s0))+[GOOD] (assert (= (table0 #x51) s0))+[GOOD] (assert (= (table0 #x52) s0))+[GOOD] (assert (= (table0 #x53) s0))+[GOOD] (assert (= (table0 #x54) s0))+[GOOD] (assert (= (table0 #x55) s0))+[GOOD] (assert (= (table0 #x56) s0))+[GOOD] (assert (= (table0 #x57) s0))+[GOOD] (assert (= (table0 #x58) s0))+[GOOD] (assert (= (table0 #x59) s0))+[GOOD] (assert (= (table0 #x5a) s0))+[GOOD] (assert (= (table0 #x5b) s0))+[GOOD] (assert (= (table0 #x5c) s0))+[GOOD] (assert (= (table0 #x5d) s0))+[GOOD] (assert (= (table0 #x5e) s0))+[GOOD] (assert (= (table0 #x5f) s0))+[GOOD] (assert (= (table0 #x60) s0))+[GOOD] (assert (= (table0 #x61) s0))+[GOOD] (assert (= (table0 #x62) s0))+[GOOD] (assert (= (table0 #x63) s0))+[GOOD] (assert (= (table0 #x64) s0))+[GOOD] (assert (= (table0 #x65) s0))+[GOOD] (assert (= (table0 #x66) s0))+[GOOD] (assert (= (table0 #x67) s0))+[GOOD] (assert (= (table0 #x68) s0))+[GOOD] (assert (= (table0 #x69) s0))+[GOOD] (assert (= (table0 #x6a) s0))+[GOOD] (assert (= (table0 #x6b) s0))+[GOOD] (assert (= (table0 #x6c) s0))+[GOOD] (assert (= (table0 #x6d) s0))+[GOOD] (assert (= (table0 #x6e) s0))+[GOOD] (assert (= (table0 #x6f) s0))+[GOOD] (assert (= (table0 #x70) s0))+[GOOD] (assert (= (table0 #x71) s0))+[GOOD] (assert (= (table0 #x72) s0))+[GOOD] (assert (= (table0 #x73) s0))+[GOOD] (assert (= (table0 #x74) s0))+[GOOD] (assert (= (table0 #x75) s0))+[GOOD] (assert (= (table0 #x76) s0))+[GOOD] (assert (= (table0 #x77) s0))+[GOOD] (assert (= (table0 #x78) s0))+[GOOD] (assert (= (table0 #x79) s0))+[GOOD] (assert (= (table0 #x7a) s0))+[GOOD] (assert (= (table0 #x7b) s0))+[GOOD] (assert (= (table0 #x7c) s0))+[GOOD] (assert (= (table0 #x7d) s0))+[GOOD] (assert (= (table0 #x7e) s0))+[GOOD] (assert (= (table0 #x7f) s0))+[GOOD] (assert (= (table0 #x80) s0))+[GOOD] (assert (= (table0 #x81) s0))+[GOOD] (assert (= (table0 #x82) s0))+[GOOD] (assert (= (table0 #x83) s0))+[GOOD] (assert (= (table0 #x84) s0))+[GOOD] (assert (= (table0 #x85) s0))+[GOOD] (assert (= (table0 #x86) s0))+[GOOD] (assert (= (table0 #x87) s0))+[GOOD] (assert (= (table0 #x88) s0))+[GOOD] (assert (= (table0 #x89) s0))+[GOOD] (assert (= (table0 #x8a) s0))+[GOOD] (assert (= (table0 #x8b) s0))+[GOOD] (assert (= (table0 #x8c) s0))+[GOOD] (assert (= (table0 #x8d) s0))+[GOOD] (assert (= (table0 #x8e) s0))+[GOOD] (assert (= (table0 #x8f) s0))+[GOOD] (assert (= (table0 #x90) s0))+[GOOD] (assert (= (table0 #x91) s0))+[GOOD] (assert (= (table0 #x92) s0))+[GOOD] (assert (= (table0 #x93) s0))+[GOOD] (assert (= (table0 #x94) s0))+[GOOD] (assert (= (table0 #x95) s0))+[GOOD] (assert (= (table0 #x96) s0))+[GOOD] (assert (= (table0 #x97) s0))+[GOOD] (assert (= (table0 #x98) s0))+[GOOD] (assert (= (table0 #x99) s0))+[GOOD] (assert (= (table0 #x9a) s0))+[GOOD] (assert (= (table0 #x9b) s0))+[GOOD] (assert (= (table0 #x9c) s0))+[GOOD] (assert (= (table0 #x9d) s0))+[GOOD] (assert (= (table0 #x9e) s0))+[GOOD] (assert (= (table0 #x9f) s0))+[GOOD] (assert (= (table0 #xa0) s0))+[GOOD] (assert (= (table0 #xa1) s0))+[GOOD] (assert (= (table0 #xa2) s0))+[GOOD] (assert (= (table0 #xa3) s0))+[GOOD] (assert (= (table0 #xa4) s0))+[GOOD] (assert (= (table0 #xa5) s0))+[GOOD] (assert (= (table0 #xa6) s0))+[GOOD] (assert (= (table0 #xa7) s0))+[GOOD] (assert (= (table0 #xa8) s0))+[GOOD] (assert (= (table0 #xa9) s0))+[GOOD] (assert (= (table0 #xaa) s0))+[GOOD] (assert (= (table0 #xab) s0))+[GOOD] (assert (= (table0 #xac) s0))+[GOOD] (assert (= (table0 #xad) s0))+[GOOD] (assert (= (table0 #xae) s0))+[GOOD] (assert (= (table0 #xaf) s0))+[GOOD] (assert (= (table0 #xb0) s0))+[GOOD] (assert (= (table0 #xb1) s0))+[GOOD] (assert (= (table0 #xb2) s0))+[GOOD] (assert (= (table0 #xb3) s0))+[GOOD] (assert (= (table0 #xb4) s0))+[GOOD] (assert (= (table0 #xb5) s0))+[GOOD] (assert (= (table0 #xb6) s0))+[GOOD] (assert (= (table0 #xb7) s0))+[GOOD] (assert (= (table0 #xb8) s0))+[GOOD] (assert (= (table0 #xb9) s0))+[GOOD] (assert (= (table0 #xba) s0))+[GOOD] (assert (= (table0 #xbb) s0))+[GOOD] (assert (= (table0 #xbc) s0))+[GOOD] (assert (= (table0 #xbd) s0))+[GOOD] (assert (= (table0 #xbe) s0))+[GOOD] (assert (= (table0 #xbf) s0))+[GOOD] (assert (= (table0 #xc0) s0))+[GOOD] (assert (= (table0 #xc1) s0))+[GOOD] (assert (= (table0 #xc2) s0))+[GOOD] (assert (= (table0 #xc3) s0))+[GOOD] (assert (= (table0 #xc4) s0))+[GOOD] (assert (= (table0 #xc5) s0))+[GOOD] (assert (= (table0 #xc6) s0))+[GOOD] (assert (= (table0 #xc7) s0))+[GOOD] (assert (= (table0 #xc8) s0))+[GOOD] (assert (= (table0 #xc9) s0))+[GOOD] (assert (= (table0 #xca) s0))+[GOOD] (assert (= (table0 #xcb) s0))+[GOOD] (assert (= (table0 #xcc) s0))+[GOOD] (assert (= (table0 #xcd) s0))+[GOOD] (assert (= (table0 #xce) s0))+[GOOD] (assert (= (table0 #xcf) s0))+[GOOD] (assert (= (table0 #xd0) s0))+[GOOD] (assert (= (table0 #xd1) s0))+[GOOD] (assert (= (table0 #xd2) s0))+[GOOD] (assert (= (table0 #xd3) s0))+[GOOD] (assert (= (table0 #xd4) s0))+[GOOD] (assert (= (table0 #xd5) s0))+[GOOD] (assert (= (table0 #xd6) s0))+[GOOD] (assert (= (table0 #xd7) s0))+[GOOD] (assert (= (table0 #xd8) s0))+[GOOD] (assert (= (table0 #xd9) s0))+[GOOD] (assert (= (table0 #xda) s0))+[GOOD] (assert (= (table0 #xdb) s0))+[GOOD] (assert (= (table0 #xdc) s0))+[GOOD] (assert (= (table0 #xdd) s0))+[GOOD] (assert (= (table0 #xde) s0))+[GOOD] (assert (= (table0 #xdf) s0))+[GOOD] (assert (= (table0 #xe0) s0))+[GOOD] (assert (= (table0 #xe1) s0))+[GOOD] (assert (= (table0 #xe2) s0))+[GOOD] (assert (= (table0 #xe3) s0))+[GOOD] (assert (= (table0 #xe4) s0))+[GOOD] (assert (= (table0 #xe5) s0))+[GOOD] (assert (= (table0 #xe6) s0))+[GOOD] (assert (= (table0 #xe7) s0))+[GOOD] (assert (= (table0 #xe8) s0))+[GOOD] (assert (= (table0 #xe9) s0))+[GOOD] (assert (= (table0 #xea) s0))+[GOOD] (assert (= (table0 #xeb) s0))+[GOOD] (assert (= (table0 #xec) s0))+[GOOD] (assert (= (table0 #xed) s0))+[GOOD] (assert (= (table0 #xee) s0))+[GOOD] (assert (= (table0 #xef) s0))+[GOOD] (assert (= (table0 #xf0) s0))+[GOOD] (assert (= (table0 #xf1) s0))+[GOOD] (assert (= (table0 #xf2) s0))+[GOOD] (assert (= (table0 #xf3) s0))+[GOOD] (assert (= (table0 #xf4) s0))+[GOOD] (assert (= (table0 #xf5) s0))+[GOOD] (assert (= (table0 #xf6) s0))+[GOOD] (assert (= (table0 #xf7) s0))+[GOOD] (assert (= (table0 #xf8) s0))+[GOOD] (assert (= (table0 #xf9) s0))+[GOOD] (assert (= (table0 #xfa) s0))+[GOOD] (assert (= (table0 #xfb) s0))+[GOOD] (assert (= (table0 #xfc) s0))+[GOOD] (assert (= (table0 #xfd) s0))+[GOOD] (assert (= (table0 #xfe) s0))+[GOOD] (assert (= (table0 #xff) s0))+[GOOD] (define-fun s2 () (_ BitVec 8) (table0 s0))+[GOOD] (define-fun s3 () Bool (= s0 s2))+[GOOD] (assert s3)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #x00))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:0+DONE!
+ SBVTestSuite/GoldFiles/queryArrays4.gold view
@@ -0,0 +1,557 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_UFBV) ; NB. User specified.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "i"+[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "j"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (assert s_1)+[GOOD] (define-fun s2 () (_ BitVec 8) #x00)+[GOOD] (define-fun s3 () (_ BitVec 8) #x01)+[GOOD] (define-fun s4 () (_ BitVec 8) #x02)+[GOOD] (define-fun s5 () (_ BitVec 8) #x03)+[GOOD] (define-fun s6 () (_ BitVec 8) #x04)+[GOOD] (define-fun s7 () (_ BitVec 8) #x05)+[GOOD] (define-fun s8 () (_ BitVec 8) #x06)+[GOOD] (define-fun s9 () (_ BitVec 8) #x07)+[GOOD] (define-fun s10 () (_ BitVec 8) #x08)+[GOOD] (define-fun s11 () (_ BitVec 8) #x09)+[GOOD] (define-fun s12 () (_ BitVec 8) #x0a)+[GOOD] (define-fun s13 () (_ BitVec 8) #x0b)+[GOOD] (define-fun s14 () (_ BitVec 8) #x0c)+[GOOD] (define-fun s15 () (_ BitVec 8) #x0d)+[GOOD] (define-fun s16 () (_ BitVec 8) #x0e)+[GOOD] (define-fun s17 () (_ BitVec 8) #x0f)+[GOOD] (define-fun s18 () (_ BitVec 8) #x10)+[GOOD] (define-fun s19 () (_ BitVec 8) #x11)+[GOOD] (define-fun s20 () (_ BitVec 8) #x12)+[GOOD] (define-fun s21 () (_ BitVec 8) #x13)+[GOOD] (define-fun s22 () (_ BitVec 8) #x14)+[GOOD] (define-fun s23 () (_ BitVec 8) #x15)+[GOOD] (define-fun s24 () (_ BitVec 8) #x16)+[GOOD] (define-fun s25 () (_ BitVec 8) #x17)+[GOOD] (define-fun s26 () (_ BitVec 8) #x18)+[GOOD] (define-fun s27 () (_ BitVec 8) #x19)+[GOOD] (define-fun s28 () (_ BitVec 8) #x1a)+[GOOD] (define-fun s29 () (_ BitVec 8) #x1b)+[GOOD] (define-fun s30 () (_ BitVec 8) #x1c)+[GOOD] (define-fun s31 () (_ BitVec 8) #x1d)+[GOOD] (define-fun s32 () (_ BitVec 8) #x1e)+[GOOD] (define-fun s33 () (_ BitVec 8) #x1f)+[GOOD] (define-fun s34 () (_ BitVec 8) #x20)+[GOOD] (define-fun s35 () (_ BitVec 8) #x21)+[GOOD] (define-fun s36 () (_ BitVec 8) #x22)+[GOOD] (define-fun s37 () (_ BitVec 8) #x23)+[GOOD] (define-fun s38 () (_ BitVec 8) #x24)+[GOOD] (define-fun s39 () (_ BitVec 8) #x25)+[GOOD] (define-fun s40 () (_ BitVec 8) #x26)+[GOOD] (define-fun s41 () (_ BitVec 8) #x27)+[GOOD] (define-fun s42 () (_ BitVec 8) #x28)+[GOOD] (define-fun s43 () (_ BitVec 8) #x29)+[GOOD] (define-fun s44 () (_ BitVec 8) #x2a)+[GOOD] (define-fun s45 () (_ BitVec 8) #x2b)+[GOOD] (define-fun s46 () (_ BitVec 8) #x2c)+[GOOD] (define-fun s47 () (_ BitVec 8) #x2d)+[GOOD] (define-fun s48 () (_ BitVec 8) #x2e)+[GOOD] (define-fun s49 () (_ BitVec 8) #x2f)+[GOOD] (define-fun s50 () (_ BitVec 8) #x30)+[GOOD] (define-fun s51 () (_ BitVec 8) #x31)+[GOOD] (define-fun s52 () (_ BitVec 8) #x32)+[GOOD] (define-fun s53 () (_ BitVec 8) #x33)+[GOOD] (define-fun s54 () (_ BitVec 8) #x34)+[GOOD] (define-fun s55 () (_ BitVec 8) #x35)+[GOOD] (define-fun s56 () (_ BitVec 8) #x36)+[GOOD] (define-fun s57 () (_ BitVec 8) #x37)+[GOOD] (define-fun s58 () (_ BitVec 8) #x38)+[GOOD] (define-fun s59 () (_ BitVec 8) #x39)+[GOOD] (define-fun s60 () (_ BitVec 8) #x3a)+[GOOD] (define-fun s61 () (_ BitVec 8) #x3b)+[GOOD] (define-fun s62 () (_ BitVec 8) #x3c)+[GOOD] (define-fun s63 () (_ BitVec 8) #x3d)+[GOOD] (define-fun s64 () (_ BitVec 8) #x3e)+[GOOD] (define-fun s65 () (_ BitVec 8) #x3f)+[GOOD] (define-fun s66 () (_ BitVec 8) #x40)+[GOOD] (define-fun s67 () (_ BitVec 8) #x41)+[GOOD] (define-fun s68 () (_ BitVec 8) #x42)+[GOOD] (define-fun s69 () (_ BitVec 8) #x43)+[GOOD] (define-fun s70 () (_ BitVec 8) #x44)+[GOOD] (define-fun s71 () (_ BitVec 8) #x45)+[GOOD] (define-fun s72 () (_ BitVec 8) #x46)+[GOOD] (define-fun s73 () (_ BitVec 8) #x47)+[GOOD] (define-fun s74 () (_ BitVec 8) #x48)+[GOOD] (define-fun s75 () (_ BitVec 8) #x49)+[GOOD] (define-fun s76 () (_ BitVec 8) #x4a)+[GOOD] (define-fun s77 () (_ BitVec 8) #x4b)+[GOOD] (define-fun s78 () (_ BitVec 8) #x4c)+[GOOD] (define-fun s79 () (_ BitVec 8) #x4d)+[GOOD] (define-fun s80 () (_ BitVec 8) #x4e)+[GOOD] (define-fun s81 () (_ BitVec 8) #x4f)+[GOOD] (define-fun s82 () (_ BitVec 8) #x50)+[GOOD] (define-fun s83 () (_ BitVec 8) #x51)+[GOOD] (define-fun s84 () (_ BitVec 8) #x52)+[GOOD] (define-fun s85 () (_ BitVec 8) #x53)+[GOOD] (define-fun s86 () (_ BitVec 8) #x54)+[GOOD] (define-fun s87 () (_ BitVec 8) #x55)+[GOOD] (define-fun s88 () (_ BitVec 8) #x56)+[GOOD] (define-fun s89 () (_ BitVec 8) #x57)+[GOOD] (define-fun s90 () (_ BitVec 8) #x58)+[GOOD] (define-fun s91 () (_ BitVec 8) #x59)+[GOOD] (define-fun s92 () (_ BitVec 8) #x5a)+[GOOD] (define-fun s93 () (_ BitVec 8) #x5b)+[GOOD] (define-fun s94 () (_ BitVec 8) #x5c)+[GOOD] (define-fun s95 () (_ BitVec 8) #x5d)+[GOOD] (define-fun s96 () (_ BitVec 8) #x5e)+[GOOD] (define-fun s97 () (_ BitVec 8) #x5f)+[GOOD] (define-fun s98 () (_ BitVec 8) #x60)+[GOOD] (define-fun s99 () (_ BitVec 8) #x61)+[GOOD] (define-fun s100 () (_ BitVec 8) #x62)+[GOOD] (define-fun s101 () (_ BitVec 8) #x63)+[GOOD] (define-fun s102 () (_ BitVec 8) #x64)+[GOOD] (define-fun s103 () (_ BitVec 8) #x65)+[GOOD] (define-fun s104 () (_ BitVec 8) #x66)+[GOOD] (define-fun s105 () (_ BitVec 8) #x67)+[GOOD] (define-fun s106 () (_ BitVec 8) #x68)+[GOOD] (define-fun s107 () (_ BitVec 8) #x69)+[GOOD] (define-fun s108 () (_ BitVec 8) #x6a)+[GOOD] (define-fun s109 () (_ BitVec 8) #x6b)+[GOOD] (define-fun s110 () (_ BitVec 8) #x6c)+[GOOD] (define-fun s111 () (_ BitVec 8) #x6d)+[GOOD] (define-fun s112 () (_ BitVec 8) #x6e)+[GOOD] (define-fun s113 () (_ BitVec 8) #x6f)+[GOOD] (define-fun s114 () (_ BitVec 8) #x70)+[GOOD] (define-fun s115 () (_ BitVec 8) #x71)+[GOOD] (define-fun s116 () (_ BitVec 8) #x72)+[GOOD] (define-fun s117 () (_ BitVec 8) #x73)+[GOOD] (define-fun s118 () (_ BitVec 8) #x74)+[GOOD] (define-fun s119 () (_ BitVec 8) #x75)+[GOOD] (define-fun s120 () (_ BitVec 8) #x76)+[GOOD] (define-fun s121 () (_ BitVec 8) #x77)+[GOOD] (define-fun s122 () (_ BitVec 8) #x78)+[GOOD] (define-fun s123 () (_ BitVec 8) #x79)+[GOOD] (define-fun s124 () (_ BitVec 8) #x7a)+[GOOD] (define-fun s125 () (_ BitVec 8) #x7b)+[GOOD] (define-fun s126 () (_ BitVec 8) #x7c)+[GOOD] (define-fun s127 () (_ BitVec 8) #x7d)+[GOOD] (define-fun s128 () (_ BitVec 8) #x7e)+[GOOD] (define-fun s129 () (_ BitVec 8) #x7f)+[GOOD] (define-fun s130 () (_ BitVec 8) #x80)+[GOOD] (define-fun s131 () (_ BitVec 8) #x81)+[GOOD] (define-fun s132 () (_ BitVec 8) #x82)+[GOOD] (define-fun s133 () (_ BitVec 8) #x83)+[GOOD] (define-fun s134 () (_ BitVec 8) #x84)+[GOOD] (define-fun s135 () (_ BitVec 8) #x85)+[GOOD] (define-fun s136 () (_ BitVec 8) #x86)+[GOOD] (define-fun s137 () (_ BitVec 8) #x87)+[GOOD] (define-fun s138 () (_ BitVec 8) #x88)+[GOOD] (define-fun s139 () (_ BitVec 8) #x89)+[GOOD] (define-fun s140 () (_ BitVec 8) #x8a)+[GOOD] (define-fun s141 () (_ BitVec 8) #x8b)+[GOOD] (define-fun s142 () (_ BitVec 8) #x8c)+[GOOD] (define-fun s143 () (_ BitVec 8) #x8d)+[GOOD] (define-fun s144 () (_ BitVec 8) #x8e)+[GOOD] (define-fun s145 () (_ BitVec 8) #x8f)+[GOOD] (define-fun s146 () (_ BitVec 8) #x90)+[GOOD] (define-fun s147 () (_ BitVec 8) #x91)+[GOOD] (define-fun s148 () (_ BitVec 8) #x92)+[GOOD] (define-fun s149 () (_ BitVec 8) #x93)+[GOOD] (define-fun s150 () (_ BitVec 8) #x94)+[GOOD] (define-fun s151 () (_ BitVec 8) #x95)+[GOOD] (define-fun s152 () (_ BitVec 8) #x96)+[GOOD] (define-fun s153 () (_ BitVec 8) #x97)+[GOOD] (define-fun s154 () (_ BitVec 8) #x98)+[GOOD] (define-fun s155 () (_ BitVec 8) #x99)+[GOOD] (define-fun s156 () (_ BitVec 8) #x9a)+[GOOD] (define-fun s157 () (_ BitVec 8) #x9b)+[GOOD] (define-fun s158 () (_ BitVec 8) #x9c)+[GOOD] (define-fun s159 () (_ BitVec 8) #x9d)+[GOOD] (define-fun s160 () (_ BitVec 8) #x9e)+[GOOD] (define-fun s161 () (_ BitVec 8) #x9f)+[GOOD] (define-fun s162 () (_ BitVec 8) #xa0)+[GOOD] (define-fun s163 () (_ BitVec 8) #xa1)+[GOOD] (define-fun s164 () (_ BitVec 8) #xa2)+[GOOD] (define-fun s165 () (_ BitVec 8) #xa3)+[GOOD] (define-fun s166 () (_ BitVec 8) #xa4)+[GOOD] (define-fun s167 () (_ BitVec 8) #xa5)+[GOOD] (define-fun s168 () (_ BitVec 8) #xa6)+[GOOD] (define-fun s169 () (_ BitVec 8) #xa7)+[GOOD] (define-fun s170 () (_ BitVec 8) #xa8)+[GOOD] (define-fun s171 () (_ BitVec 8) #xa9)+[GOOD] (define-fun s172 () (_ BitVec 8) #xaa)+[GOOD] (define-fun s173 () (_ BitVec 8) #xab)+[GOOD] (define-fun s174 () (_ BitVec 8) #xac)+[GOOD] (define-fun s175 () (_ BitVec 8) #xad)+[GOOD] (define-fun s176 () (_ BitVec 8) #xae)+[GOOD] (define-fun s177 () (_ BitVec 8) #xaf)+[GOOD] (define-fun s178 () (_ BitVec 8) #xb0)+[GOOD] (define-fun s179 () (_ BitVec 8) #xb1)+[GOOD] (define-fun s180 () (_ BitVec 8) #xb2)+[GOOD] (define-fun s181 () (_ BitVec 8) #xb3)+[GOOD] (define-fun s182 () (_ BitVec 8) #xb4)+[GOOD] (define-fun s183 () (_ BitVec 8) #xb5)+[GOOD] (define-fun s184 () (_ BitVec 8) #xb6)+[GOOD] (define-fun s185 () (_ BitVec 8) #xb7)+[GOOD] (define-fun s186 () (_ BitVec 8) #xb8)+[GOOD] (define-fun s187 () (_ BitVec 8) #xb9)+[GOOD] (define-fun s188 () (_ BitVec 8) #xba)+[GOOD] (define-fun s189 () (_ BitVec 8) #xbb)+[GOOD] (define-fun s190 () (_ BitVec 8) #xbc)+[GOOD] (define-fun s191 () (_ BitVec 8) #xbd)+[GOOD] (define-fun s192 () (_ BitVec 8) #xbe)+[GOOD] (define-fun s193 () (_ BitVec 8) #xbf)+[GOOD] (define-fun s194 () (_ BitVec 8) #xc0)+[GOOD] (define-fun s195 () (_ BitVec 8) #xc1)+[GOOD] (define-fun s196 () (_ BitVec 8) #xc2)+[GOOD] (define-fun s197 () (_ BitVec 8) #xc3)+[GOOD] (define-fun s198 () (_ BitVec 8) #xc4)+[GOOD] (define-fun s199 () (_ BitVec 8) #xc5)+[GOOD] (define-fun s200 () (_ BitVec 8) #xc6)+[GOOD] (define-fun s201 () (_ BitVec 8) #xc7)+[GOOD] (define-fun s202 () (_ BitVec 8) #xc8)+[GOOD] (define-fun s203 () (_ BitVec 8) #xc9)+[GOOD] (define-fun s204 () (_ BitVec 8) #xca)+[GOOD] (define-fun s205 () (_ BitVec 8) #xcb)+[GOOD] (define-fun s206 () (_ BitVec 8) #xcc)+[GOOD] (define-fun s207 () (_ BitVec 8) #xcd)+[GOOD] (define-fun s208 () (_ BitVec 8) #xce)+[GOOD] (define-fun s209 () (_ BitVec 8) #xcf)+[GOOD] (define-fun s210 () (_ BitVec 8) #xd0)+[GOOD] (define-fun s211 () (_ BitVec 8) #xd1)+[GOOD] (define-fun s212 () (_ BitVec 8) #xd2)+[GOOD] (define-fun s213 () (_ BitVec 8) #xd3)+[GOOD] (define-fun s214 () (_ BitVec 8) #xd4)+[GOOD] (define-fun s215 () (_ BitVec 8) #xd5)+[GOOD] (define-fun s216 () (_ BitVec 8) #xd6)+[GOOD] (define-fun s217 () (_ BitVec 8) #xd7)+[GOOD] (define-fun s218 () (_ BitVec 8) #xd8)+[GOOD] (define-fun s219 () (_ BitVec 8) #xd9)+[GOOD] (define-fun s220 () (_ BitVec 8) #xda)+[GOOD] (define-fun s221 () (_ BitVec 8) #xdb)+[GOOD] (define-fun s222 () (_ BitVec 8) #xdc)+[GOOD] (define-fun s223 () (_ BitVec 8) #xdd)+[GOOD] (define-fun s224 () (_ BitVec 8) #xde)+[GOOD] (define-fun s225 () (_ BitVec 8) #xdf)+[GOOD] (define-fun s226 () (_ BitVec 8) #xe0)+[GOOD] (define-fun s227 () (_ BitVec 8) #xe1)+[GOOD] (define-fun s228 () (_ BitVec 8) #xe2)+[GOOD] (define-fun s229 () (_ BitVec 8) #xe3)+[GOOD] (define-fun s230 () (_ BitVec 8) #xe4)+[GOOD] (define-fun s231 () (_ BitVec 8) #xe5)+[GOOD] (define-fun s232 () (_ BitVec 8) #xe6)+[GOOD] (define-fun s233 () (_ BitVec 8) #xe7)+[GOOD] (define-fun s234 () (_ BitVec 8) #xe8)+[GOOD] (define-fun s235 () (_ BitVec 8) #xe9)+[GOOD] (define-fun s236 () (_ BitVec 8) #xea)+[GOOD] (define-fun s237 () (_ BitVec 8) #xeb)+[GOOD] (define-fun s238 () (_ BitVec 8) #xec)+[GOOD] (define-fun s239 () (_ BitVec 8) #xed)+[GOOD] (define-fun s240 () (_ BitVec 8) #xee)+[GOOD] (define-fun s241 () (_ BitVec 8) #xef)+[GOOD] (define-fun s242 () (_ BitVec 8) #xf0)+[GOOD] (define-fun s243 () (_ BitVec 8) #xf1)+[GOOD] (define-fun s244 () (_ BitVec 8) #xf2)+[GOOD] (define-fun s245 () (_ BitVec 8) #xf3)+[GOOD] (define-fun s246 () (_ BitVec 8) #xf4)+[GOOD] (define-fun s247 () (_ BitVec 8) #xf5)+[GOOD] (define-fun s248 () (_ BitVec 8) #xf6)+[GOOD] (define-fun s249 () (_ BitVec 8) #xf7)+[GOOD] (define-fun s250 () (_ BitVec 8) #xf8)+[GOOD] (define-fun s251 () (_ BitVec 8) #xf9)+[GOOD] (define-fun s252 () (_ BitVec 8) #xfa)+[GOOD] (define-fun s253 () (_ BitVec 8) #xfb)+[GOOD] (define-fun s254 () (_ BitVec 8) #xfc)+[GOOD] (define-fun s255 () (_ BitVec 8) #xfd)+[GOOD] (define-fun s256 () (_ BitVec 8) #xfe)+[GOOD] (define-fun s257 () (_ BitVec 8) #xff)+[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))+[GOOD] (assert (= (table0 #x00) s2))+[GOOD] (assert (= (table0 #x01) s3))+[GOOD] (assert (= (table0 #x02) s4))+[GOOD] (assert (= (table0 #x03) s5))+[GOOD] (assert (= (table0 #x04) s6))+[GOOD] (assert (= (table0 #x05) s7))+[GOOD] (assert (= (table0 #x06) s8))+[GOOD] (assert (= (table0 #x07) s9))+[GOOD] (assert (= (table0 #x08) s10))+[GOOD] (assert (= (table0 #x09) s11))+[GOOD] (assert (= (table0 #x0a) s12))+[GOOD] (assert (= (table0 #x0b) s13))+[GOOD] (assert (= (table0 #x0c) s14))+[GOOD] (assert (= (table0 #x0d) s15))+[GOOD] (assert (= (table0 #x0e) s16))+[GOOD] (assert (= (table0 #x0f) s17))+[GOOD] (assert (= (table0 #x10) s18))+[GOOD] (assert (= (table0 #x11) s19))+[GOOD] (assert (= (table0 #x12) s20))+[GOOD] (assert (= (table0 #x13) s21))+[GOOD] (assert (= (table0 #x14) s22))+[GOOD] (assert (= (table0 #x15) s23))+[GOOD] (assert (= (table0 #x16) s24))+[GOOD] (assert (= (table0 #x17) s25))+[GOOD] (assert (= (table0 #x18) s26))+[GOOD] (assert (= (table0 #x19) s27))+[GOOD] (assert (= (table0 #x1a) s28))+[GOOD] (assert (= (table0 #x1b) s29))+[GOOD] (assert (= (table0 #x1c) s30))+[GOOD] (assert (= (table0 #x1d) s31))+[GOOD] (assert (= (table0 #x1e) s32))+[GOOD] (assert (= (table0 #x1f) s33))+[GOOD] (assert (= (table0 #x20) s34))+[GOOD] (assert (= (table0 #x21) s35))+[GOOD] (assert (= (table0 #x22) s36))+[GOOD] (assert (= (table0 #x23) s37))+[GOOD] (assert (= (table0 #x24) s38))+[GOOD] (assert (= (table0 #x25) s39))+[GOOD] (assert (= (table0 #x26) s40))+[GOOD] (assert (= (table0 #x27) s41))+[GOOD] (assert (= (table0 #x28) s42))+[GOOD] (assert (= (table0 #x29) s43))+[GOOD] (assert (= (table0 #x2a) s44))+[GOOD] (assert (= (table0 #x2b) s45))+[GOOD] (assert (= (table0 #x2c) s46))+[GOOD] (assert (= (table0 #x2d) s47))+[GOOD] (assert (= (table0 #x2e) s48))+[GOOD] (assert (= (table0 #x2f) s49))+[GOOD] (assert (= (table0 #x30) s50))+[GOOD] (assert (= (table0 #x31) s51))+[GOOD] (assert (= (table0 #x32) s52))+[GOOD] (assert (= (table0 #x33) s53))+[GOOD] (assert (= (table0 #x34) s54))+[GOOD] (assert (= (table0 #x35) s55))+[GOOD] (assert (= (table0 #x36) s56))+[GOOD] (assert (= (table0 #x37) s57))+[GOOD] (assert (= (table0 #x38) s58))+[GOOD] (assert (= (table0 #x39) s59))+[GOOD] (assert (= (table0 #x3a) s60))+[GOOD] (assert (= (table0 #x3b) s61))+[GOOD] (assert (= (table0 #x3c) s62))+[GOOD] (assert (= (table0 #x3d) s63))+[GOOD] (assert (= (table0 #x3e) s64))+[GOOD] (assert (= (table0 #x3f) s65))+[GOOD] (assert (= (table0 #x40) s66))+[GOOD] (assert (= (table0 #x41) s67))+[GOOD] (assert (= (table0 #x42) s68))+[GOOD] (assert (= (table0 #x43) s69))+[GOOD] (assert (= (table0 #x44) s70))+[GOOD] (assert (= (table0 #x45) s71))+[GOOD] (assert (= (table0 #x46) s72))+[GOOD] (assert (= (table0 #x47) s73))+[GOOD] (assert (= (table0 #x48) s74))+[GOOD] (assert (= (table0 #x49) s75))+[GOOD] (assert (= (table0 #x4a) s76))+[GOOD] (assert (= (table0 #x4b) s77))+[GOOD] (assert (= (table0 #x4c) s78))+[GOOD] (assert (= (table0 #x4d) s79))+[GOOD] (assert (= (table0 #x4e) s80))+[GOOD] (assert (= (table0 #x4f) s81))+[GOOD] (assert (= (table0 #x50) s82))+[GOOD] (assert (= (table0 #x51) s83))+[GOOD] (assert (= (table0 #x52) s84))+[GOOD] (assert (= (table0 #x53) s85))+[GOOD] (assert (= (table0 #x54) s86))+[GOOD] (assert (= (table0 #x55) s87))+[GOOD] (assert (= (table0 #x56) s88))+[GOOD] (assert (= (table0 #x57) s89))+[GOOD] (assert (= (table0 #x58) s90))+[GOOD] (assert (= (table0 #x59) s91))+[GOOD] (assert (= (table0 #x5a) s92))+[GOOD] (assert (= (table0 #x5b) s93))+[GOOD] (assert (= (table0 #x5c) s94))+[GOOD] (assert (= (table0 #x5d) s95))+[GOOD] (assert (= (table0 #x5e) s96))+[GOOD] (assert (= (table0 #x5f) s97))+[GOOD] (assert (= (table0 #x60) s98))+[GOOD] (assert (= (table0 #x61) s99))+[GOOD] (assert (= (table0 #x62) s100))+[GOOD] (assert (= (table0 #x63) s101))+[GOOD] (assert (= (table0 #x64) s102))+[GOOD] (assert (= (table0 #x65) s103))+[GOOD] (assert (= (table0 #x66) s104))+[GOOD] (assert (= (table0 #x67) s105))+[GOOD] (assert (= (table0 #x68) s106))+[GOOD] (assert (= (table0 #x69) s107))+[GOOD] (assert (= (table0 #x6a) s108))+[GOOD] (assert (= (table0 #x6b) s109))+[GOOD] (assert (= (table0 #x6c) s110))+[GOOD] (assert (= (table0 #x6d) s111))+[GOOD] (assert (= (table0 #x6e) s112))+[GOOD] (assert (= (table0 #x6f) s113))+[GOOD] (assert (= (table0 #x70) s114))+[GOOD] (assert (= (table0 #x71) s115))+[GOOD] (assert (= (table0 #x72) s116))+[GOOD] (assert (= (table0 #x73) s117))+[GOOD] (assert (= (table0 #x74) s118))+[GOOD] (assert (= (table0 #x75) s119))+[GOOD] (assert (= (table0 #x76) s120))+[GOOD] (assert (= (table0 #x77) s121))+[GOOD] (assert (= (table0 #x78) s122))+[GOOD] (assert (= (table0 #x79) s123))+[GOOD] (assert (= (table0 #x7a) s124))+[GOOD] (assert (= (table0 #x7b) s125))+[GOOD] (assert (= (table0 #x7c) s126))+[GOOD] (assert (= (table0 #x7d) s127))+[GOOD] (assert (= (table0 #x7e) s128))+[GOOD] (assert (= (table0 #x7f) s129))+[GOOD] (assert (= (table0 #x80) s130))+[GOOD] (assert (= (table0 #x81) s131))+[GOOD] (assert (= (table0 #x82) s132))+[GOOD] (assert (= (table0 #x83) s133))+[GOOD] (assert (= (table0 #x84) s134))+[GOOD] (assert (= (table0 #x85) s135))+[GOOD] (assert (= (table0 #x86) s136))+[GOOD] (assert (= (table0 #x87) s137))+[GOOD] (assert (= (table0 #x88) s138))+[GOOD] (assert (= (table0 #x89) s139))+[GOOD] (assert (= (table0 #x8a) s140))+[GOOD] (assert (= (table0 #x8b) s141))+[GOOD] (assert (= (table0 #x8c) s142))+[GOOD] (assert (= (table0 #x8d) s143))+[GOOD] (assert (= (table0 #x8e) s144))+[GOOD] (assert (= (table0 #x8f) s145))+[GOOD] (assert (= (table0 #x90) s146))+[GOOD] (assert (= (table0 #x91) s147))+[GOOD] (assert (= (table0 #x92) s148))+[GOOD] (assert (= (table0 #x93) s149))+[GOOD] (assert (= (table0 #x94) s150))+[GOOD] (assert (= (table0 #x95) s151))+[GOOD] (assert (= (table0 #x96) s152))+[GOOD] (assert (= (table0 #x97) s153))+[GOOD] (assert (= (table0 #x98) s154))+[GOOD] (assert (= (table0 #x99) s155))+[GOOD] (assert (= (table0 #x9a) s156))+[GOOD] (assert (= (table0 #x9b) s157))+[GOOD] (assert (= (table0 #x9c) s158))+[GOOD] (assert (= (table0 #x9d) s159))+[GOOD] (assert (= (table0 #x9e) s160))+[GOOD] (assert (= (table0 #x9f) s161))+[GOOD] (assert (= (table0 #xa0) s162))+[GOOD] (assert (= (table0 #xa1) s163))+[GOOD] (assert (= (table0 #xa2) s164))+[GOOD] (assert (= (table0 #xa3) s165))+[GOOD] (assert (= (table0 #xa4) s166))+[GOOD] (assert (= (table0 #xa5) s167))+[GOOD] (assert (= (table0 #xa6) s168))+[GOOD] (assert (= (table0 #xa7) s169))+[GOOD] (assert (= (table0 #xa8) s170))+[GOOD] (assert (= (table0 #xa9) s171))+[GOOD] (assert (= (table0 #xaa) s172))+[GOOD] (assert (= (table0 #xab) s173))+[GOOD] (assert (= (table0 #xac) s174))+[GOOD] (assert (= (table0 #xad) s175))+[GOOD] (assert (= (table0 #xae) s176))+[GOOD] (assert (= (table0 #xaf) s177))+[GOOD] (assert (= (table0 #xb0) s178))+[GOOD] (assert (= (table0 #xb1) s179))+[GOOD] (assert (= (table0 #xb2) s180))+[GOOD] (assert (= (table0 #xb3) s181))+[GOOD] (assert (= (table0 #xb4) s182))+[GOOD] (assert (= (table0 #xb5) s183))+[GOOD] (assert (= (table0 #xb6) s184))+[GOOD] (assert (= (table0 #xb7) s185))+[GOOD] (assert (= (table0 #xb8) s186))+[GOOD] (assert (= (table0 #xb9) s187))+[GOOD] (assert (= (table0 #xba) s188))+[GOOD] (assert (= (table0 #xbb) s189))+[GOOD] (assert (= (table0 #xbc) s190))+[GOOD] (assert (= (table0 #xbd) s191))+[GOOD] (assert (= (table0 #xbe) s192))+[GOOD] (assert (= (table0 #xbf) s193))+[GOOD] (assert (= (table0 #xc0) s194))+[GOOD] (assert (= (table0 #xc1) s195))+[GOOD] (assert (= (table0 #xc2) s196))+[GOOD] (assert (= (table0 #xc3) s197))+[GOOD] (assert (= (table0 #xc4) s198))+[GOOD] (assert (= (table0 #xc5) s199))+[GOOD] (assert (= (table0 #xc6) s200))+[GOOD] (assert (= (table0 #xc7) s201))+[GOOD] (assert (= (table0 #xc8) s202))+[GOOD] (assert (= (table0 #xc9) s203))+[GOOD] (assert (= (table0 #xca) s204))+[GOOD] (assert (= (table0 #xcb) s205))+[GOOD] (assert (= (table0 #xcc) s206))+[GOOD] (assert (= (table0 #xcd) s207))+[GOOD] (assert (= (table0 #xce) s208))+[GOOD] (assert (= (table0 #xcf) s209))+[GOOD] (assert (= (table0 #xd0) s210))+[GOOD] (assert (= (table0 #xd1) s211))+[GOOD] (assert (= (table0 #xd2) s212))+[GOOD] (assert (= (table0 #xd3) s213))+[GOOD] (assert (= (table0 #xd4) s214))+[GOOD] (assert (= (table0 #xd5) s215))+[GOOD] (assert (= (table0 #xd6) s216))+[GOOD] (assert (= (table0 #xd7) s217))+[GOOD] (assert (= (table0 #xd8) s218))+[GOOD] (assert (= (table0 #xd9) s219))+[GOOD] (assert (= (table0 #xda) s220))+[GOOD] (assert (= (table0 #xdb) s221))+[GOOD] (assert (= (table0 #xdc) s222))+[GOOD] (assert (= (table0 #xdd) s223))+[GOOD] (assert (= (table0 #xde) s224))+[GOOD] (assert (= (table0 #xdf) s225))+[GOOD] (assert (= (table0 #xe0) s226))+[GOOD] (assert (= (table0 #xe1) s227))+[GOOD] (assert (= (table0 #xe2) s228))+[GOOD] (assert (= (table0 #xe3) s229))+[GOOD] (assert (= (table0 #xe4) s230))+[GOOD] (assert (= (table0 #xe5) s231))+[GOOD] (assert (= (table0 #xe6) s232))+[GOOD] (assert (= (table0 #xe7) s233))+[GOOD] (assert (= (table0 #xe8) s234))+[GOOD] (assert (= (table0 #xe9) s235))+[GOOD] (assert (= (table0 #xea) s236))+[GOOD] (assert (= (table0 #xeb) s237))+[GOOD] (assert (= (table0 #xec) s238))+[GOOD] (assert (= (table0 #xed) s239))+[GOOD] (assert (= (table0 #xee) s240))+[GOOD] (assert (= (table0 #xef) s241))+[GOOD] (assert (= (table0 #xf0) s242))+[GOOD] (assert (= (table0 #xf1) s243))+[GOOD] (assert (= (table0 #xf2) s244))+[GOOD] (assert (= (table0 #xf3) s245))+[GOOD] (assert (= (table0 #xf4) s246))+[GOOD] (assert (= (table0 #xf5) s247))+[GOOD] (assert (= (table0 #xf6) s248))+[GOOD] (assert (= (table0 #xf7) s249))+[GOOD] (assert (= (table0 #xf8) s250))+[GOOD] (assert (= (table0 #xf9) s251))+[GOOD] (assert (= (table0 #xfa) s252))+[GOOD] (assert (= (table0 #xfb) s253))+[GOOD] (assert (= (table0 #xfc) s254))+[GOOD] (assert (= (table0 #xfd) s255))+[GOOD] (assert (= (table0 #xfe) s256))+[GOOD] (assert (= (table0 #xff) s257))+[GOOD] (define-fun s258 () (_ BitVec 8) (table0 s0))+[GOOD] (define-fun s259 () Bool (= s0 s258))+[GOOD] (assert s259)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #x00))+[GOOD] (define-fun s260 () (_ BitVec 8) (table0 s1))+[GOOD] (define-fun s261 () Bool (= s1 s260))+[GOOD] (assert s261)+[GOOD] (define-fun s262 () (_ BitVec 8) (bvadd s0 s3))+[GOOD] (define-fun s263 () Bool (= s1 s262))+[GOOD] (assert s263)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s1))+[RECV] ((s1 #x01))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:(0,1)+DONE!
+ SBVTestSuite/GoldFiles/queryArrays5.gold view
@@ -0,0 +1,41 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_ABV)+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "a"+[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "v"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] (declare-fun array_0 () (Array (_ BitVec 8) (_ BitVec 8)))+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (assert s_1)+[GOOD] (define-fun s4 () (_ BitVec 8) #x01)+[GOOD] (define-fun s2 () (_ BitVec 8) #x01)+[GOOD] (declare-fun array_1 () (Array (_ BitVec 8) (_ BitVec 8)))+[GOOD] (declare-fun array_2 () (Array (_ BitVec 8) (_ BitVec 8)))+[GOOD] (define-fun s3 () (_ BitVec 8) (bvadd s1 s2))+[GOOD] (define-fun s5 () (_ BitVec 8) (bvadd s0 s4))+[GOOD] (define-fun s6 () (_ BitVec 8) (select array_2 s5))+[GOOD] (define-fun s7 () Bool (distinct s3 s6))+[GOOD] (assert (= array_1 (store array_0 s0 s1)))+[GOOD] (assert (= array_2 (store array_1 s5 s3)))+[GOOD] (assert s7)+[SEND] (check-sat)+[RECV] unsat+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:Nothing+DONE!
SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -43,4 +43,3 @@ *** bug/feature request with the solver! CallStack (from HasCallStack):- error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.2-BmAQsjRcnLN24H2yOFpcOt:Data.SBV.SMT.SMT
SBVTestSuite/SBVDocTest.hs view
@@ -11,16 +11,18 @@ import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), CIOS(..)) main :: IO ()-main = do (testEnv, _) <- getTestEnvironment+main = do (testEnv, testPercentage) <- getTestEnvironment putStrLn $ "SBVDocTest: Test platform: " ++ show testEnv case testEnv of- TestEnvLocal -> runDocTest False- TestEnvCI CIWindows -> runDocTest True- TestEnvCI _ -> runDocTest False- TestEnvUnknown -> do putStrLn "Unknown test environment, skipping doctests"+ TestEnvLocal -> runDocTest False+ TestEnvCI env -> if testPercentage < 50+ then do putStrLn $ "Test percentage below tresheold, skipping doctest: " ++ show testPercentage exitSuccess+ else runDocTest (env == CIWindows)+ TestEnvUnknown -> do putStrLn "Unknown test environment, skipping doctests"+ exitSuccess where runDocTest windowsSkip = do allFiles <- glob "Data/SBV/**/*.hs" let testFiles | windowsSkip = filter (not . bad) allFiles
SBVTestSuite/SBVHLint.hs view
@@ -14,13 +14,16 @@ main :: IO () main = do- (testEnv, _) <- getTestEnvironment+ (testEnv, testPercentage) <- getTestEnvironment putStrLn $ "SBVHLint: Test platform: " ++ show testEnv case testEnv of TestEnvLocal -> runHLint- TestEnvCI{} -> runHLint+ TestEnvCI{} -> if testPercentage < 50+ then do putStrLn $ "Test percentage below tresheold, skipping hlint: " ++ show testPercentage+ exitSuccess+ else runHLint TestEnvUnknown -> do putStrLn "Unknown test environment, skipping hlint run" exitSuccess where runHLint = do hints <- hlint arguments
SBVTestSuite/SBVTest.hs view
@@ -8,6 +8,7 @@ import System.Exit (exitSuccess) import qualified TestSuite.Arrays.Memory+import qualified TestSuite.Arrays.Query import qualified TestSuite.Basics.AllSat import qualified TestSuite.Basics.ArithNoSolver import qualified TestSuite.Basics.ArithSolver@@ -125,6 +126,7 @@ otherTests :: TestTree otherTests = testGroup "SBVOtherTests" [ TestSuite.Arrays.Memory.tests+ , TestSuite.Arrays.Query.tests , TestSuite.Basics.AllSat.tests , TestSuite.Basics.ArithNoSolver.tests , TestSuite.Basics.BasicTests.tests
+ SBVTestSuite/TestSuite/Arrays/Query.hs view
@@ -0,0 +1,103 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Arrays.Query+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for query mode arrays+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++module TestSuite.Arrays.Query(tests) where++import Data.SBV.Control++import Utils.SBVTestFramework++-- Test suite+tests :: TestTree+tests =+ testGroup "Arrays.Query"+ [ goldenCapturedIO "queryArrays1" $ t q1+ , goldenCapturedIO "queryArrays2" $ t q2+ , goldenCapturedIO "queryArrays3" $ t q3+ , goldenCapturedIO "queryArrays4" $ t q4+ , goldenCapturedIO "queryArrays5" $ t q5+ ]+ where t tc goldFile = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc+ appendFile goldFile ("\n FINAL:" ++ show r ++ "\nDONE!\n")++q1 :: Symbolic (Word8, Word8, Int8)+q1 = do m :: SArray Word8 Int8 <- newArray "a"++ a1 <- sWord8 "a1"+ a2 <- sWord8 "a2"++ constrain $ a1 ./= a2++ v1 <- sInt8 "v1"++ query $ do constrain $ v1 .== readArray (writeArray m a1 v1) a1+ _ <- checkSat+ va1 <- getValue a1+ va2 <- getValue a2+ vv1 <- getValue v1+ return (va1, va2, vv1)++q2 :: Symbolic Word8+q2 = do i <- sWord8 "i"++ setLogic QF_UFBV++ query $ do constrain $ i .== select [0 .. 255] 0 i+ _ <- checkSat+ getValue i++q3 :: Symbolic Word8+q3 = do i <- sWord8 "i"++ setLogic QF_UFBV++ query $ do constrain $ i .== select (replicate 256 i) 0 i+ _ <- checkSat+ getValue i++q4 :: Symbolic (Word8, Word8)+q4 = do i <- sWord8 "i"+ j <- sWord8 "j"++ setLogic QF_UFBV++ query $ do constrain $ i .== select [0 .. 255] 0 i+ _ <- checkSat+ iv <- getValue i+ constrain $ j .== select [0 .. 255] 0 j+ constrain $ j .== i+1+ _ <- checkSat+ jv <- getValue j+ return (iv, jv)++q5 :: Symbolic (Maybe (Word8, Int8))+q5 = do m :: SArray Word8 Int8 <- newArray "a"++ a <- sWord8 "a"+ v <- sInt8 "v"++ query $ do let m2 = writeArray (writeArray m a v) (a+1) (v+1)+ vRead = readArray m2 (a+1)++ constrain $ v + 1 ./= vRead++ cs <- checkSat++ case cs of+ Unsat -> return Nothing+ Unk -> error "solver returned Unknown!"+ Sat -> do av <- getValue a+ vv <- getValue v+ return $ Just (av, vv)++{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
SBVTestSuite/TestSuite/Queries/BadOption.hs view
@@ -23,7 +23,7 @@ testGroup "Basics.QueryIndividual" [ goldenCapturedIO "query_badOption" $ \rf -> runSMTWith z3{verbose=True, redirectVerbose=Just rf} q `C.catch`- (\(e::C.SomeException) -> appendFile rf ("\n\n" ++ show e))+ (\(e::C.SomeException) -> appendFile rf ("\n\n" ++ unlines (init (lines (show e))))) ] q :: Symbolic ()
SBVTestSuite/Utils/SBVTestFramework.hs view
@@ -59,7 +59,7 @@ data CIOS = CILinux | CIOSX | CIWindows- deriving Show+ deriving (Show, Eq) data TestEnvironment = TestEnvLocal | TestEnvCI CIOS
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 7.2+Version: 7.3 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT@@ -165,6 +165,7 @@ main-is : SBVTest.hs Other-modules : Utils.SBVTestFramework , TestSuite.Arrays.Memory+ , TestSuite.Arrays.Query , TestSuite.Basics.AllSat , TestSuite.Basics.ArithNoSolver , TestSuite.Basics.ArithSolver