diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,15 @@ * Hackage: * GitHub: -* 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. diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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 diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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 diff --git a/Data/SBV/SMT/Utils.hs b/Data/SBV/SMT/Utils.hs --- a/Data/SBV/SMT/Utils.hs +++ b/Data/SBV/SMT/Utils.hs @@ -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 diff --git a/SBVTestSuite/GoldFiles/queryArrays1.gold b/SBVTestSuite/GoldFiles/queryArrays1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/queryArrays1.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/queryArrays2.gold b/SBVTestSuite/GoldFiles/queryArrays2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/queryArrays2.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/queryArrays3.gold b/SBVTestSuite/GoldFiles/queryArrays3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/queryArrays3.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/queryArrays4.gold b/SBVTestSuite/GoldFiles/queryArrays4.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/queryArrays4.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/queryArrays5.gold b/SBVTestSuite/GoldFiles/queryArrays5.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/queryArrays5.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold --- a/SBVTestSuite/GoldFiles/query_badOption.gold +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -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 diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs --- a/SBVTestSuite/SBVDocTest.hs +++ b/SBVTestSuite/SBVDocTest.hs @@ -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 diff --git a/SBVTestSuite/SBVHLint.hs b/SBVTestSuite/SBVHLint.hs --- a/SBVTestSuite/SBVHLint.hs +++ b/SBVTestSuite/SBVHLint.hs @@ -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 diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Arrays/Query.hs b/SBVTestSuite/TestSuite/Arrays/Query.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Arrays/Query.hs @@ -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) #-} diff --git a/SBVTestSuite/TestSuite/Queries/BadOption.hs b/SBVTestSuite/TestSuite/Queries/BadOption.hs --- a/SBVTestSuite/TestSuite/Queries/BadOption.hs +++ b/SBVTestSuite/TestSuite/Queries/BadOption.hs @@ -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 () diff --git a/SBVTestSuite/Utils/SBVTestFramework.hs b/SBVTestSuite/Utils/SBVTestFramework.hs --- a/SBVTestSuite/Utils/SBVTestFramework.hs +++ b/SBVTestSuite/Utils/SBVTestFramework.hs @@ -59,7 +59,7 @@ data CIOS = CILinux | CIOSX | CIWindows - deriving Show + deriving (Show, Eq) data TestEnvironment = TestEnvLocal | TestEnvCI CIOS diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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