diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,22 @@ * Hackage: * GitHub: -* Latest Hackage released version: 8.2, 2019-04-07 +* Latest Hackage released version: 8.3, 2019-06-08 + +### Version 8.3, 2019-06-08 + + * Increment base dependency to 4.11. + + * Add support for `Data.Set.hasSize`. + + * Add `supportsFP` to CVC4 capabilities list. (#469) + + * Fix a glitch in allSat computations that incorrectly + used values of internal variables in model construction. + + * SBV now directly uses the new `seq.nth` function from z3 + for sequence element access, instead of implementing it + internally. ### Version 8.2, 2019-04-07 diff --git a/Data/SBV/Client.hs b/Data/SBV/Client.hs --- a/Data/SBV/Client.hs +++ b/Data/SBV/Client.hs @@ -9,6 +9,7 @@ -- Cross-cutting toplevel client functions ----------------------------------------------------------------------------- +{-# LANGUAGE PackageImports #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} @@ -25,7 +26,8 @@ import Data.Generics import qualified Control.Exception as C -import qualified Language.Haskell.TH as TH + +import qualified "template-haskell" Language.Haskell.TH as TH import Data.SBV.Core.Data import Data.SBV.Core.Model 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 @@ -42,7 +42,7 @@ ) where import Data.Maybe (isJust) -import Data.List (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort) +import Data.List (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf) import Data.Char (isPunctuation, isSpace, chr, ord, isDigit) import Data.Function (on) @@ -1261,7 +1261,9 @@ mkSVal :: NamedSymVar -> (SVal, NamedSymVar) mkSVal nm@(sv, _) = (SVal (kindOf sv) (Right (cache (const (return sv)))), nm) - in map mkSVal $ sortByNodeId [nv | (_, nv@(_, n)) <- allModelInputs, not (isNonModelVar cfg n)] + ignored n = isNonModelVar cfg n || "__internal_sbv" `isPrefixOf` n + + in map mkSVal $ sortByNodeId [nv | (_, nv@(_, n)) <- allModelInputs, not (ignored n)] -- If we have any universals, then the solutions are unique upto prefix existentials. w = ALL `elem` map fst qinps 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 @@ -263,6 +263,7 @@ data StrOp = StrConcat -- ^ Concatenation of one or more strings | StrLen -- ^ String length | StrUnit -- ^ Unit string + | StrNth -- ^ Nth element | StrSubstr -- ^ Retrieves substring of @s@ at @offset@ | StrIndexOf -- ^ Retrieves first position of @sub@ in @s@, @-1@ if there are no occurrences | StrContains -- ^ Does @s@ contain the substring @sub@? @@ -348,6 +349,7 @@ show StrConcat = "str.++" show StrLen = "str.len" show StrUnit = "seq.unit" -- NB. The "seq" prefix is intentional; works uniformly. + show StrNth = "seq.nth" -- NB. The "seq" prefix is intentional; works uniformly. show StrSubstr = "str.substr" show StrIndexOf = "str.indexof" show StrContains = "str.contains" @@ -363,6 +365,7 @@ data SeqOp = SeqConcat -- ^ See StrConcat | SeqLen -- ^ See StrLen | SeqUnit -- ^ See StrUnit + | SeqNth -- ^ See StrNth | SeqSubseq -- ^ See StrSubseq | SeqIndexOf -- ^ See StrIndexOf | SeqContains -- ^ See StrContains @@ -376,6 +379,7 @@ show SeqConcat = "seq.++" show SeqLen = "seq.len" show SeqUnit = "seq.unit" + show SeqNth = "seq.nth" show SeqSubseq = "seq.extract" show SeqIndexOf = "seq.indexof" show SeqContains = "seq.contains" @@ -393,6 +397,7 @@ | SetSubset | SetDifference | SetComplement + | SetHasSize deriving (Eq, Ord) -- The show instance for 'SetOp' is merely for debugging, we map them separately so @@ -407,6 +412,7 @@ show SetSubset = "Set.subset" show SetDifference = "Set.difference" show SetComplement = "Set.complement" + show SetHasSize = "Set.setHasSize" -- Show instance for 'Op'. Note that this is largely for debugging purposes, not used -- for being read by any tool. @@ -628,12 +634,12 @@ instance NFData Penalty where rnf DefaultPenalty = () - rnf (Penalty p mbs) = rnf p `seq` rnf mbs `seq` () + rnf (Penalty p mbs) = rnf p `seq` rnf mbs instance NFData a => NFData (Objective a) where - rnf (Minimize s a) = rnf s `seq` rnf a `seq` () - rnf (Maximize s a) = rnf s `seq` rnf a `seq` () - rnf (AssertWithPenalty s a p) = rnf s `seq` rnf a `seq` rnf p `seq` () + rnf (Minimize s a) = rnf s `seq` rnf a + rnf (Maximize s a) = rnf s `seq` rnf a + rnf (AssertWithPenalty s a p) = rnf s `seq` rnf a `seq` rnf p -- | Result of running a symbolic computation data Result = Result { reskinds :: Set.Set Kind -- ^ kinds used in the program @@ -1620,7 +1626,7 @@ stored <- readIORef rCache sn <- f `seq` makeStableName f let h = hashStableName sn - case maybe Nothing (sn `lookup`) (h `IMap.lookup` stored) of + case (h `IMap.lookup` stored) >>= (sn `lookup`) of Just r -> return r Nothing -> do r <- f st r `seq` R.modifyIORef' rCache (IMap.insertWith (++) h [(sn, r)]) @@ -1640,7 +1646,7 @@ data SMTLibPgm = SMTLibPgm SMTLibVersion [String] instance NFData SMTLibVersion where rnf a = a `seq` () -instance NFData SMTLibPgm where rnf (SMTLibPgm v p) = rnf v `seq` rnf p `seq` () +instance NFData SMTLibPgm where rnf (SMTLibPgm v p) = rnf v `seq` rnf p instance Show SMTLibPgm where show (SMTLibPgm _ pre) = intercalate "\n" pre @@ -1675,20 +1681,20 @@ instance NFData SBVType where rnf a = seq a () instance NFData SBVPgm where rnf a = seq a () instance NFData (Cached a) where rnf (Cached f) = f `seq` () -instance NFData SVal where rnf (SVal x y) = rnf x `seq` rnf y `seq` () +instance NFData SVal where rnf (SVal x y) = rnf x `seq` rnf y instance NFData SMTResult where rnf (Unsatisfiable _ xs ) = rnf xs - rnf (Satisfiable _ xs ) = rnf xs `seq` () - rnf (SatExtField _ xs ) = rnf xs `seq` () - rnf (Unknown _ xs ) = rnf xs `seq` () - rnf (ProofError _ xs mr) = rnf xs `seq` rnf mr `seq` () + rnf (Satisfiable _ xs ) = rnf xs + rnf (SatExtField _ xs ) = rnf xs + rnf (Unknown _ xs ) = rnf xs + rnf (ProofError _ xs mr) = rnf xs `seq` rnf mr instance NFData SMTModel where - rnf (SMTModel objs bndgs assocs uifuns) = rnf objs `seq` rnf bndgs `seq` rnf assocs `seq` rnf uifuns `seq` () + rnf (SMTModel objs bndgs assocs uifuns) = rnf objs `seq` rnf bndgs `seq` rnf assocs `seq` rnf uifuns instance NFData SMTScript where - rnf (SMTScript b m) = rnf b `seq` rnf m `seq` () + rnf (SMTScript b m) = rnf b `seq` rnf m -- | Translation tricks needed for specific capabilities afforded by each solver data SolverCapabilities = SolverCapabilities { diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -135,40 +135,16 @@ -- | @`elemAt` l i@ is the value stored at location @i@. Unspecified if -- index is out of bounds. -- --- >>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger) +-- >>> prove $ \i -> i `inRange` (0, 4) .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger) -- Q.E.D. --- >>> prove $ \(l :: SList Integer) i e -> l `elemAt` i .== e .=> indexOf l (singleton e) .<= i +-- >>> prove $ \(l :: SList Integer) i e -> i `inRange` (0, length l - 1) .&& l `elemAt` i .== e .=> indexOf l (singleton e) .<= i -- Q.E.D. elemAt :: forall a. SymVal a => SList a -> SInteger -> SBV a elemAt l i | Just xs <- unliteral l, Just ci <- unliteral i, ci >= 0, ci < genericLength xs, let x = xs `genericIndex` ci = literal x | True - = SBV (SVal kElem (Right (cache (y (l `listToListAt` i))))) - where kElem = kindOf (Proxy @a) - kSeq = KList kElem - - -- This is trickier than it needs to be, but necessary since there's - -- no SMTLib function to extract the element from a list. Instead, - -- we form a singleton list, and assert that it is equivalent to - -- the extracted value. See - y si st = do -- grab an internal variable and make a unit list out of it - e <- internalVariable st kElem - es <- newExpr st kSeq (SBVApp (SeqOp SeqUnit) [e]) - - -- Create the condition that it is equal to si - li <- sbvToSV st si - eq <- newExpr st KBool (SBVApp Equal [es, li]) - - -- Gotta make sure we do this only when length is at least > i - caseTooShort <- sbvToSV st (length l .<= i) - require <- newExpr st KBool (SBVApp Or [caseTooShort, eq]) - - -- register the constraint: - internalConstraint st False [] $ SVal KBool $ Right $ cache $ \_ -> return require - - -- We're good to go: - return e + = lift2 SeqNth Nothing l i -- | Short cut for 'elemAt' (.!!) :: SymVal a => SList a -> SInteger -> SBV a @@ -339,10 +315,6 @@ -- -- >>> prove $ \(l :: SList Int8) i -> i .> 0 .&& i .< length l .=> indexOf l (subList l i 1) .<= i -- Q.E.D. --- >>> prove $ \(l :: SList Word16) i -> i .> 0 .&& i .< length l .=> indexOf l (subList l i 1) .== i --- Falsifiable. Counter-example: --- s0 = [2048,0,0,0,0,0] :: [Word16] --- s1 = 3 :: Integer -- >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 .=> indexOf l1 l2 .== -1 -- Q.E.D. indexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -34,7 +34,7 @@ , supportsUnboundedInts = True , supportsReals = True -- Not quite the same capability as Z3; but works more or less.. , supportsApproxReals = False - , supportsIEEE754 = False + , supportsIEEE754 = True , supportsSets = False , supportsOptimization = False , supportsPseudoBooleans = False 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 @@ -45,6 +45,7 @@ hasDouble = KDouble `Set.member` kindInfo hasBVs = hasChar || not (null [() | KBounded{} <- Set.toList kindInfo]) -- Remember, characters map to Word8 usorts = [(s, dt) | KUninterpreted s dt <- Set.toList kindInfo] + trueUSorts = [s | (s, _) <- usorts, s /= "RoundingMode"] tupleArities = findTupleArities kindInfo hasNonBVArrays = (not . null) [() | (_, (_, (k1, k2), _)) <- arrs, not (isBounded k1 && isBounded k2)] hasArrayInits = (not . null) [() | (_, (_, _, ArrayFree (Just _))) <- arrs] @@ -97,29 +98,27 @@ -- we never set QF_S (ALL seems to work better in all cases) - | hasArrayInits - = ["(set-logic ALL)"] - - | hasString || hasList - = ["(set-logic ALL)"] + | hasInteger || hasReal || not (null trueUSorts) || hasNonBVArrays || hasTuples || hasEither || hasMaybe || hasSets || hasList || hasString || hasArrayInits + = let why | hasInteger = "has unbounded values" + | hasReal = "has algebraic reals" + | not (null trueUSorts) = "has user-defined sorts" + | hasNonBVArrays = "has non-bitvector arrays" + | hasTuples = "has tuples" + | hasEither = "has either type" + | hasMaybe = "has maybe type" + | hasSets = "has sets" + | hasList = "has lists" + | hasString = "has strings" + | hasArrayInits = "has array initializers" + | True = "cannot determine the SMTLib-logic to use" + in ["(set-logic ALL) ; " ++ why ++ ", using catch-all."] | hasDouble || hasFloat - = if hasInteger || not (null foralls) + = if not (null foralls) then ["(set-logic ALL)"] else if hasBVs then ["(set-logic QF_FPBV)"] else ["(set-logic QF_FP)"] - | hasInteger || hasReal || not (null usorts) || hasNonBVArrays || hasTuples || hasEither || hasMaybe || hasSets - = let why | hasInteger = "has unbounded values" - | hasReal = "has algebraic reals" - | not (null usorts) = "has user-defined sorts" - | hasNonBVArrays = "has non-bitvector arrays" - | hasTuples = "has tuples" - | hasEither = "has either type" - | hasMaybe = "has maybe type" - | hasSets = "has sets" - | True = "cannot determine the SMTLib-logic to use" - in ["(set-logic ALL) ; " ++ why ++ ", using catch-all."] -- If we're in a user query context, we'll pick ALL, otherwise -- we'll stick to some bit-vector logic based on what we see in the problem. @@ -834,11 +833,12 @@ sh (SBVApp (SetOp SetMember) [e, s]) = "(select " ++ ssv s ++ " " ++ ssv e ++ ")" sh (SBVApp (SetOp SetInsert) [e, s]) = "(store " ++ ssv s ++ " " ++ ssv e ++ " true)" sh (SBVApp (SetOp SetDelete) [e, s]) = "(store " ++ ssv s ++ " " ++ ssv e ++ " false)" - sh (SBVApp (SetOp SetIntersect) args) = "((_ map and) " ++ unwords (map ssv args) ++ ")" - sh (SBVApp (SetOp SetUnion) args) = "((_ map or) " ++ unwords (map ssv args) ++ ")" - sh (SBVApp (SetOp SetSubset) args) = "(subset " ++ unwords (map ssv args) ++ ")" - sh (SBVApp (SetOp SetDifference) args) = "(difference " ++ unwords (map ssv args) ++ ")" - sh (SBVApp (SetOp SetComplement) args) = "((_ map not) " ++ unwords (map ssv args) ++ ")" + sh (SBVApp (SetOp SetIntersect) args) = "(intersection " ++ unwords (map ssv args) ++ ")" + sh (SBVApp (SetOp SetUnion) args) = "(union " ++ unwords (map ssv args) ++ ")" + sh (SBVApp (SetOp SetSubset) args) = "(subset " ++ unwords (map ssv args) ++ ")" + sh (SBVApp (SetOp SetDifference) args) = "(setminus " ++ unwords (map ssv args) ++ ")" + sh (SBVApp (SetOp SetComplement) args) = "(complement " ++ unwords (map ssv args) ++ ")" + sh (SBVApp (SetOp SetHasSize) args) = "(set-has-size " ++ unwords (map ssv args) ++ ")" sh (SBVApp (TupleConstructor 0) []) = "mkSBVTuple0" sh (SBVApp (TupleConstructor n) args) = "(mkSBVTuple" ++ show n ++ " " ++ unwords (map ssv args) ++ ")" diff --git a/Data/SBV/Set.hs b/Data/SBV/Set.hs --- a/Data/SBV/Set.hs +++ b/Data/SBV/Set.hs @@ -19,6 +19,10 @@ -- which is something you cannot do in Haskell! Conversely, you cannot compute -- the size of a symbolic set (as it can be infinite!), nor you can turn -- it into a list or necessarily enumerate its elements. +-- +-- __A note on cardinality__: You can indirectly talk about cardinality: 'Data.SBV.Set.hasSize' +-- can be used to state that the set is finite and has size @k@ for a user-specified symbolic +-- integer @k@. ----------------------------------------------------------------------------- {-# LANGUAGE Rank2Types #-} @@ -36,7 +40,7 @@ , insert, delete -- * Query - , member, notMember, null, isEmpty, isFull, isUniversal, isSubsetOf, isProperSubsetOf, disjoint + , member, notMember, null, isEmpty, isFull, isUniversal, hasSize, isSubsetOf, isProperSubsetOf, disjoint -- * Combinations , union, unions, intersection, intersections, difference, (\\) @@ -293,6 +297,44 @@ isUniversal :: HasKind a => SSet a -> SBool isUniversal = isFull +-- | Does the set have the given size? It implicitly asserts that the set +-- it is operating on is finite. Also see 'Data.SBV.Set.card'. +-- +-- >>> prove $ \i -> hasSize (empty :: SSet Integer) i .== (i .== 0) +-- Q.E.D. +-- +-- >>> sat $ \i -> hasSize (full :: SSet Integer) i +-- Unsatisfiable +-- +-- >>> prove $ \a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a `union` b) k .=> k .>= i `smax` j +-- Q.E.D. +-- +-- >>> prove $ \a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a `intersection` b) k .=> k .<= i `smin` j +-- Q.E.D. +-- +-- >>> prove $ \a k -> hasSize (a :: SSet Integer) k .=> k .>= 0 +-- Q.E.D. +hasSize :: (Ord a, SymVal a) => SSet a -> SInteger -> SBool +hasSize sa si + -- Case 1: Constant regular set, see if the size matches + | Just (RegularSet a) <- unliteral sa + = literal (fromIntegral (Set.size a)) .== si + + -- Case 2: Constant complement set, will never have finite size + | Just (ComplementSet _) <- unliteral sa + = sFalse + + -- Case 3: Integer is constant, and is negative: + | Just i <- unliteral si, i < 0 + = sFalse + + -- Otherwise, go symbolic + | True + = SBV $ SVal KBool $ Right $ cache r + where r st = do sva <- sbvToSV st sa + svi <- sbvToSV st si + newExpr st KBool $ SBVApp (SetOp SetHasSize) [sva, svi] + -- | Subset test. -- -- >>> prove $ empty `isSubsetOf` (full :: SSet Integer) @@ -327,16 +369,16 @@ -- -- >>> prove $ \x (s :: SSet Integer) -> s `isProperSubsetOf` (x `insert` s) -- Falsifiable. Counter-example: --- s0 = 0 :: Integer --- s1 = U - {1} :: {Integer} +-- s0 = 0 :: Integer +-- s1 = U :: {Integer} -- -- >>> prove $ \x (s :: SSet Integer) -> x `notMember` s .=> s `isProperSubsetOf` (x `insert` s) -- Q.E.D. -- -- >>> prove $ \x (s :: SSet Integer) -> (x `delete` s) `isProperSubsetOf` s -- Falsifiable. Counter-example: --- s0 = 0 :: Integer --- s1 = {1} :: {Integer} +-- s0 = 0 :: Integer +-- s1 = {} :: {Integer} -- -- >>> prove $ \x (s :: SSet Integer) -> x `member` s .=> (x `delete` s) `isProperSubsetOf` s -- Q.E.D. diff --git a/Data/SBV/String.hs b/Data/SBV/String.hs --- a/Data/SBV/String.hs +++ b/Data/SBV/String.hs @@ -140,24 +140,14 @@ -- -- >>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `strToCharAt` i .== literal 'A' -- Q.E.D. --- >>> prove $ \s i c -> s `strToCharAt` i .== c .=> indexOf s (singleton c) .<= i +-- >>> prove $ \s i c -> i `inRange` (0, length s - 1) .&& s `strToCharAt` i .== c .=> indexOf s (singleton c) .<= i -- Q.E.D. strToCharAt :: SString -> SInteger -> SChar strToCharAt s i | Just cs <- unliteral s, Just ci <- unliteral i, ci >= 0, ci < genericLength cs, let c = C.ord (cs `genericIndex` ci) = literal (C.chr c) | True - = SBV (SVal w8 (Right (cache (y (s `strToStrAt` i))))) - where w8 = KBounded False 8 - -- This is trickier than it needs to be, but necessary since there's - -- no SMTLib function to extract the character from a string. Instead, - -- we form a singleton string, and assert that it is equivalent to - -- the extracted value. See - y si st = do c <- internalVariable st w8 - cs <- newExpr st KString (SBVApp (StrOp StrUnit) [c]) - let csSBV = SBV (SVal KString (Right (cache (\_ -> return cs)))) - internalConstraint st False [] $ unSBV $ length s .> i .=> csSBV .== si - return c + = lift2 StrNth Nothing s i -- | Short cut for 'strToCharAt' (.!!) :: SString -> SInteger -> SChar @@ -320,10 +310,6 @@ -- -- >>> prove $ \s i -> i .> 0 .&& i .< length s .=> indexOf s (subStr s i 1) .<= i -- Q.E.D. --- >>> prove $ \s i -> i .> 0 .&& i .< length s .=> indexOf s (subStr s i 1) .== i --- Falsifiable. Counter-example: --- s0 = "\128\NUL\NUL" :: String --- s1 = 2 :: Integer -- >>> prove $ \s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1 -- Q.E.D. indexOf :: SString -> SString -> SInteger @@ -355,7 +341,7 @@ -- that is, if it encodes a natural number. Otherwise, it returns '-1'. -- See for details. -- --- >>> prove $ \s -> let n = strToNat s in n .>= 0 .&& n .< 10 .=> length s .== 1 +-- >>> prove $ \s -> let n = strToNat s in length s .== 1 .=> (-1) .<= n .&& n .<= 9 -- Q.E.D. strToNat :: SString -> SInteger strToNat s diff --git a/SBVTestSuite/GoldFiles/foldlABC1.gold b/SBVTestSuite/GoldFiles/foldlABC1.gold --- a/SBVTestSuite/GoldFiles/foldlABC1.gold +++ b/SBVTestSuite/GoldFiles/foldlABC1.gold @@ -7,18 +7,16 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s3 () Int 0) -[GOOD] (define-fun s16 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -35,20 +33,15 @@ [GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) [GOOD] (define-fun s12 () Int (seq.len s11)) [GOOD] (define-fun s13 () Bool (= s3 s12)) -[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s3 s16)) +[GOOD] (define-fun s14 () Int (seq.nth s11 s3)) +[GOOD] (define-fun s15 () Int (ite s13 s3 s14)) +[GOOD] (define-fun s16 () Int (+ s0 s1)) +[GOOD] (define-fun s17 () Int (+ s2 s16)) [GOOD] (define-fun s18 () Bool (= s15 s17)) -[GOOD] (define-fun s19 () Bool (<= s12 s3)) -[GOOD] (define-fun s20 () Bool (or s18 s19)) -[GOOD] (define-fun s21 () Int (ite s13 s3 s14)) -[GOOD] (define-fun s22 () Int (+ s0 s1)) -[GOOD] (define-fun s23 () Int (+ s2 s22)) -[GOOD] (define-fun s24 () Bool (= s21 s23)) [GOOD] (assert s4) [GOOD] (assert s5) [GOOD] (assert s6) -[GOOD] (assert s20) -[GOOD] (assert s24) +[GOOD] (assert s18) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/foldlABC2.gold b/SBVTestSuite/GoldFiles/foldlABC2.gold --- a/SBVTestSuite/GoldFiles/foldlABC2.gold +++ b/SBVTestSuite/GoldFiles/foldlABC2.gold @@ -7,19 +7,17 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s3 () Int 0) -[GOOD] (define-fun s16 () Int 1) +[GOOD] (define-fun s15 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14" -[GOOD] (declare-fun s25 () Int) ; tracks user variable "__internal_sbv_s25" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -36,32 +34,22 @@ [GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) [GOOD] (define-fun s12 () Int (seq.len s11)) [GOOD] (define-fun s13 () Bool (= s3 s12)) -[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s3 s16)) -[GOOD] (define-fun s18 () Bool (= s15 s17)) -[GOOD] (define-fun s19 () Bool (<= s12 s3)) -[GOOD] (define-fun s20 () Bool (or s18 s19)) -[GOOD] (define-fun s21 () Int (- s12 s16)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s11 s16 s21)) -[GOOD] (define-fun s23 () Int (seq.len s22)) -[GOOD] (define-fun s24 () Bool (= s3 s23)) -[GOOD] (define-fun s26 () (Seq Int) (seq.unit s25)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s3 s16)) -[GOOD] (define-fun s28 () Bool (= s26 s27)) -[GOOD] (define-fun s29 () Bool (<= s23 s3)) -[GOOD] (define-fun s30 () Bool (or s28 s29)) -[GOOD] (define-fun s31 () Int (ite s24 s3 s25)) -[GOOD] (define-fun s32 () Int (+ s14 s31)) -[GOOD] (define-fun s33 () Int (ite s13 s3 s32)) -[GOOD] (define-fun s34 () Int (+ s0 s1)) -[GOOD] (define-fun s35 () Int (+ s2 s34)) -[GOOD] (define-fun s36 () Bool (= s33 s35)) +[GOOD] (define-fun s14 () Int (seq.nth s11 s3)) +[GOOD] (define-fun s16 () Int (- s12 s15)) +[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s15 s16)) +[GOOD] (define-fun s18 () Int (seq.len s17)) +[GOOD] (define-fun s19 () Bool (= s3 s18)) +[GOOD] (define-fun s20 () Int (seq.nth s17 s3)) +[GOOD] (define-fun s21 () Int (ite s19 s3 s20)) +[GOOD] (define-fun s22 () Int (+ s14 s21)) +[GOOD] (define-fun s23 () Int (ite s13 s3 s22)) +[GOOD] (define-fun s24 () Int (+ s0 s1)) +[GOOD] (define-fun s25 () Int (+ s2 s24)) +[GOOD] (define-fun s26 () Bool (= s23 s25)) [GOOD] (assert s4) [GOOD] (assert s5) [GOOD] (assert s6) -[GOOD] (assert s20) -[GOOD] (assert s30) -[GOOD] (assert s36) +[GOOD] (assert s26) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/foldlABC3.gold b/SBVTestSuite/GoldFiles/foldlABC3.gold --- a/SBVTestSuite/GoldFiles/foldlABC3.gold +++ b/SBVTestSuite/GoldFiles/foldlABC3.gold @@ -7,20 +7,17 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s3 () Int 0) -[GOOD] (define-fun s16 () Int 1) +[GOOD] (define-fun s15 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14" -[GOOD] (declare-fun s25 () Int) ; tracks user variable "__internal_sbv_s25" -[GOOD] (declare-fun s35 () Int) ; tracks user variable "__internal_sbv_s35" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -37,44 +34,29 @@ [GOOD] (define-fun s11 () (Seq Int) (seq.++ s7 s10)) [GOOD] (define-fun s12 () Int (seq.len s11)) [GOOD] (define-fun s13 () Bool (= s3 s12)) -[GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s3 s16)) -[GOOD] (define-fun s18 () Bool (= s15 s17)) -[GOOD] (define-fun s19 () Bool (<= s12 s3)) -[GOOD] (define-fun s20 () Bool (or s18 s19)) -[GOOD] (define-fun s21 () Int (- s12 s16)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s11 s16 s21)) +[GOOD] (define-fun s14 () Int (seq.nth s11 s3)) +[GOOD] (define-fun s16 () Int (- s12 s15)) +[GOOD] (define-fun s17 () (Seq Int) (seq.extract s11 s15 s16)) +[GOOD] (define-fun s18 () Int (seq.len s17)) +[GOOD] (define-fun s19 () Bool (= s3 s18)) +[GOOD] (define-fun s20 () Int (seq.nth s17 s3)) +[GOOD] (define-fun s21 () Int (- s18 s15)) +[GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s15 s21)) [GOOD] (define-fun s23 () Int (seq.len s22)) [GOOD] (define-fun s24 () Bool (= s3 s23)) -[GOOD] (define-fun s26 () (Seq Int) (seq.unit s25)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s3 s16)) -[GOOD] (define-fun s28 () Bool (= s26 s27)) -[GOOD] (define-fun s29 () Bool (<= s23 s3)) -[GOOD] (define-fun s30 () Bool (or s28 s29)) -[GOOD] (define-fun s31 () Int (- s23 s16)) -[GOOD] (define-fun s32 () (Seq Int) (seq.extract s22 s16 s31)) -[GOOD] (define-fun s33 () Int (seq.len s32)) -[GOOD] (define-fun s34 () Bool (= s3 s33)) -[GOOD] (define-fun s36 () (Seq Int) (seq.unit s35)) -[GOOD] (define-fun s37 () (Seq Int) (seq.extract s32 s3 s16)) -[GOOD] (define-fun s38 () Bool (= s36 s37)) -[GOOD] (define-fun s39 () Bool (<= s33 s3)) -[GOOD] (define-fun s40 () Bool (or s38 s39)) -[GOOD] (define-fun s41 () Int (ite s34 s3 s35)) -[GOOD] (define-fun s42 () Int (+ s25 s41)) -[GOOD] (define-fun s43 () Int (ite s24 s3 s42)) -[GOOD] (define-fun s44 () Int (+ s14 s43)) -[GOOD] (define-fun s45 () Int (ite s13 s3 s44)) -[GOOD] (define-fun s46 () Int (+ s0 s1)) -[GOOD] (define-fun s47 () Int (+ s2 s46)) -[GOOD] (define-fun s48 () Bool (= s45 s47)) +[GOOD] (define-fun s25 () Int (seq.nth s22 s3)) +[GOOD] (define-fun s26 () Int (ite s24 s3 s25)) +[GOOD] (define-fun s27 () Int (+ s20 s26)) +[GOOD] (define-fun s28 () Int (ite s19 s3 s27)) +[GOOD] (define-fun s29 () Int (+ s14 s28)) +[GOOD] (define-fun s30 () Int (ite s13 s3 s29)) +[GOOD] (define-fun s31 () Int (+ s0 s1)) +[GOOD] (define-fun s32 () Int (+ s2 s31)) +[GOOD] (define-fun s33 () Bool (= s30 s32)) [GOOD] (assert s4) [GOOD] (assert s5) [GOOD] (assert s6) -[GOOD] (assert s20) -[GOOD] (assert s30) -[GOOD] (assert s40) -[GOOD] (assert s48) +[GOOD] (assert s33) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/foldrAB1.gold b/SBVTestSuite/GoldFiles/foldrAB1.gold --- a/SBVTestSuite/GoldFiles/foldrAB1.gold +++ b/SBVTestSuite/GoldFiles/foldrAB1.gold @@ -7,17 +7,15 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 0) -[GOOD] (define-fun s12 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s10 () Int) ; tracks user variable "__internal_sbv_s10" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -31,18 +29,13 @@ [GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) [GOOD] (define-fun s8 () Int (seq.len s7)) [GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s11 () (Seq Int) (seq.unit s10)) -[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s2 s12)) -[GOOD] (define-fun s14 () Bool (= s11 s13)) -[GOOD] (define-fun s15 () Bool (<= s8 s2)) -[GOOD] (define-fun s16 () Bool (or s14 s15)) -[GOOD] (define-fun s17 () Int (ite s9 s2 s10)) -[GOOD] (define-fun s18 () Int (+ s0 s1)) -[GOOD] (define-fun s19 () Bool (= s17 s18)) +[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) +[GOOD] (define-fun s11 () Int (ite s9 s2 s10)) +[GOOD] (define-fun s12 () Int (+ s0 s1)) +[GOOD] (define-fun s13 () Bool (= s11 s12)) [GOOD] (assert s3) [GOOD] (assert s4) -[GOOD] (assert s16) -[GOOD] (assert s19) +[GOOD] (assert s13) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/foldrAB2.gold b/SBVTestSuite/GoldFiles/foldrAB2.gold --- a/SBVTestSuite/GoldFiles/foldrAB2.gold +++ b/SBVTestSuite/GoldFiles/foldrAB2.gold @@ -7,18 +7,16 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 0) -[GOOD] (define-fun s12 () Int 1) +[GOOD] (define-fun s11 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s10 () Int) ; tracks user variable "__internal_sbv_s10" -[GOOD] (declare-fun s21 () Int) ; tracks user variable "__internal_sbv_s21" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -32,30 +30,20 @@ [GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) [GOOD] (define-fun s8 () Int (seq.len s7)) [GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s11 () (Seq Int) (seq.unit s10)) -[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s2 s12)) -[GOOD] (define-fun s14 () Bool (= s11 s13)) -[GOOD] (define-fun s15 () Bool (<= s8 s2)) -[GOOD] (define-fun s16 () Bool (or s14 s15)) -[GOOD] (define-fun s17 () Int (- s8 s12)) -[GOOD] (define-fun s18 () (Seq Int) (seq.extract s7 s12 s17)) -[GOOD] (define-fun s19 () Int (seq.len s18)) -[GOOD] (define-fun s20 () Bool (= s2 s19)) -[GOOD] (define-fun s22 () (Seq Int) (seq.unit s21)) -[GOOD] (define-fun s23 () (Seq Int) (seq.extract s18 s2 s12)) -[GOOD] (define-fun s24 () Bool (= s22 s23)) -[GOOD] (define-fun s25 () Bool (<= s19 s2)) -[GOOD] (define-fun s26 () Bool (or s24 s25)) -[GOOD] (define-fun s27 () Int (ite s20 s2 s21)) -[GOOD] (define-fun s28 () Int (+ s10 s27)) -[GOOD] (define-fun s29 () Int (ite s9 s2 s28)) -[GOOD] (define-fun s30 () Int (+ s0 s1)) -[GOOD] (define-fun s31 () Bool (= s29 s30)) +[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) +[GOOD] (define-fun s12 () Int (- s8 s11)) +[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s11 s12)) +[GOOD] (define-fun s14 () Int (seq.len s13)) +[GOOD] (define-fun s15 () Bool (= s2 s14)) +[GOOD] (define-fun s16 () Int (seq.nth s13 s2)) +[GOOD] (define-fun s17 () Int (ite s15 s2 s16)) +[GOOD] (define-fun s18 () Int (+ s10 s17)) +[GOOD] (define-fun s19 () Int (ite s9 s2 s18)) +[GOOD] (define-fun s20 () Int (+ s0 s1)) +[GOOD] (define-fun s21 () Bool (= s19 s20)) [GOOD] (assert s3) [GOOD] (assert s4) -[GOOD] (assert s16) -[GOOD] (assert s26) -[GOOD] (assert s31) +[GOOD] (assert s21) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/foldrAB3.gold b/SBVTestSuite/GoldFiles/foldrAB3.gold --- a/SBVTestSuite/GoldFiles/foldrAB3.gold +++ b/SBVTestSuite/GoldFiles/foldrAB3.gold @@ -7,19 +7,16 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 0) -[GOOD] (define-fun s12 () Int 1) +[GOOD] (define-fun s11 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" -[GOOD] (declare-fun s10 () Int) ; tracks user variable "__internal_sbv_s10" -[GOOD] (declare-fun s21 () Int) ; tracks user variable "__internal_sbv_s21" -[GOOD] (declare-fun s31 () Int) ; tracks user variable "__internal_sbv_s31" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -33,42 +30,27 @@ [GOOD] (define-fun s7 () (Seq Int) (seq.++ s5 s6)) [GOOD] (define-fun s8 () Int (seq.len s7)) [GOOD] (define-fun s9 () Bool (= s2 s8)) -[GOOD] (define-fun s11 () (Seq Int) (seq.unit s10)) -[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s2 s12)) -[GOOD] (define-fun s14 () Bool (= s11 s13)) -[GOOD] (define-fun s15 () Bool (<= s8 s2)) -[GOOD] (define-fun s16 () Bool (or s14 s15)) -[GOOD] (define-fun s17 () Int (- s8 s12)) -[GOOD] (define-fun s18 () (Seq Int) (seq.extract s7 s12 s17)) +[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) +[GOOD] (define-fun s12 () Int (- s8 s11)) +[GOOD] (define-fun s13 () (Seq Int) (seq.extract s7 s11 s12)) +[GOOD] (define-fun s14 () Int (seq.len s13)) +[GOOD] (define-fun s15 () Bool (= s2 s14)) +[GOOD] (define-fun s16 () Int (seq.nth s13 s2)) +[GOOD] (define-fun s17 () Int (- s14 s11)) +[GOOD] (define-fun s18 () (Seq Int) (seq.extract s13 s11 s17)) [GOOD] (define-fun s19 () Int (seq.len s18)) [GOOD] (define-fun s20 () Bool (= s2 s19)) -[GOOD] (define-fun s22 () (Seq Int) (seq.unit s21)) -[GOOD] (define-fun s23 () (Seq Int) (seq.extract s18 s2 s12)) -[GOOD] (define-fun s24 () Bool (= s22 s23)) -[GOOD] (define-fun s25 () Bool (<= s19 s2)) -[GOOD] (define-fun s26 () Bool (or s24 s25)) -[GOOD] (define-fun s27 () Int (- s19 s12)) -[GOOD] (define-fun s28 () (Seq Int) (seq.extract s18 s12 s27)) -[GOOD] (define-fun s29 () Int (seq.len s28)) -[GOOD] (define-fun s30 () Bool (= s2 s29)) -[GOOD] (define-fun s32 () (Seq Int) (seq.unit s31)) -[GOOD] (define-fun s33 () (Seq Int) (seq.extract s28 s2 s12)) -[GOOD] (define-fun s34 () Bool (= s32 s33)) -[GOOD] (define-fun s35 () Bool (<= s29 s2)) -[GOOD] (define-fun s36 () Bool (or s34 s35)) -[GOOD] (define-fun s37 () Int (ite s30 s2 s31)) -[GOOD] (define-fun s38 () Int (+ s21 s37)) -[GOOD] (define-fun s39 () Int (ite s20 s2 s38)) -[GOOD] (define-fun s40 () Int (+ s10 s39)) -[GOOD] (define-fun s41 () Int (ite s9 s2 s40)) -[GOOD] (define-fun s42 () Int (+ s0 s1)) -[GOOD] (define-fun s43 () Bool (= s41 s42)) +[GOOD] (define-fun s21 () Int (seq.nth s18 s2)) +[GOOD] (define-fun s22 () Int (ite s20 s2 s21)) +[GOOD] (define-fun s23 () Int (+ s16 s22)) +[GOOD] (define-fun s24 () Int (ite s15 s2 s23)) +[GOOD] (define-fun s25 () Int (+ s10 s24)) +[GOOD] (define-fun s26 () Int (ite s9 s2 s25)) +[GOOD] (define-fun s27 () Int (+ s0 s1)) +[GOOD] (define-fun s28 () Bool (= s26 s27)) [GOOD] (assert s3) [GOOD] (assert s4) -[GOOD] (assert s16) -[GOOD] (assert s26) -[GOOD] (assert s36) -[GOOD] (assert s43) +[GOOD] (assert s28) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/listSum.gold b/SBVTestSuite/GoldFiles/listSum.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/listSum.gold +++ /dev/null @@ -1,60 +0,0 @@ -** 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-option :pp.max_depth 4294967295) -[GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) -[GOOD] ; --- uninterpreted sorts --- -[GOOD] ; --- tuples --- -[GOOD] ; --- sums --- -[GOOD] (declare-datatypes ((SBVSum2 2)) ( - (par (X Y) ( (left (getLeft X)) (right (getRight Y)) )) - )) -[GOOD] ; --- literal constants --- -[GOOD] (define-fun s2 () Int 2) -[GOOD] (define-fun s6 () Int 0) -[GOOD] (define-fun s9 () Int 1) -[GOOD] ; --- skolem constants --- -[GOOD] (declare-fun s0 () (Seq (SBVSum2 Int (_ BitVec 8)))) ; tracks user variable "x" -[GOOD] (declare-fun s4 () (SBVSum2 Int (_ BitVec 8))) ; tracks user variable "__internal_sbv_s4" -[GOOD] (declare-fun s15 () (SBVSum2 Int (_ BitVec 8))) ; tracks user variable "__internal_sbv_s15" -[GOOD] ; --- constant tables --- -[GOOD] ; --- skolemized tables --- -[GOOD] ; --- arrays --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user given axioms --- -[GOOD] ; --- formula --- -[GOOD] (define-fun s1 () Int (seq.len s0)) -[GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s5 () (Seq (SBVSum2 Int (_ BitVec 8))) (seq.unit s4)) -[GOOD] (define-fun s7 () Bool (> s1 s6)) -[GOOD] (define-fun s8 () Bool (not s7)) -[GOOD] (define-fun s10 () (Seq (SBVSum2 Int (_ BitVec 8))) (seq.extract s0 s6 s9)) -[GOOD] (define-fun s11 () Bool (= s5 s10)) -[GOOD] (define-fun s12 () Bool (or s8 s11)) -[GOOD] (define-fun s13 () Bool ((_ is left) s4)) -[GOOD] (define-fun s14 () Bool (ite s13 true false)) -[GOOD] (define-fun s16 () (Seq (SBVSum2 Int (_ BitVec 8))) (seq.unit s15)) -[GOOD] (define-fun s17 () Int (- s1 s9)) -[GOOD] (define-fun s18 () (Seq (SBVSum2 Int (_ BitVec 8))) (seq.extract s0 s9 s17)) -[GOOD] (define-fun s19 () Int (seq.len s18)) -[GOOD] (define-fun s20 () Bool (> s19 s6)) -[GOOD] (define-fun s21 () Bool (not s20)) -[GOOD] (define-fun s22 () (Seq (SBVSum2 Int (_ BitVec 8))) (seq.extract s18 s6 s9)) -[GOOD] (define-fun s23 () Bool (= s16 s22)) -[GOOD] (define-fun s24 () Bool (or s21 s23)) -[GOOD] (define-fun s25 () Bool ((_ is left) s15)) -[GOOD] (define-fun s26 () Bool (ite s25 false true)) -[GOOD] (assert s3) -[GOOD] (assert s12) -[GOOD] (assert s14) -[GOOD] (assert s24) -[GOOD] (assert s26) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/makePair.gold b/SBVTestSuite/GoldFiles/makePair.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/makePair.gold +++ /dev/null @@ -1,35 +0,0 @@ -** 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 ALL) ; has unbounded values, using catch-all. -[GOOD] ; --- uninterpreted sorts --- -[GOOD] ; --- tuples --- -[GOOD] (declare-datatypes (T1 T2) ((tup-2 (mk-tup-2 (proj-1 T1) (proj-2 T2))))) -[GOOD] ; --- sums --- -[GOOD] ; --- literal constants --- -[GOOD] (define-fun s_2 () Bool false) -[GOOD] (define-fun s_1 () Bool true) -[GOOD] (define-fun s6 () Int 0) -[GOOD] ; --- skolem constants --- -[GOOD] (declare-fun s0 () Int) ; tracks user variable "x" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "y" -[GOOD] ; --- constant tables --- -[GOOD] ; --- skolemized tables --- -[GOOD] ; --- arrays --- -[GOOD] ; --- uninterpreted constants --- -[GOOD] ; --- user given axioms --- -[GOOD] ; --- formula --- -[GOOD] (define-fun s2 () (tup-2 Int Int) (mk-tup-2 s0 s1)) -[GOOD] (define-fun s3 () Int (proj-1 s2)) -[GOOD] (define-fun s4 () Int (proj-2 s2)) -[GOOD] (define-fun s5 () Int (+ s3 s4)) -[GOOD] (define-fun s7 () Bool (= s5 s6)) -[GOOD] (assert s7) -[SEND] (check-sat) -[RECV] sat -*** Solver : Z3 -*** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/mapNoFailure.gold b/SBVTestSuite/GoldFiles/mapNoFailure.gold --- a/SBVTestSuite/GoldFiles/mapNoFailure.gold +++ b/SBVTestSuite/GoldFiles/mapNoFailure.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -15,21 +15,11 @@ [GOOD] (define-fun s5 () Int 6) [GOOD] (define-fun s7 () Int 0) [GOOD] (define-fun s20 () Int 1) -[GOOD] (define-fun s64 () Int 10) +[GOOD] (define-fun s59 () Int 10) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] (declare-fun s57 () Int) ; tracks user variable "__internal_sbv_s57" -[GOOD] (declare-fun s69 () Int) ; tracks user variable "__internal_sbv_s69" -[GOOD] (declare-fun s81 () Int) ; tracks user variable "__internal_sbv_s81" -[GOOD] (declare-fun s93 () Int) ; tracks user variable "__internal_sbv_s93" -[GOOD] (declare-fun s105 () Int) ; tracks user variable "__internal_sbv_s105" -[GOOD] (declare-fun s117 () Int) ; tracks user variable "__internal_sbv_s117" -[GOOD] (declare-fun s129 () Int) ; tracks user variable "__internal_sbv_s129" -[GOOD] (declare-fun s141 () Int) ; tracks user variable "__internal_sbv_s141" -[GOOD] (declare-fun s153 () Int) ; tracks user variable "__internal_sbv_s153" -[GOOD] (declare-fun s165 () Int) ; tracks user variable "__internal_sbv_s165" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -87,128 +77,78 @@ [GOOD] (define-fun s54 () (Seq Int) (seq.extract s50 s20 s53)) [GOOD] (define-fun s55 () Int (seq.len s54)) [GOOD] (define-fun s56 () Bool (= s7 s55)) -[GOOD] (define-fun s58 () (Seq Int) (seq.unit s57)) -[GOOD] (define-fun s59 () (Seq Int) (seq.extract s54 s7 s20)) -[GOOD] (define-fun s60 () Bool (= s58 s59)) -[GOOD] (define-fun s61 () Bool (<= s55 s7)) -[GOOD] (define-fun s62 () Bool (or s60 s61)) -[GOOD] (define-fun s63 () Bool (< s57 s7)) -[GOOD] (define-fun s65 () Bool (> s57 s64)) -[GOOD] (define-fun s66 () Bool (or s63 s65)) -[GOOD] (define-fun s67 () Bool (not s56)) -[GOOD] (define-fun s68 () Bool (and s66 s67)) -[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) -[GOOD] (define-fun s71 () (Seq Int) (seq.extract s50 s7 s20)) -[GOOD] (define-fun s72 () Bool (= s70 s71)) -[GOOD] (define-fun s73 () Bool (<= s51 s7)) +[GOOD] (define-fun s57 () Int (seq.nth s54 s7)) +[GOOD] (define-fun s58 () Bool (< s57 s7)) +[GOOD] (define-fun s60 () Bool (> s57 s59)) +[GOOD] (define-fun s61 () Bool (or s58 s60)) +[GOOD] (define-fun s62 () Bool (not s56)) +[GOOD] (define-fun s63 () Bool (and s61 s62)) +[GOOD] (define-fun s64 () Int (seq.nth s50 s7)) +[GOOD] (define-fun s65 () Bool (< s64 s7)) +[GOOD] (define-fun s66 () Bool (> s64 s59)) +[GOOD] (define-fun s67 () Bool (or s65 s66)) +[GOOD] (define-fun s68 () Bool (or s63 s67)) +[GOOD] (define-fun s69 () Bool (not s52)) +[GOOD] (define-fun s70 () Bool (and s68 s69)) +[GOOD] (define-fun s71 () Int (seq.nth s46 s7)) +[GOOD] (define-fun s72 () Bool (< s71 s7)) +[GOOD] (define-fun s73 () Bool (> s71 s59)) [GOOD] (define-fun s74 () Bool (or s72 s73)) -[GOOD] (define-fun s75 () Bool (< s69 s7)) -[GOOD] (define-fun s76 () Bool (> s69 s64)) -[GOOD] (define-fun s77 () Bool (or s75 s76)) -[GOOD] (define-fun s78 () Bool (or s68 s77)) -[GOOD] (define-fun s79 () Bool (not s52)) -[GOOD] (define-fun s80 () Bool (and s78 s79)) -[GOOD] (define-fun s82 () (Seq Int) (seq.unit s81)) -[GOOD] (define-fun s83 () (Seq Int) (seq.extract s46 s7 s20)) -[GOOD] (define-fun s84 () Bool (= s82 s83)) -[GOOD] (define-fun s85 () Bool (<= s47 s7)) -[GOOD] (define-fun s86 () Bool (or s84 s85)) -[GOOD] (define-fun s87 () Bool (< s81 s7)) -[GOOD] (define-fun s88 () Bool (> s81 s64)) -[GOOD] (define-fun s89 () Bool (or s87 s88)) -[GOOD] (define-fun s90 () Bool (or s80 s89)) -[GOOD] (define-fun s91 () Bool (not s48)) -[GOOD] (define-fun s92 () Bool (and s90 s91)) -[GOOD] (define-fun s94 () (Seq Int) (seq.unit s93)) -[GOOD] (define-fun s95 () (Seq Int) (seq.extract s42 s7 s20)) -[GOOD] (define-fun s96 () Bool (= s94 s95)) -[GOOD] (define-fun s97 () Bool (<= s43 s7)) -[GOOD] (define-fun s98 () Bool (or s96 s97)) -[GOOD] (define-fun s99 () Bool (< s93 s7)) -[GOOD] (define-fun s100 () Bool (> s93 s64)) -[GOOD] (define-fun s101 () Bool (or s99 s100)) -[GOOD] (define-fun s102 () Bool (or s92 s101)) -[GOOD] (define-fun s103 () Bool (not s44)) -[GOOD] (define-fun s104 () Bool (and s102 s103)) -[GOOD] (define-fun s106 () (Seq Int) (seq.unit s105)) -[GOOD] (define-fun s107 () (Seq Int) (seq.extract s38 s7 s20)) -[GOOD] (define-fun s108 () Bool (= s106 s107)) -[GOOD] (define-fun s109 () Bool (<= s39 s7)) -[GOOD] (define-fun s110 () Bool (or s108 s109)) -[GOOD] (define-fun s111 () Bool (< s105 s7)) -[GOOD] (define-fun s112 () Bool (> s105 s64)) -[GOOD] (define-fun s113 () Bool (or s111 s112)) -[GOOD] (define-fun s114 () Bool (or s104 s113)) -[GOOD] (define-fun s115 () Bool (not s40)) -[GOOD] (define-fun s116 () Bool (and s114 s115)) -[GOOD] (define-fun s118 () (Seq Int) (seq.unit s117)) -[GOOD] (define-fun s119 () (Seq Int) (seq.extract s34 s7 s20)) -[GOOD] (define-fun s120 () Bool (= s118 s119)) -[GOOD] (define-fun s121 () Bool (<= s35 s7)) -[GOOD] (define-fun s122 () Bool (or s120 s121)) -[GOOD] (define-fun s123 () Bool (< s117 s7)) -[GOOD] (define-fun s124 () Bool (> s117 s64)) -[GOOD] (define-fun s125 () Bool (or s123 s124)) -[GOOD] (define-fun s126 () Bool (or s116 s125)) -[GOOD] (define-fun s127 () Bool (not s36)) -[GOOD] (define-fun s128 () Bool (and s126 s127)) -[GOOD] (define-fun s130 () (Seq Int) (seq.unit s129)) -[GOOD] (define-fun s131 () (Seq Int) (seq.extract s30 s7 s20)) -[GOOD] (define-fun s132 () Bool (= s130 s131)) -[GOOD] (define-fun s133 () Bool (<= s31 s7)) -[GOOD] (define-fun s134 () Bool (or s132 s133)) -[GOOD] (define-fun s135 () Bool (< s129 s7)) -[GOOD] (define-fun s136 () Bool (> s129 s64)) -[GOOD] (define-fun s137 () Bool (or s135 s136)) -[GOOD] (define-fun s138 () Bool (or s128 s137)) -[GOOD] (define-fun s139 () Bool (not s32)) -[GOOD] (define-fun s140 () Bool (and s138 s139)) -[GOOD] (define-fun s142 () (Seq Int) (seq.unit s141)) -[GOOD] (define-fun s143 () (Seq Int) (seq.extract s26 s7 s20)) -[GOOD] (define-fun s144 () Bool (= s142 s143)) -[GOOD] (define-fun s145 () Bool (<= s27 s7)) -[GOOD] (define-fun s146 () Bool (or s144 s145)) -[GOOD] (define-fun s147 () Bool (< s141 s7)) -[GOOD] (define-fun s148 () Bool (> s141 s64)) -[GOOD] (define-fun s149 () Bool (or s147 s148)) -[GOOD] (define-fun s150 () Bool (or s140 s149)) -[GOOD] (define-fun s151 () Bool (not s28)) -[GOOD] (define-fun s152 () Bool (and s150 s151)) -[GOOD] (define-fun s154 () (Seq Int) (seq.unit s153)) -[GOOD] (define-fun s155 () (Seq Int) (seq.extract s22 s7 s20)) -[GOOD] (define-fun s156 () Bool (= s154 s155)) -[GOOD] (define-fun s157 () Bool (<= s23 s7)) -[GOOD] (define-fun s158 () Bool (or s156 s157)) -[GOOD] (define-fun s159 () Bool (< s153 s7)) -[GOOD] (define-fun s160 () Bool (> s153 s64)) -[GOOD] (define-fun s161 () Bool (or s159 s160)) -[GOOD] (define-fun s162 () Bool (or s152 s161)) -[GOOD] (define-fun s163 () Bool (not s24)) -[GOOD] (define-fun s164 () Bool (and s162 s163)) -[GOOD] (define-fun s166 () (Seq Int) (seq.unit s165)) -[GOOD] (define-fun s167 () (Seq Int) (seq.extract s17 s7 s20)) -[GOOD] (define-fun s168 () Bool (= s166 s167)) -[GOOD] (define-fun s169 () Bool (<= s18 s7)) -[GOOD] (define-fun s170 () Bool (or s168 s169)) -[GOOD] (define-fun s171 () Bool (< s165 s7)) -[GOOD] (define-fun s172 () Bool (> s165 s64)) -[GOOD] (define-fun s173 () Bool (or s171 s172)) -[GOOD] (define-fun s174 () Bool (or s164 s173)) -[GOOD] (define-fun s175 () Bool (not s19)) -[GOOD] (define-fun s176 () Bool (and s174 s175)) +[GOOD] (define-fun s75 () Bool (or s70 s74)) +[GOOD] (define-fun s76 () Bool (not s48)) +[GOOD] (define-fun s77 () Bool (and s75 s76)) +[GOOD] (define-fun s78 () Int (seq.nth s42 s7)) +[GOOD] (define-fun s79 () Bool (< s78 s7)) +[GOOD] (define-fun s80 () Bool (> s78 s59)) +[GOOD] (define-fun s81 () Bool (or s79 s80)) +[GOOD] (define-fun s82 () Bool (or s77 s81)) +[GOOD] (define-fun s83 () Bool (not s44)) +[GOOD] (define-fun s84 () Bool (and s82 s83)) +[GOOD] (define-fun s85 () Int (seq.nth s38 s7)) +[GOOD] (define-fun s86 () Bool (< s85 s7)) +[GOOD] (define-fun s87 () Bool (> s85 s59)) +[GOOD] (define-fun s88 () Bool (or s86 s87)) +[GOOD] (define-fun s89 () Bool (or s84 s88)) +[GOOD] (define-fun s90 () Bool (not s40)) +[GOOD] (define-fun s91 () Bool (and s89 s90)) +[GOOD] (define-fun s92 () Int (seq.nth s34 s7)) +[GOOD] (define-fun s93 () Bool (< s92 s7)) +[GOOD] (define-fun s94 () Bool (> s92 s59)) +[GOOD] (define-fun s95 () Bool (or s93 s94)) +[GOOD] (define-fun s96 () Bool (or s91 s95)) +[GOOD] (define-fun s97 () Bool (not s36)) +[GOOD] (define-fun s98 () Bool (and s96 s97)) +[GOOD] (define-fun s99 () Int (seq.nth s30 s7)) +[GOOD] (define-fun s100 () Bool (< s99 s7)) +[GOOD] (define-fun s101 () Bool (> s99 s59)) +[GOOD] (define-fun s102 () Bool (or s100 s101)) +[GOOD] (define-fun s103 () Bool (or s98 s102)) +[GOOD] (define-fun s104 () Bool (not s32)) +[GOOD] (define-fun s105 () Bool (and s103 s104)) +[GOOD] (define-fun s106 () Int (seq.nth s26 s7)) +[GOOD] (define-fun s107 () Bool (< s106 s7)) +[GOOD] (define-fun s108 () Bool (> s106 s59)) +[GOOD] (define-fun s109 () Bool (or s107 s108)) +[GOOD] (define-fun s110 () Bool (or s105 s109)) +[GOOD] (define-fun s111 () Bool (not s28)) +[GOOD] (define-fun s112 () Bool (and s110 s111)) +[GOOD] (define-fun s113 () Int (seq.nth s22 s7)) +[GOOD] (define-fun s114 () Bool (< s113 s7)) +[GOOD] (define-fun s115 () Bool (> s113 s59)) +[GOOD] (define-fun s116 () Bool (or s114 s115)) +[GOOD] (define-fun s117 () Bool (or s112 s116)) +[GOOD] (define-fun s118 () Bool (not s24)) +[GOOD] (define-fun s119 () Bool (and s117 s118)) +[GOOD] (define-fun s120 () Int (seq.nth s17 s7)) +[GOOD] (define-fun s121 () Bool (< s120 s7)) +[GOOD] (define-fun s122 () Bool (> s120 s59)) +[GOOD] (define-fun s123 () Bool (or s121 s122)) +[GOOD] (define-fun s124 () Bool (or s119 s123)) +[GOOD] (define-fun s125 () Bool (not s19)) +[GOOD] (define-fun s126 () Bool (and s124 s125)) [GOOD] (assert s6) [GOOD] (assert s12) -[GOOD] (assert s62) -[GOOD] (assert s74) -[GOOD] (assert s86) -[GOOD] (assert s98) -[GOOD] (assert s110) -[GOOD] (assert s122) -[GOOD] (assert s134) -[GOOD] (assert s146) -[GOOD] (assert s158) -[GOOD] (assert s170) -[GOOD] (assert s176) +[GOOD] (assert s126) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/mapWithFailure.gold b/SBVTestSuite/GoldFiles/mapWithFailure.gold --- a/SBVTestSuite/GoldFiles/mapWithFailure.gold +++ b/SBVTestSuite/GoldFiles/mapWithFailure.gold @@ -7,243 +7,176 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- -[GOOD] (define-fun s4 () Int 0) -[GOOD] (define-fun s9 () Int 1) -[GOOD] (define-fun s143 () Int 2) -[GOOD] (define-fun s149 () Int 11) -[GOOD] (define-fun s153 () Int 10) -[GOOD] (define-fun s6 () (Seq Int) (as seq.empty (Seq Int))) +[GOOD] (define-fun s2 () Int 0) +[GOOD] (define-fun s6 () Int 1) +[GOOD] (define-fun s91 () Int 2) +[GOOD] (define-fun s93 () Int 11) +[GOOD] (define-fun s97 () Int 10) +[GOOD] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" -[GOOD] (declare-fun s1 () Int) ; tracks user variable "__internal_sbv_s1" -[GOOD] (declare-fun s7 () Int) ; tracks user variable "__internal_sbv_s7" -[GOOD] (declare-fun s20 () Int) ; tracks user variable "__internal_sbv_s20" -[GOOD] (declare-fun s32 () Int) ; tracks user variable "__internal_sbv_s32" -[GOOD] (declare-fun s44 () Int) ; tracks user variable "__internal_sbv_s44" -[GOOD] (declare-fun s56 () Int) ; tracks user variable "__internal_sbv_s56" -[GOOD] (declare-fun s68 () Int) ; tracks user variable "__internal_sbv_s68" -[GOOD] (declare-fun s80 () Int) ; tracks user variable "__internal_sbv_s80" -[GOOD] (declare-fun s92 () Int) ; tracks user variable "__internal_sbv_s92" -[GOOD] (declare-fun s104 () Int) ; tracks user variable "__internal_sbv_s104" -[GOOD] (declare-fun s116 () Int) ; tracks user variable "__internal_sbv_s116" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- -[GOOD] (define-fun s2 () (Seq Int) (seq.unit s1)) -[GOOD] (define-fun s3 () Int (seq.len s0)) -[GOOD] (define-fun s5 () Bool (= s3 s4)) +[GOOD] (define-fun s1 () Int (seq.len s0)) +[GOOD] (define-fun s3 () Bool (= s1 s2)) +[GOOD] (define-fun s5 () Int (seq.nth s0 s2)) +[GOOD] (define-fun s7 () Int (+ s5 s6)) [GOOD] (define-fun s8 () (Seq Int) (seq.unit s7)) -[GOOD] (define-fun s10 () (Seq Int) (seq.extract s0 s4 s9)) -[GOOD] (define-fun s11 () Bool (= s8 s10)) -[GOOD] (define-fun s12 () Bool (<= s3 s4)) -[GOOD] (define-fun s13 () Bool (or s11 s12)) -[GOOD] (define-fun s14 () Int (+ s7 s9)) +[GOOD] (define-fun s9 () Int (- s1 s6)) +[GOOD] (define-fun s10 () (Seq Int) (seq.extract s0 s6 s9)) +[GOOD] (define-fun s11 () Int (seq.len s10)) +[GOOD] (define-fun s12 () Bool (= s2 s11)) +[GOOD] (define-fun s13 () Int (seq.nth s10 s2)) +[GOOD] (define-fun s14 () Int (+ s6 s13)) [GOOD] (define-fun s15 () (Seq Int) (seq.unit s14)) -[GOOD] (define-fun s16 () Int (- s3 s9)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s0 s9 s16)) +[GOOD] (define-fun s16 () Int (- s11 s6)) +[GOOD] (define-fun s17 () (Seq Int) (seq.extract s10 s6 s16)) [GOOD] (define-fun s18 () Int (seq.len s17)) -[GOOD] (define-fun s19 () Bool (= s4 s18)) -[GOOD] (define-fun s21 () (Seq Int) (seq.unit s20)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s4 s9)) -[GOOD] (define-fun s23 () Bool (= s21 s22)) -[GOOD] (define-fun s24 () Bool (<= s18 s4)) -[GOOD] (define-fun s25 () Bool (or s23 s24)) -[GOOD] (define-fun s26 () Int (+ s9 s20)) -[GOOD] (define-fun s27 () (Seq Int) (seq.unit s26)) -[GOOD] (define-fun s28 () Int (- s18 s9)) -[GOOD] (define-fun s29 () (Seq Int) (seq.extract s17 s9 s28)) -[GOOD] (define-fun s30 () Int (seq.len s29)) -[GOOD] (define-fun s31 () Bool (= s4 s30)) -[GOOD] (define-fun s33 () (Seq Int) (seq.unit s32)) -[GOOD] (define-fun s34 () (Seq Int) (seq.extract s29 s4 s9)) -[GOOD] (define-fun s35 () Bool (= s33 s34)) -[GOOD] (define-fun s36 () Bool (<= s30 s4)) -[GOOD] (define-fun s37 () Bool (or s35 s36)) -[GOOD] (define-fun s38 () Int (+ s9 s32)) -[GOOD] (define-fun s39 () (Seq Int) (seq.unit s38)) -[GOOD] (define-fun s40 () Int (- s30 s9)) -[GOOD] (define-fun s41 () (Seq Int) (seq.extract s29 s9 s40)) -[GOOD] (define-fun s42 () Int (seq.len s41)) -[GOOD] (define-fun s43 () Bool (= s4 s42)) -[GOOD] (define-fun s45 () (Seq Int) (seq.unit s44)) -[GOOD] (define-fun s46 () (Seq Int) (seq.extract s41 s4 s9)) -[GOOD] (define-fun s47 () Bool (= s45 s46)) -[GOOD] (define-fun s48 () Bool (<= s42 s4)) -[GOOD] (define-fun s49 () Bool (or s47 s48)) -[GOOD] (define-fun s50 () Int (+ s9 s44)) -[GOOD] (define-fun s51 () (Seq Int) (seq.unit s50)) -[GOOD] (define-fun s52 () Int (- s42 s9)) -[GOOD] (define-fun s53 () (Seq Int) (seq.extract s41 s9 s52)) -[GOOD] (define-fun s54 () Int (seq.len s53)) -[GOOD] (define-fun s55 () Bool (= s4 s54)) +[GOOD] (define-fun s19 () Bool (= s2 s18)) +[GOOD] (define-fun s20 () Int (seq.nth s17 s2)) +[GOOD] (define-fun s21 () Int (+ s6 s20)) +[GOOD] (define-fun s22 () (Seq Int) (seq.unit s21)) +[GOOD] (define-fun s23 () Int (- s18 s6)) +[GOOD] (define-fun s24 () (Seq Int) (seq.extract s17 s6 s23)) +[GOOD] (define-fun s25 () Int (seq.len s24)) +[GOOD] (define-fun s26 () Bool (= s2 s25)) +[GOOD] (define-fun s27 () Int (seq.nth s24 s2)) +[GOOD] (define-fun s28 () Int (+ s6 s27)) +[GOOD] (define-fun s29 () (Seq Int) (seq.unit s28)) +[GOOD] (define-fun s30 () Int (- s25 s6)) +[GOOD] (define-fun s31 () (Seq Int) (seq.extract s24 s6 s30)) +[GOOD] (define-fun s32 () Int (seq.len s31)) +[GOOD] (define-fun s33 () Bool (= s2 s32)) +[GOOD] (define-fun s34 () Int (seq.nth s31 s2)) +[GOOD] (define-fun s35 () Int (+ s6 s34)) +[GOOD] (define-fun s36 () (Seq Int) (seq.unit s35)) +[GOOD] (define-fun s37 () Int (- s32 s6)) +[GOOD] (define-fun s38 () (Seq Int) (seq.extract s31 s6 s37)) +[GOOD] (define-fun s39 () Int (seq.len s38)) +[GOOD] (define-fun s40 () Bool (= s2 s39)) +[GOOD] (define-fun s41 () Int (seq.nth s38 s2)) +[GOOD] (define-fun s42 () Int (+ s6 s41)) +[GOOD] (define-fun s43 () (Seq Int) (seq.unit s42)) +[GOOD] (define-fun s44 () Int (- s39 s6)) +[GOOD] (define-fun s45 () (Seq Int) (seq.extract s38 s6 s44)) +[GOOD] (define-fun s46 () Int (seq.len s45)) +[GOOD] (define-fun s47 () Bool (= s2 s46)) +[GOOD] (define-fun s48 () Int (seq.nth s45 s2)) +[GOOD] (define-fun s49 () Int (+ s6 s48)) +[GOOD] (define-fun s50 () (Seq Int) (seq.unit s49)) +[GOOD] (define-fun s51 () Int (- s46 s6)) +[GOOD] (define-fun s52 () (Seq Int) (seq.extract s45 s6 s51)) +[GOOD] (define-fun s53 () Int (seq.len s52)) +[GOOD] (define-fun s54 () Bool (= s2 s53)) +[GOOD] (define-fun s55 () Int (seq.nth s52 s2)) +[GOOD] (define-fun s56 () Int (+ s6 s55)) [GOOD] (define-fun s57 () (Seq Int) (seq.unit s56)) -[GOOD] (define-fun s58 () (Seq Int) (seq.extract s53 s4 s9)) -[GOOD] (define-fun s59 () Bool (= s57 s58)) -[GOOD] (define-fun s60 () Bool (<= s54 s4)) -[GOOD] (define-fun s61 () Bool (or s59 s60)) -[GOOD] (define-fun s62 () Int (+ s9 s56)) -[GOOD] (define-fun s63 () (Seq Int) (seq.unit s62)) -[GOOD] (define-fun s64 () Int (- s54 s9)) -[GOOD] (define-fun s65 () (Seq Int) (seq.extract s53 s9 s64)) -[GOOD] (define-fun s66 () Int (seq.len s65)) -[GOOD] (define-fun s67 () Bool (= s4 s66)) -[GOOD] (define-fun s69 () (Seq Int) (seq.unit s68)) -[GOOD] (define-fun s70 () (Seq Int) (seq.extract s65 s4 s9)) -[GOOD] (define-fun s71 () Bool (= s69 s70)) -[GOOD] (define-fun s72 () Bool (<= s66 s4)) -[GOOD] (define-fun s73 () Bool (or s71 s72)) -[GOOD] (define-fun s74 () Int (+ s9 s68)) -[GOOD] (define-fun s75 () (Seq Int) (seq.unit s74)) -[GOOD] (define-fun s76 () Int (- s66 s9)) -[GOOD] (define-fun s77 () (Seq Int) (seq.extract s65 s9 s76)) -[GOOD] (define-fun s78 () Int (seq.len s77)) -[GOOD] (define-fun s79 () Bool (= s4 s78)) -[GOOD] (define-fun s81 () (Seq Int) (seq.unit s80)) -[GOOD] (define-fun s82 () (Seq Int) (seq.extract s77 s4 s9)) -[GOOD] (define-fun s83 () Bool (= s81 s82)) -[GOOD] (define-fun s84 () Bool (<= s78 s4)) -[GOOD] (define-fun s85 () Bool (or s83 s84)) -[GOOD] (define-fun s86 () Int (+ s9 s80)) -[GOOD] (define-fun s87 () (Seq Int) (seq.unit s86)) -[GOOD] (define-fun s88 () Int (- s78 s9)) -[GOOD] (define-fun s89 () (Seq Int) (seq.extract s77 s9 s88)) -[GOOD] (define-fun s90 () Int (seq.len s89)) -[GOOD] (define-fun s91 () Bool (= s4 s90)) -[GOOD] (define-fun s93 () (Seq Int) (seq.unit s92)) -[GOOD] (define-fun s94 () (Seq Int) (seq.extract s89 s4 s9)) -[GOOD] (define-fun s95 () Bool (= s93 s94)) -[GOOD] (define-fun s96 () Bool (<= s90 s4)) -[GOOD] (define-fun s97 () Bool (or s95 s96)) -[GOOD] (define-fun s98 () Int (+ s9 s92)) -[GOOD] (define-fun s99 () (Seq Int) (seq.unit s98)) -[GOOD] (define-fun s100 () Int (- s90 s9)) -[GOOD] (define-fun s101 () (Seq Int) (seq.extract s89 s9 s100)) -[GOOD] (define-fun s102 () Int (seq.len s101)) -[GOOD] (define-fun s103 () Bool (= s4 s102)) -[GOOD] (define-fun s105 () (Seq Int) (seq.unit s104)) -[GOOD] (define-fun s106 () (Seq Int) (seq.extract s101 s4 s9)) -[GOOD] (define-fun s107 () Bool (= s105 s106)) -[GOOD] (define-fun s108 () Bool (<= s102 s4)) -[GOOD] (define-fun s109 () Bool (or s107 s108)) -[GOOD] (define-fun s110 () Int (+ s9 s104)) -[GOOD] (define-fun s111 () (Seq Int) (seq.unit s110)) -[GOOD] (define-fun s112 () Int (- s102 s9)) -[GOOD] (define-fun s113 () (Seq Int) (seq.extract s101 s9 s112)) -[GOOD] (define-fun s114 () Int (seq.len s113)) -[GOOD] (define-fun s115 () Bool (= s4 s114)) -[GOOD] (define-fun s117 () (Seq Int) (seq.unit s116)) -[GOOD] (define-fun s118 () (Seq Int) (seq.extract s113 s4 s9)) -[GOOD] (define-fun s119 () Bool (= s117 s118)) -[GOOD] (define-fun s120 () Bool (<= s114 s4)) -[GOOD] (define-fun s121 () Bool (or s119 s120)) -[GOOD] (define-fun s122 () Int (+ s9 s116)) -[GOOD] (define-fun s123 () (Seq Int) (seq.unit s122)) -[GOOD] (define-fun s124 () (Seq Int) (ite s115 s6 s123)) -[GOOD] (define-fun s125 () (Seq Int) (seq.++ s111 s124)) -[GOOD] (define-fun s126 () (Seq Int) (ite s103 s6 s125)) -[GOOD] (define-fun s127 () (Seq Int) (seq.++ s99 s126)) -[GOOD] (define-fun s128 () (Seq Int) (ite s91 s6 s127)) -[GOOD] (define-fun s129 () (Seq Int) (seq.++ s87 s128)) -[GOOD] (define-fun s130 () (Seq Int) (ite s79 s6 s129)) -[GOOD] (define-fun s131 () (Seq Int) (seq.++ s75 s130)) -[GOOD] (define-fun s132 () (Seq Int) (ite s67 s6 s131)) -[GOOD] (define-fun s133 () (Seq Int) (seq.++ s63 s132)) -[GOOD] (define-fun s134 () (Seq Int) (ite s55 s6 s133)) -[GOOD] (define-fun s135 () (Seq Int) (seq.++ s51 s134)) -[GOOD] (define-fun s136 () (Seq Int) (ite s43 s6 s135)) -[GOOD] (define-fun s137 () (Seq Int) (seq.++ s39 s136)) -[GOOD] (define-fun s138 () (Seq Int) (ite s31 s6 s137)) -[GOOD] (define-fun s139 () (Seq Int) (seq.++ s27 s138)) -[GOOD] (define-fun s140 () (Seq Int) (ite s19 s6 s139)) -[GOOD] (define-fun s141 () (Seq Int) (seq.++ s15 s140)) -[GOOD] (define-fun s142 () (Seq Int) (ite s5 s6 s141)) -[GOOD] (define-fun s144 () (Seq Int) (seq.extract s142 s143 s9)) -[GOOD] (define-fun s145 () Bool (= s2 s144)) -[GOOD] (define-fun s146 () Int (seq.len s142)) -[GOOD] (define-fun s147 () Bool (<= s146 s143)) -[GOOD] (define-fun s148 () Bool (or s145 s147)) -[GOOD] (define-fun s150 () Bool (> s1 s149)) -[GOOD] (define-fun s151 () Bool (not s150)) -[GOOD] (define-fun s152 () Bool (< s116 s4)) -[GOOD] (define-fun s154 () Bool (> s116 s153)) -[GOOD] (define-fun s155 () Bool (or s152 s154)) -[GOOD] (define-fun s156 () Bool (not s115)) -[GOOD] (define-fun s157 () Bool (and s155 s156)) -[GOOD] (define-fun s158 () Bool (< s104 s4)) -[GOOD] (define-fun s159 () Bool (> s104 s153)) -[GOOD] (define-fun s160 () Bool (or s158 s159)) -[GOOD] (define-fun s161 () Bool (or s157 s160)) -[GOOD] (define-fun s162 () Bool (not s103)) -[GOOD] (define-fun s163 () Bool (and s161 s162)) -[GOOD] (define-fun s164 () Bool (< s92 s4)) -[GOOD] (define-fun s165 () Bool (> s92 s153)) -[GOOD] (define-fun s166 () Bool (or s164 s165)) -[GOOD] (define-fun s167 () Bool (or s163 s166)) -[GOOD] (define-fun s168 () Bool (not s91)) -[GOOD] (define-fun s169 () Bool (and s167 s168)) -[GOOD] (define-fun s170 () Bool (< s80 s4)) -[GOOD] (define-fun s171 () Bool (> s80 s153)) -[GOOD] (define-fun s172 () Bool (or s170 s171)) -[GOOD] (define-fun s173 () Bool (or s169 s172)) -[GOOD] (define-fun s174 () Bool (not s79)) -[GOOD] (define-fun s175 () Bool (and s173 s174)) -[GOOD] (define-fun s176 () Bool (< s68 s4)) -[GOOD] (define-fun s177 () Bool (> s68 s153)) -[GOOD] (define-fun s178 () Bool (or s176 s177)) -[GOOD] (define-fun s179 () Bool (or s175 s178)) -[GOOD] (define-fun s180 () Bool (not s67)) -[GOOD] (define-fun s181 () Bool (and s179 s180)) -[GOOD] (define-fun s182 () Bool (< s56 s4)) -[GOOD] (define-fun s183 () Bool (> s56 s153)) -[GOOD] (define-fun s184 () Bool (or s182 s183)) -[GOOD] (define-fun s185 () Bool (or s181 s184)) -[GOOD] (define-fun s186 () Bool (not s55)) -[GOOD] (define-fun s187 () Bool (and s185 s186)) -[GOOD] (define-fun s188 () Bool (< s44 s4)) -[GOOD] (define-fun s189 () Bool (> s44 s153)) -[GOOD] (define-fun s190 () Bool (or s188 s189)) -[GOOD] (define-fun s191 () Bool (or s187 s190)) -[GOOD] (define-fun s192 () Bool (not s43)) -[GOOD] (define-fun s193 () Bool (and s191 s192)) -[GOOD] (define-fun s194 () Bool (< s32 s4)) -[GOOD] (define-fun s195 () Bool (> s32 s153)) -[GOOD] (define-fun s196 () Bool (or s194 s195)) -[GOOD] (define-fun s197 () Bool (or s193 s196)) -[GOOD] (define-fun s198 () Bool (not s31)) -[GOOD] (define-fun s199 () Bool (and s197 s198)) -[GOOD] (define-fun s200 () Bool (< s20 s4)) -[GOOD] (define-fun s201 () Bool (> s20 s153)) -[GOOD] (define-fun s202 () Bool (or s200 s201)) -[GOOD] (define-fun s203 () Bool (or s199 s202)) -[GOOD] (define-fun s204 () Bool (not s19)) -[GOOD] (define-fun s205 () Bool (and s203 s204)) -[GOOD] (define-fun s206 () Bool (< s7 s4)) -[GOOD] (define-fun s207 () Bool (> s7 s153)) -[GOOD] (define-fun s208 () Bool (or s206 s207)) -[GOOD] (define-fun s209 () Bool (or s205 s208)) -[GOOD] (define-fun s210 () Bool (not s5)) -[GOOD] (define-fun s211 () Bool (and s209 s210)) -[GOOD] (define-fun s212 () Bool (or s151 s211)) -[GOOD] (assert s13) -[GOOD] (assert s25) -[GOOD] (assert s37) -[GOOD] (assert s49) -[GOOD] (assert s61) -[GOOD] (assert s73) -[GOOD] (assert s85) -[GOOD] (assert s97) -[GOOD] (assert s109) -[GOOD] (assert s121) -[GOOD] (assert s148) -[GOOD] (assert s212) +[GOOD] (define-fun s58 () Int (- s53 s6)) +[GOOD] (define-fun s59 () (Seq Int) (seq.extract s52 s6 s58)) +[GOOD] (define-fun s60 () Int (seq.len s59)) +[GOOD] (define-fun s61 () Bool (= s2 s60)) +[GOOD] (define-fun s62 () Int (seq.nth s59 s2)) +[GOOD] (define-fun s63 () Int (+ s6 s62)) +[GOOD] (define-fun s64 () (Seq Int) (seq.unit s63)) +[GOOD] (define-fun s65 () Int (- s60 s6)) +[GOOD] (define-fun s66 () (Seq Int) (seq.extract s59 s6 s65)) +[GOOD] (define-fun s67 () Int (seq.len s66)) +[GOOD] (define-fun s68 () Bool (= s2 s67)) +[GOOD] (define-fun s69 () Int (seq.nth s66 s2)) +[GOOD] (define-fun s70 () Int (+ s6 s69)) +[GOOD] (define-fun s71 () (Seq Int) (seq.unit s70)) +[GOOD] (define-fun s72 () (Seq Int) (ite s68 s4 s71)) +[GOOD] (define-fun s73 () (Seq Int) (seq.++ s64 s72)) +[GOOD] (define-fun s74 () (Seq Int) (ite s61 s4 s73)) +[GOOD] (define-fun s75 () (Seq Int) (seq.++ s57 s74)) +[GOOD] (define-fun s76 () (Seq Int) (ite s54 s4 s75)) +[GOOD] (define-fun s77 () (Seq Int) (seq.++ s50 s76)) +[GOOD] (define-fun s78 () (Seq Int) (ite s47 s4 s77)) +[GOOD] (define-fun s79 () (Seq Int) (seq.++ s43 s78)) +[GOOD] (define-fun s80 () (Seq Int) (ite s40 s4 s79)) +[GOOD] (define-fun s81 () (Seq Int) (seq.++ s36 s80)) +[GOOD] (define-fun s82 () (Seq Int) (ite s33 s4 s81)) +[GOOD] (define-fun s83 () (Seq Int) (seq.++ s29 s82)) +[GOOD] (define-fun s84 () (Seq Int) (ite s26 s4 s83)) +[GOOD] (define-fun s85 () (Seq Int) (seq.++ s22 s84)) +[GOOD] (define-fun s86 () (Seq Int) (ite s19 s4 s85)) +[GOOD] (define-fun s87 () (Seq Int) (seq.++ s15 s86)) +[GOOD] (define-fun s88 () (Seq Int) (ite s12 s4 s87)) +[GOOD] (define-fun s89 () (Seq Int) (seq.++ s8 s88)) +[GOOD] (define-fun s90 () (Seq Int) (ite s3 s4 s89)) +[GOOD] (define-fun s92 () Int (seq.nth s90 s91)) +[GOOD] (define-fun s94 () Bool (> s92 s93)) +[GOOD] (define-fun s95 () Bool (not s94)) +[GOOD] (define-fun s96 () Bool (< s69 s2)) +[GOOD] (define-fun s98 () Bool (> s69 s97)) +[GOOD] (define-fun s99 () Bool (or s96 s98)) +[GOOD] (define-fun s100 () Bool (not s68)) +[GOOD] (define-fun s101 () Bool (and s99 s100)) +[GOOD] (define-fun s102 () Bool (< s62 s2)) +[GOOD] (define-fun s103 () Bool (> s62 s97)) +[GOOD] (define-fun s104 () Bool (or s102 s103)) +[GOOD] (define-fun s105 () Bool (or s101 s104)) +[GOOD] (define-fun s106 () Bool (not s61)) +[GOOD] (define-fun s107 () Bool (and s105 s106)) +[GOOD] (define-fun s108 () Bool (< s55 s2)) +[GOOD] (define-fun s109 () Bool (> s55 s97)) +[GOOD] (define-fun s110 () Bool (or s108 s109)) +[GOOD] (define-fun s111 () Bool (or s107 s110)) +[GOOD] (define-fun s112 () Bool (not s54)) +[GOOD] (define-fun s113 () Bool (and s111 s112)) +[GOOD] (define-fun s114 () Bool (< s48 s2)) +[GOOD] (define-fun s115 () Bool (> s48 s97)) +[GOOD] (define-fun s116 () Bool (or s114 s115)) +[GOOD] (define-fun s117 () Bool (or s113 s116)) +[GOOD] (define-fun s118 () Bool (not s47)) +[GOOD] (define-fun s119 () Bool (and s117 s118)) +[GOOD] (define-fun s120 () Bool (< s41 s2)) +[GOOD] (define-fun s121 () Bool (> s41 s97)) +[GOOD] (define-fun s122 () Bool (or s120 s121)) +[GOOD] (define-fun s123 () Bool (or s119 s122)) +[GOOD] (define-fun s124 () Bool (not s40)) +[GOOD] (define-fun s125 () Bool (and s123 s124)) +[GOOD] (define-fun s126 () Bool (< s34 s2)) +[GOOD] (define-fun s127 () Bool (> s34 s97)) +[GOOD] (define-fun s128 () Bool (or s126 s127)) +[GOOD] (define-fun s129 () Bool (or s125 s128)) +[GOOD] (define-fun s130 () Bool (not s33)) +[GOOD] (define-fun s131 () Bool (and s129 s130)) +[GOOD] (define-fun s132 () Bool (< s27 s2)) +[GOOD] (define-fun s133 () Bool (> s27 s97)) +[GOOD] (define-fun s134 () Bool (or s132 s133)) +[GOOD] (define-fun s135 () Bool (or s131 s134)) +[GOOD] (define-fun s136 () Bool (not s26)) +[GOOD] (define-fun s137 () Bool (and s135 s136)) +[GOOD] (define-fun s138 () Bool (< s20 s2)) +[GOOD] (define-fun s139 () Bool (> s20 s97)) +[GOOD] (define-fun s140 () Bool (or s138 s139)) +[GOOD] (define-fun s141 () Bool (or s137 s140)) +[GOOD] (define-fun s142 () Bool (not s19)) +[GOOD] (define-fun s143 () Bool (and s141 s142)) +[GOOD] (define-fun s144 () Bool (< s13 s2)) +[GOOD] (define-fun s145 () Bool (> s13 s97)) +[GOOD] (define-fun s146 () Bool (or s144 s145)) +[GOOD] (define-fun s147 () Bool (or s143 s146)) +[GOOD] (define-fun s148 () Bool (not s12)) +[GOOD] (define-fun s149 () Bool (and s147 s148)) +[GOOD] (define-fun s150 () Bool (< s5 s2)) +[GOOD] (define-fun s151 () Bool (> s5 s97)) +[GOOD] (define-fun s152 () Bool (or s150 s151)) +[GOOD] (define-fun s153 () Bool (or s149 s152)) +[GOOD] (define-fun s154 () Bool (not s3)) +[GOOD] (define-fun s155 () Bool (and s153 s154)) +[GOOD] (define-fun s156 () Bool (or s95 s155)) +[GOOD] (assert s156) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/maxlWithFailure.gold b/SBVTestSuite/GoldFiles/maxlWithFailure.gold --- a/SBVTestSuite/GoldFiles/maxlWithFailure.gold +++ b/SBVTestSuite/GoldFiles/maxlWithFailure.gold @@ -7,26 +7,16 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 0) [GOOD] (define-fun s4 () Int 1) -[GOOD] (define-fun s131 () Int 10) +[GOOD] (define-fun s81 () Int 10) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" -[GOOD] (declare-fun s9 () Int) ; tracks user variable "__internal_sbv_s9" -[GOOD] (declare-fun s21 () Int) ; tracks user variable "__internal_sbv_s21" -[GOOD] (declare-fun s33 () Int) ; tracks user variable "__internal_sbv_s33" -[GOOD] (declare-fun s45 () Int) ; tracks user variable "__internal_sbv_s45" -[GOOD] (declare-fun s57 () Int) ; tracks user variable "__internal_sbv_s57" -[GOOD] (declare-fun s69 () Int) ; tracks user variable "__internal_sbv_s69" -[GOOD] (declare-fun s81 () Int) ; tracks user variable "__internal_sbv_s81" -[GOOD] (declare-fun s93 () Int) ; tracks user variable "__internal_sbv_s93" -[GOOD] (declare-fun s105 () Int) ; tracks user variable "__internal_sbv_s105" -[GOOD] (declare-fun s113 () Int) ; tracks user variable "__internal_sbv_s113" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -39,182 +29,132 @@ [GOOD] (define-fun s6 () (Seq Int) (seq.extract s0 s4 s5)) [GOOD] (define-fun s7 () Int (seq.len s6)) [GOOD] (define-fun s8 () Bool (= s2 s7)) -[GOOD] (define-fun s10 () (Seq Int) (seq.unit s9)) -[GOOD] (define-fun s11 () (Seq Int) (seq.extract s0 s2 s4)) -[GOOD] (define-fun s12 () Bool (= s10 s11)) -[GOOD] (define-fun s13 () Bool (<= s1 s2)) -[GOOD] (define-fun s14 () Bool (or s12 s13)) -[GOOD] (define-fun s15 () Bool (<= s9 s2)) -[GOOD] (define-fun s16 () Int (ite s15 s2 s9)) -[GOOD] (define-fun s17 () Int (- s7 s4)) -[GOOD] (define-fun s18 () (Seq Int) (seq.extract s6 s4 s17)) -[GOOD] (define-fun s19 () Int (seq.len s18)) -[GOOD] (define-fun s20 () Bool (= s2 s19)) -[GOOD] (define-fun s22 () (Seq Int) (seq.unit s21)) -[GOOD] (define-fun s23 () (Seq Int) (seq.extract s6 s2 s4)) -[GOOD] (define-fun s24 () Bool (= s22 s23)) -[GOOD] (define-fun s25 () Bool (<= s7 s2)) -[GOOD] (define-fun s26 () Bool (or s24 s25)) -[GOOD] (define-fun s27 () Bool (<= s21 s16)) -[GOOD] (define-fun s28 () Int (ite s27 s16 s21)) -[GOOD] (define-fun s29 () Int (- s19 s4)) -[GOOD] (define-fun s30 () (Seq Int) (seq.extract s18 s4 s29)) -[GOOD] (define-fun s31 () Int (seq.len s30)) -[GOOD] (define-fun s32 () Bool (= s2 s31)) -[GOOD] (define-fun s34 () (Seq Int) (seq.unit s33)) -[GOOD] (define-fun s35 () (Seq Int) (seq.extract s18 s2 s4)) -[GOOD] (define-fun s36 () Bool (= s34 s35)) -[GOOD] (define-fun s37 () Bool (<= s19 s2)) -[GOOD] (define-fun s38 () Bool (or s36 s37)) -[GOOD] (define-fun s39 () Bool (<= s33 s28)) -[GOOD] (define-fun s40 () Int (ite s39 s28 s33)) -[GOOD] (define-fun s41 () Int (- s31 s4)) -[GOOD] (define-fun s42 () (Seq Int) (seq.extract s30 s4 s41)) -[GOOD] (define-fun s43 () Int (seq.len s42)) -[GOOD] (define-fun s44 () Bool (= s2 s43)) -[GOOD] (define-fun s46 () (Seq Int) (seq.unit s45)) -[GOOD] (define-fun s47 () (Seq Int) (seq.extract s30 s2 s4)) -[GOOD] (define-fun s48 () Bool (= s46 s47)) -[GOOD] (define-fun s49 () Bool (<= s31 s2)) -[GOOD] (define-fun s50 () Bool (or s48 s49)) -[GOOD] (define-fun s51 () Bool (<= s45 s40)) -[GOOD] (define-fun s52 () Int (ite s51 s40 s45)) -[GOOD] (define-fun s53 () Int (- s43 s4)) -[GOOD] (define-fun s54 () (Seq Int) (seq.extract s42 s4 s53)) -[GOOD] (define-fun s55 () Int (seq.len s54)) -[GOOD] (define-fun s56 () Bool (= s2 s55)) -[GOOD] (define-fun s58 () (Seq Int) (seq.unit s57)) -[GOOD] (define-fun s59 () (Seq Int) (seq.extract s42 s2 s4)) -[GOOD] (define-fun s60 () Bool (= s58 s59)) -[GOOD] (define-fun s61 () Bool (<= s43 s2)) -[GOOD] (define-fun s62 () Bool (or s60 s61)) -[GOOD] (define-fun s63 () Bool (<= s57 s52)) -[GOOD] (define-fun s64 () Int (ite s63 s52 s57)) -[GOOD] (define-fun s65 () Int (- s55 s4)) -[GOOD] (define-fun s66 () (Seq Int) (seq.extract s54 s4 s65)) -[GOOD] (define-fun s67 () Int (seq.len s66)) -[GOOD] (define-fun s68 () Bool (= s2 s67)) -[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) -[GOOD] (define-fun s71 () (Seq Int) (seq.extract s54 s2 s4)) -[GOOD] (define-fun s72 () Bool (= s70 s71)) -[GOOD] (define-fun s73 () Bool (<= s55 s2)) -[GOOD] (define-fun s74 () Bool (or s72 s73)) -[GOOD] (define-fun s75 () Bool (<= s69 s64)) -[GOOD] (define-fun s76 () Int (ite s75 s64 s69)) -[GOOD] (define-fun s77 () Int (- s67 s4)) -[GOOD] (define-fun s78 () (Seq Int) (seq.extract s66 s4 s77)) -[GOOD] (define-fun s79 () Int (seq.len s78)) -[GOOD] (define-fun s80 () Bool (= s2 s79)) -[GOOD] (define-fun s82 () (Seq Int) (seq.unit s81)) -[GOOD] (define-fun s83 () (Seq Int) (seq.extract s66 s2 s4)) -[GOOD] (define-fun s84 () Bool (= s82 s83)) -[GOOD] (define-fun s85 () Bool (<= s67 s2)) +[GOOD] (define-fun s9 () Int (seq.nth s0 s2)) +[GOOD] (define-fun s10 () Bool (<= s9 s2)) +[GOOD] (define-fun s11 () Int (ite s10 s2 s9)) +[GOOD] (define-fun s12 () Int (- s7 s4)) +[GOOD] (define-fun s13 () (Seq Int) (seq.extract s6 s4 s12)) +[GOOD] (define-fun s14 () Int (seq.len s13)) +[GOOD] (define-fun s15 () Bool (= s2 s14)) +[GOOD] (define-fun s16 () Int (seq.nth s6 s2)) +[GOOD] (define-fun s17 () Bool (<= s16 s11)) +[GOOD] (define-fun s18 () Int (ite s17 s11 s16)) +[GOOD] (define-fun s19 () Int (- s14 s4)) +[GOOD] (define-fun s20 () (Seq Int) (seq.extract s13 s4 s19)) +[GOOD] (define-fun s21 () Int (seq.len s20)) +[GOOD] (define-fun s22 () Bool (= s2 s21)) +[GOOD] (define-fun s23 () Int (seq.nth s13 s2)) +[GOOD] (define-fun s24 () Bool (<= s23 s18)) +[GOOD] (define-fun s25 () Int (ite s24 s18 s23)) +[GOOD] (define-fun s26 () Int (- s21 s4)) +[GOOD] (define-fun s27 () (Seq Int) (seq.extract s20 s4 s26)) +[GOOD] (define-fun s28 () Int (seq.len s27)) +[GOOD] (define-fun s29 () Bool (= s2 s28)) +[GOOD] (define-fun s30 () Int (seq.nth s20 s2)) +[GOOD] (define-fun s31 () Bool (<= s30 s25)) +[GOOD] (define-fun s32 () Int (ite s31 s25 s30)) +[GOOD] (define-fun s33 () Int (- s28 s4)) +[GOOD] (define-fun s34 () (Seq Int) (seq.extract s27 s4 s33)) +[GOOD] (define-fun s35 () Int (seq.len s34)) +[GOOD] (define-fun s36 () Bool (= s2 s35)) +[GOOD] (define-fun s37 () Int (seq.nth s27 s2)) +[GOOD] (define-fun s38 () Bool (<= s37 s32)) +[GOOD] (define-fun s39 () Int (ite s38 s32 s37)) +[GOOD] (define-fun s40 () Int (- s35 s4)) +[GOOD] (define-fun s41 () (Seq Int) (seq.extract s34 s4 s40)) +[GOOD] (define-fun s42 () Int (seq.len s41)) +[GOOD] (define-fun s43 () Bool (= s2 s42)) +[GOOD] (define-fun s44 () Int (seq.nth s34 s2)) +[GOOD] (define-fun s45 () Bool (<= s44 s39)) +[GOOD] (define-fun s46 () Int (ite s45 s39 s44)) +[GOOD] (define-fun s47 () Int (- s42 s4)) +[GOOD] (define-fun s48 () (Seq Int) (seq.extract s41 s4 s47)) +[GOOD] (define-fun s49 () Int (seq.len s48)) +[GOOD] (define-fun s50 () Bool (= s2 s49)) +[GOOD] (define-fun s51 () Int (seq.nth s41 s2)) +[GOOD] (define-fun s52 () Bool (<= s51 s46)) +[GOOD] (define-fun s53 () Int (ite s52 s46 s51)) +[GOOD] (define-fun s54 () Int (- s49 s4)) +[GOOD] (define-fun s55 () (Seq Int) (seq.extract s48 s4 s54)) +[GOOD] (define-fun s56 () Int (seq.len s55)) +[GOOD] (define-fun s57 () Bool (= s2 s56)) +[GOOD] (define-fun s58 () Int (seq.nth s48 s2)) +[GOOD] (define-fun s59 () Bool (<= s58 s53)) +[GOOD] (define-fun s60 () Int (ite s59 s53 s58)) +[GOOD] (define-fun s61 () Int (- s56 s4)) +[GOOD] (define-fun s62 () (Seq Int) (seq.extract s55 s4 s61)) +[GOOD] (define-fun s63 () Int (seq.len s62)) +[GOOD] (define-fun s64 () Bool (= s2 s63)) +[GOOD] (define-fun s65 () Int (seq.nth s55 s2)) +[GOOD] (define-fun s66 () Bool (<= s65 s60)) +[GOOD] (define-fun s67 () Int (ite s66 s60 s65)) +[GOOD] (define-fun s68 () Int (seq.nth s62 s2)) +[GOOD] (define-fun s69 () Bool (<= s68 s67)) +[GOOD] (define-fun s70 () Int (ite s69 s67 s68)) +[GOOD] (define-fun s71 () Int (ite s64 s67 s70)) +[GOOD] (define-fun s72 () Int (ite s57 s60 s71)) +[GOOD] (define-fun s73 () Int (ite s50 s53 s72)) +[GOOD] (define-fun s74 () Int (ite s43 s46 s73)) +[GOOD] (define-fun s75 () Int (ite s36 s39 s74)) +[GOOD] (define-fun s76 () Int (ite s29 s32 s75)) +[GOOD] (define-fun s77 () Int (ite s22 s25 s76)) +[GOOD] (define-fun s78 () Int (ite s15 s18 s77)) +[GOOD] (define-fun s79 () Int (ite s8 s11 s78)) +[GOOD] (define-fun s80 () Int (ite s3 s2 s79)) +[GOOD] (define-fun s82 () Bool (> s80 s81)) +[GOOD] (define-fun s83 () Bool (not s82)) +[GOOD] (define-fun s84 () Bool (< s9 s2)) +[GOOD] (define-fun s85 () Bool (> s9 s81)) [GOOD] (define-fun s86 () Bool (or s84 s85)) -[GOOD] (define-fun s87 () Bool (<= s81 s76)) -[GOOD] (define-fun s88 () Int (ite s87 s76 s81)) -[GOOD] (define-fun s89 () Int (- s79 s4)) -[GOOD] (define-fun s90 () (Seq Int) (seq.extract s78 s4 s89)) -[GOOD] (define-fun s91 () Int (seq.len s90)) -[GOOD] (define-fun s92 () Bool (= s2 s91)) -[GOOD] (define-fun s94 () (Seq Int) (seq.unit s93)) -[GOOD] (define-fun s95 () (Seq Int) (seq.extract s78 s2 s4)) -[GOOD] (define-fun s96 () Bool (= s94 s95)) -[GOOD] (define-fun s97 () Bool (<= s79 s2)) -[GOOD] (define-fun s98 () Bool (or s96 s97)) -[GOOD] (define-fun s99 () Bool (<= s93 s88)) -[GOOD] (define-fun s100 () Int (ite s99 s88 s93)) -[GOOD] (define-fun s101 () Int (- s91 s4)) -[GOOD] (define-fun s102 () (Seq Int) (seq.extract s90 s4 s101)) -[GOOD] (define-fun s103 () Int (seq.len s102)) -[GOOD] (define-fun s104 () Bool (= s2 s103)) -[GOOD] (define-fun s106 () (Seq Int) (seq.unit s105)) -[GOOD] (define-fun s107 () (Seq Int) (seq.extract s90 s2 s4)) -[GOOD] (define-fun s108 () Bool (= s106 s107)) -[GOOD] (define-fun s109 () Bool (<= s91 s2)) -[GOOD] (define-fun s110 () Bool (or s108 s109)) -[GOOD] (define-fun s111 () Bool (<= s105 s100)) -[GOOD] (define-fun s112 () Int (ite s111 s100 s105)) -[GOOD] (define-fun s114 () (Seq Int) (seq.unit s113)) -[GOOD] (define-fun s115 () (Seq Int) (seq.extract s102 s2 s4)) -[GOOD] (define-fun s116 () Bool (= s114 s115)) -[GOOD] (define-fun s117 () Bool (<= s103 s2)) -[GOOD] (define-fun s118 () Bool (or s116 s117)) -[GOOD] (define-fun s119 () Bool (<= s113 s112)) -[GOOD] (define-fun s120 () Int (ite s119 s112 s113)) -[GOOD] (define-fun s121 () Int (ite s104 s112 s120)) -[GOOD] (define-fun s122 () Int (ite s92 s100 s121)) -[GOOD] (define-fun s123 () Int (ite s80 s88 s122)) -[GOOD] (define-fun s124 () Int (ite s68 s76 s123)) -[GOOD] (define-fun s125 () Int (ite s56 s64 s124)) -[GOOD] (define-fun s126 () Int (ite s44 s52 s125)) -[GOOD] (define-fun s127 () Int (ite s32 s40 s126)) -[GOOD] (define-fun s128 () Int (ite s20 s28 s127)) -[GOOD] (define-fun s129 () Int (ite s8 s16 s128)) -[GOOD] (define-fun s130 () Int (ite s3 s2 s129)) -[GOOD] (define-fun s132 () Bool (> s130 s131)) -[GOOD] (define-fun s133 () Bool (not s132)) -[GOOD] (define-fun s134 () Bool (< s9 s2)) -[GOOD] (define-fun s135 () Bool (> s9 s131)) -[GOOD] (define-fun s136 () Bool (or s134 s135)) -[GOOD] (define-fun s137 () Bool (< s21 s2)) -[GOOD] (define-fun s138 () Bool (> s21 s131)) -[GOOD] (define-fun s139 () Bool (or s137 s138)) -[GOOD] (define-fun s140 () Bool (or s136 s139)) -[GOOD] (define-fun s141 () Bool (< s33 s2)) -[GOOD] (define-fun s142 () Bool (> s33 s131)) -[GOOD] (define-fun s143 () Bool (or s141 s142)) -[GOOD] (define-fun s144 () Bool (or s140 s143)) -[GOOD] (define-fun s145 () Bool (< s45 s2)) -[GOOD] (define-fun s146 () Bool (> s45 s131)) -[GOOD] (define-fun s147 () Bool (or s145 s146)) -[GOOD] (define-fun s148 () Bool (or s144 s147)) -[GOOD] (define-fun s149 () Bool (< s57 s2)) -[GOOD] (define-fun s150 () Bool (> s57 s131)) -[GOOD] (define-fun s151 () Bool (or s149 s150)) -[GOOD] (define-fun s152 () Bool (or s148 s151)) -[GOOD] (define-fun s153 () Bool (< s69 s2)) -[GOOD] (define-fun s154 () Bool (> s69 s131)) -[GOOD] (define-fun s155 () Bool (or s153 s154)) -[GOOD] (define-fun s156 () Bool (or s152 s155)) -[GOOD] (define-fun s157 () Bool (< s81 s2)) -[GOOD] (define-fun s158 () Bool (> s81 s131)) -[GOOD] (define-fun s159 () Bool (or s157 s158)) -[GOOD] (define-fun s160 () Bool (or s156 s159)) -[GOOD] (define-fun s161 () Bool (< s93 s2)) -[GOOD] (define-fun s162 () Bool (> s93 s131)) -[GOOD] (define-fun s163 () Bool (or s161 s162)) -[GOOD] (define-fun s164 () Bool (or s160 s163)) -[GOOD] (define-fun s165 () Bool (< s105 s2)) -[GOOD] (define-fun s166 () Bool (> s105 s131)) -[GOOD] (define-fun s167 () Bool (or s165 s166)) -[GOOD] (define-fun s168 () Bool (or s164 s167)) -[GOOD] (define-fun s169 () Bool (< s113 s2)) -[GOOD] (define-fun s170 () Bool (> s113 s131)) -[GOOD] (define-fun s171 () Bool (or s169 s170)) -[GOOD] (define-fun s172 () Bool (or s168 s171)) -[GOOD] (define-fun s173 () Bool (ite s104 s168 s172)) -[GOOD] (define-fun s174 () Bool (ite s92 s164 s173)) -[GOOD] (define-fun s175 () Bool (ite s80 s160 s174)) -[GOOD] (define-fun s176 () Bool (ite s68 s156 s175)) -[GOOD] (define-fun s177 () Bool (ite s56 s152 s176)) -[GOOD] (define-fun s178 () Bool (ite s44 s148 s177)) -[GOOD] (define-fun s179 () Bool (ite s32 s144 s178)) -[GOOD] (define-fun s180 () Bool (ite s20 s140 s179)) -[GOOD] (define-fun s181 () Bool (ite s8 s136 s180)) -[GOOD] (define-fun s182 () Bool (not s3)) -[GOOD] (define-fun s183 () Bool (and s181 s182)) -[GOOD] (define-fun s184 () Bool (or s133 s183)) -[GOOD] (assert s14) -[GOOD] (assert s26) -[GOOD] (assert s38) -[GOOD] (assert s50) -[GOOD] (assert s62) -[GOOD] (assert s74) -[GOOD] (assert s86) -[GOOD] (assert s98) -[GOOD] (assert s110) -[GOOD] (assert s118) -[GOOD] (assert s184) +[GOOD] (define-fun s87 () Bool (< s16 s2)) +[GOOD] (define-fun s88 () Bool (> s16 s81)) +[GOOD] (define-fun s89 () Bool (or s87 s88)) +[GOOD] (define-fun s90 () Bool (or s86 s89)) +[GOOD] (define-fun s91 () Bool (< s23 s2)) +[GOOD] (define-fun s92 () Bool (> s23 s81)) +[GOOD] (define-fun s93 () Bool (or s91 s92)) +[GOOD] (define-fun s94 () Bool (or s90 s93)) +[GOOD] (define-fun s95 () Bool (< s30 s2)) +[GOOD] (define-fun s96 () Bool (> s30 s81)) +[GOOD] (define-fun s97 () Bool (or s95 s96)) +[GOOD] (define-fun s98 () Bool (or s94 s97)) +[GOOD] (define-fun s99 () Bool (< s37 s2)) +[GOOD] (define-fun s100 () Bool (> s37 s81)) +[GOOD] (define-fun s101 () Bool (or s99 s100)) +[GOOD] (define-fun s102 () Bool (or s98 s101)) +[GOOD] (define-fun s103 () Bool (< s44 s2)) +[GOOD] (define-fun s104 () Bool (> s44 s81)) +[GOOD] (define-fun s105 () Bool (or s103 s104)) +[GOOD] (define-fun s106 () Bool (or s102 s105)) +[GOOD] (define-fun s107 () Bool (< s51 s2)) +[GOOD] (define-fun s108 () Bool (> s51 s81)) +[GOOD] (define-fun s109 () Bool (or s107 s108)) +[GOOD] (define-fun s110 () Bool (or s106 s109)) +[GOOD] (define-fun s111 () Bool (< s58 s2)) +[GOOD] (define-fun s112 () Bool (> s58 s81)) +[GOOD] (define-fun s113 () Bool (or s111 s112)) +[GOOD] (define-fun s114 () Bool (or s110 s113)) +[GOOD] (define-fun s115 () Bool (< s65 s2)) +[GOOD] (define-fun s116 () Bool (> s65 s81)) +[GOOD] (define-fun s117 () Bool (or s115 s116)) +[GOOD] (define-fun s118 () Bool (or s114 s117)) +[GOOD] (define-fun s119 () Bool (< s68 s2)) +[GOOD] (define-fun s120 () Bool (> s68 s81)) +[GOOD] (define-fun s121 () Bool (or s119 s120)) +[GOOD] (define-fun s122 () Bool (or s118 s121)) +[GOOD] (define-fun s123 () Bool (ite s64 s118 s122)) +[GOOD] (define-fun s124 () Bool (ite s57 s114 s123)) +[GOOD] (define-fun s125 () Bool (ite s50 s110 s124)) +[GOOD] (define-fun s126 () Bool (ite s43 s106 s125)) +[GOOD] (define-fun s127 () Bool (ite s36 s102 s126)) +[GOOD] (define-fun s128 () Bool (ite s29 s98 s127)) +[GOOD] (define-fun s129 () Bool (ite s22 s94 s128)) +[GOOD] (define-fun s130 () Bool (ite s15 s90 s129)) +[GOOD] (define-fun s131 () Bool (ite s8 s86 s130)) +[GOOD] (define-fun s132 () Bool (not s3)) +[GOOD] (define-fun s133 () Bool (and s131 s132)) +[GOOD] (define-fun s134 () Bool (or s83 s133)) +[GOOD] (assert s134) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/maxrWithFailure.gold b/SBVTestSuite/GoldFiles/maxrWithFailure.gold --- a/SBVTestSuite/GoldFiles/maxrWithFailure.gold +++ b/SBVTestSuite/GoldFiles/maxrWithFailure.gold @@ -7,26 +7,16 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 0) -[GOOD] (define-fun s6 () Int 1) -[GOOD] (define-fun s131 () Int 10) +[GOOD] (define-fun s5 () Int 1) +[GOOD] (define-fun s81 () Int 10) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" -[GOOD] (declare-fun s4 () Int) ; tracks user variable "__internal_sbv_s4" -[GOOD] (declare-fun s15 () Int) ; tracks user variable "__internal_sbv_s15" -[GOOD] (declare-fun s25 () Int) ; tracks user variable "__internal_sbv_s25" -[GOOD] (declare-fun s35 () Int) ; tracks user variable "__internal_sbv_s35" -[GOOD] (declare-fun s45 () Int) ; tracks user variable "__internal_sbv_s45" -[GOOD] (declare-fun s55 () Int) ; tracks user variable "__internal_sbv_s55" -[GOOD] (declare-fun s65 () Int) ; tracks user variable "__internal_sbv_s65" -[GOOD] (declare-fun s75 () Int) ; tracks user variable "__internal_sbv_s75" -[GOOD] (declare-fun s85 () Int) ; tracks user variable "__internal_sbv_s85" -[GOOD] (declare-fun s95 () Int) ; tracks user variable "__internal_sbv_s95" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -35,195 +25,145 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s5 () (Seq Int) (seq.unit s4)) -[GOOD] (define-fun s7 () (Seq Int) (seq.extract s0 s2 s6)) -[GOOD] (define-fun s8 () Bool (= s5 s7)) -[GOOD] (define-fun s9 () Bool (<= s1 s2)) -[GOOD] (define-fun s10 () Bool (or s8 s9)) -[GOOD] (define-fun s11 () Int (- s1 s6)) -[GOOD] (define-fun s12 () (Seq Int) (seq.extract s0 s6 s11)) +[GOOD] (define-fun s4 () Int (seq.nth s0 s2)) +[GOOD] (define-fun s6 () Int (- s1 s5)) +[GOOD] (define-fun s7 () (Seq Int) (seq.extract s0 s5 s6)) +[GOOD] (define-fun s8 () Int (seq.len s7)) +[GOOD] (define-fun s9 () Bool (= s2 s8)) +[GOOD] (define-fun s10 () Int (seq.nth s7 s2)) +[GOOD] (define-fun s11 () Int (- s8 s5)) +[GOOD] (define-fun s12 () (Seq Int) (seq.extract s7 s5 s11)) [GOOD] (define-fun s13 () Int (seq.len s12)) [GOOD] (define-fun s14 () Bool (= s2 s13)) -[GOOD] (define-fun s16 () (Seq Int) (seq.unit s15)) -[GOOD] (define-fun s17 () (Seq Int) (seq.extract s12 s2 s6)) -[GOOD] (define-fun s18 () Bool (= s16 s17)) -[GOOD] (define-fun s19 () Bool (<= s13 s2)) -[GOOD] (define-fun s20 () Bool (or s18 s19)) -[GOOD] (define-fun s21 () Int (- s13 s6)) -[GOOD] (define-fun s22 () (Seq Int) (seq.extract s12 s6 s21)) +[GOOD] (define-fun s15 () Int (seq.nth s12 s2)) +[GOOD] (define-fun s16 () Int (- s13 s5)) +[GOOD] (define-fun s17 () (Seq Int) (seq.extract s12 s5 s16)) +[GOOD] (define-fun s18 () Int (seq.len s17)) +[GOOD] (define-fun s19 () Bool (= s2 s18)) +[GOOD] (define-fun s20 () Int (seq.nth s17 s2)) +[GOOD] (define-fun s21 () Int (- s18 s5)) +[GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s5 s21)) [GOOD] (define-fun s23 () Int (seq.len s22)) [GOOD] (define-fun s24 () Bool (= s2 s23)) -[GOOD] (define-fun s26 () (Seq Int) (seq.unit s25)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s2 s6)) -[GOOD] (define-fun s28 () Bool (= s26 s27)) -[GOOD] (define-fun s29 () Bool (<= s23 s2)) -[GOOD] (define-fun s30 () Bool (or s28 s29)) -[GOOD] (define-fun s31 () Int (- s23 s6)) -[GOOD] (define-fun s32 () (Seq Int) (seq.extract s22 s6 s31)) +[GOOD] (define-fun s25 () Int (seq.nth s22 s2)) +[GOOD] (define-fun s26 () Int (- s23 s5)) +[GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s5 s26)) +[GOOD] (define-fun s28 () Int (seq.len s27)) +[GOOD] (define-fun s29 () Bool (= s2 s28)) +[GOOD] (define-fun s30 () Int (seq.nth s27 s2)) +[GOOD] (define-fun s31 () Int (- s28 s5)) +[GOOD] (define-fun s32 () (Seq Int) (seq.extract s27 s5 s31)) [GOOD] (define-fun s33 () Int (seq.len s32)) [GOOD] (define-fun s34 () Bool (= s2 s33)) -[GOOD] (define-fun s36 () (Seq Int) (seq.unit s35)) -[GOOD] (define-fun s37 () (Seq Int) (seq.extract s32 s2 s6)) -[GOOD] (define-fun s38 () Bool (= s36 s37)) -[GOOD] (define-fun s39 () Bool (<= s33 s2)) -[GOOD] (define-fun s40 () Bool (or s38 s39)) -[GOOD] (define-fun s41 () Int (- s33 s6)) -[GOOD] (define-fun s42 () (Seq Int) (seq.extract s32 s6 s41)) +[GOOD] (define-fun s35 () Int (seq.nth s32 s2)) +[GOOD] (define-fun s36 () Int (- s33 s5)) +[GOOD] (define-fun s37 () (Seq Int) (seq.extract s32 s5 s36)) +[GOOD] (define-fun s38 () Int (seq.len s37)) +[GOOD] (define-fun s39 () Bool (= s2 s38)) +[GOOD] (define-fun s40 () Int (seq.nth s37 s2)) +[GOOD] (define-fun s41 () Int (- s38 s5)) +[GOOD] (define-fun s42 () (Seq Int) (seq.extract s37 s5 s41)) [GOOD] (define-fun s43 () Int (seq.len s42)) [GOOD] (define-fun s44 () Bool (= s2 s43)) -[GOOD] (define-fun s46 () (Seq Int) (seq.unit s45)) -[GOOD] (define-fun s47 () (Seq Int) (seq.extract s42 s2 s6)) -[GOOD] (define-fun s48 () Bool (= s46 s47)) -[GOOD] (define-fun s49 () Bool (<= s43 s2)) -[GOOD] (define-fun s50 () Bool (or s48 s49)) -[GOOD] (define-fun s51 () Int (- s43 s6)) -[GOOD] (define-fun s52 () (Seq Int) (seq.extract s42 s6 s51)) -[GOOD] (define-fun s53 () Int (seq.len s52)) -[GOOD] (define-fun s54 () Bool (= s2 s53)) -[GOOD] (define-fun s56 () (Seq Int) (seq.unit s55)) -[GOOD] (define-fun s57 () (Seq Int) (seq.extract s52 s2 s6)) -[GOOD] (define-fun s58 () Bool (= s56 s57)) -[GOOD] (define-fun s59 () Bool (<= s53 s2)) -[GOOD] (define-fun s60 () Bool (or s58 s59)) -[GOOD] (define-fun s61 () Int (- s53 s6)) -[GOOD] (define-fun s62 () (Seq Int) (seq.extract s52 s6 s61)) -[GOOD] (define-fun s63 () Int (seq.len s62)) -[GOOD] (define-fun s64 () Bool (= s2 s63)) -[GOOD] (define-fun s66 () (Seq Int) (seq.unit s65)) -[GOOD] (define-fun s67 () (Seq Int) (seq.extract s62 s2 s6)) -[GOOD] (define-fun s68 () Bool (= s66 s67)) -[GOOD] (define-fun s69 () Bool (<= s63 s2)) -[GOOD] (define-fun s70 () Bool (or s68 s69)) -[GOOD] (define-fun s71 () Int (- s63 s6)) -[GOOD] (define-fun s72 () (Seq Int) (seq.extract s62 s6 s71)) -[GOOD] (define-fun s73 () Int (seq.len s72)) -[GOOD] (define-fun s74 () Bool (= s2 s73)) -[GOOD] (define-fun s76 () (Seq Int) (seq.unit s75)) -[GOOD] (define-fun s77 () (Seq Int) (seq.extract s72 s2 s6)) -[GOOD] (define-fun s78 () Bool (= s76 s77)) -[GOOD] (define-fun s79 () Bool (<= s73 s2)) -[GOOD] (define-fun s80 () Bool (or s78 s79)) -[GOOD] (define-fun s81 () Int (- s73 s6)) -[GOOD] (define-fun s82 () (Seq Int) (seq.extract s72 s6 s81)) -[GOOD] (define-fun s83 () Int (seq.len s82)) -[GOOD] (define-fun s84 () Bool (= s2 s83)) -[GOOD] (define-fun s86 () (Seq Int) (seq.unit s85)) -[GOOD] (define-fun s87 () (Seq Int) (seq.extract s82 s2 s6)) -[GOOD] (define-fun s88 () Bool (= s86 s87)) -[GOOD] (define-fun s89 () Bool (<= s83 s2)) -[GOOD] (define-fun s90 () Bool (or s88 s89)) -[GOOD] (define-fun s91 () Int (- s83 s6)) -[GOOD] (define-fun s92 () (Seq Int) (seq.extract s82 s6 s91)) -[GOOD] (define-fun s93 () Int (seq.len s92)) -[GOOD] (define-fun s94 () Bool (= s2 s93)) -[GOOD] (define-fun s96 () (Seq Int) (seq.unit s95)) -[GOOD] (define-fun s97 () (Seq Int) (seq.extract s92 s2 s6)) -[GOOD] (define-fun s98 () Bool (= s96 s97)) -[GOOD] (define-fun s99 () Bool (<= s93 s2)) -[GOOD] (define-fun s100 () Bool (or s98 s99)) -[GOOD] (define-fun s101 () Bool (<= s95 s2)) -[GOOD] (define-fun s102 () Int (ite s101 s2 s95)) -[GOOD] (define-fun s103 () Int (ite s94 s2 s102)) -[GOOD] (define-fun s104 () Bool (<= s85 s103)) -[GOOD] (define-fun s105 () Int (ite s104 s103 s85)) -[GOOD] (define-fun s106 () Int (ite s84 s2 s105)) -[GOOD] (define-fun s107 () Bool (<= s75 s106)) -[GOOD] (define-fun s108 () Int (ite s107 s106 s75)) -[GOOD] (define-fun s109 () Int (ite s74 s2 s108)) -[GOOD] (define-fun s110 () Bool (<= s65 s109)) -[GOOD] (define-fun s111 () Int (ite s110 s109 s65)) -[GOOD] (define-fun s112 () Int (ite s64 s2 s111)) -[GOOD] (define-fun s113 () Bool (<= s55 s112)) -[GOOD] (define-fun s114 () Int (ite s113 s112 s55)) -[GOOD] (define-fun s115 () Int (ite s54 s2 s114)) -[GOOD] (define-fun s116 () Bool (<= s45 s115)) -[GOOD] (define-fun s117 () Int (ite s116 s115 s45)) -[GOOD] (define-fun s118 () Int (ite s44 s2 s117)) -[GOOD] (define-fun s119 () Bool (<= s35 s118)) -[GOOD] (define-fun s120 () Int (ite s119 s118 s35)) -[GOOD] (define-fun s121 () Int (ite s34 s2 s120)) -[GOOD] (define-fun s122 () Bool (<= s25 s121)) -[GOOD] (define-fun s123 () Int (ite s122 s121 s25)) -[GOOD] (define-fun s124 () Int (ite s24 s2 s123)) -[GOOD] (define-fun s125 () Bool (<= s15 s124)) -[GOOD] (define-fun s126 () Int (ite s125 s124 s15)) -[GOOD] (define-fun s127 () Int (ite s14 s2 s126)) -[GOOD] (define-fun s128 () Bool (<= s4 s127)) -[GOOD] (define-fun s129 () Int (ite s128 s127 s4)) -[GOOD] (define-fun s130 () Int (ite s3 s2 s129)) -[GOOD] (define-fun s132 () Bool (> s130 s131)) -[GOOD] (define-fun s133 () Bool (not s132)) -[GOOD] (define-fun s134 () Bool (< s95 s2)) -[GOOD] (define-fun s135 () Bool (> s95 s131)) -[GOOD] (define-fun s136 () Bool (or s134 s135)) -[GOOD] (define-fun s137 () Bool (not s94)) -[GOOD] (define-fun s138 () Bool (and s136 s137)) -[GOOD] (define-fun s139 () Bool (< s85 s2)) -[GOOD] (define-fun s140 () Bool (> s85 s131)) -[GOOD] (define-fun s141 () Bool (or s139 s140)) -[GOOD] (define-fun s142 () Bool (or s138 s141)) -[GOOD] (define-fun s143 () Bool (not s84)) -[GOOD] (define-fun s144 () Bool (and s142 s143)) -[GOOD] (define-fun s145 () Bool (< s75 s2)) -[GOOD] (define-fun s146 () Bool (> s75 s131)) -[GOOD] (define-fun s147 () Bool (or s145 s146)) -[GOOD] (define-fun s148 () Bool (or s144 s147)) -[GOOD] (define-fun s149 () Bool (not s74)) -[GOOD] (define-fun s150 () Bool (and s148 s149)) -[GOOD] (define-fun s151 () Bool (< s65 s2)) -[GOOD] (define-fun s152 () Bool (> s65 s131)) -[GOOD] (define-fun s153 () Bool (or s151 s152)) -[GOOD] (define-fun s154 () Bool (or s150 s153)) -[GOOD] (define-fun s155 () Bool (not s64)) -[GOOD] (define-fun s156 () Bool (and s154 s155)) -[GOOD] (define-fun s157 () Bool (< s55 s2)) -[GOOD] (define-fun s158 () Bool (> s55 s131)) -[GOOD] (define-fun s159 () Bool (or s157 s158)) -[GOOD] (define-fun s160 () Bool (or s156 s159)) -[GOOD] (define-fun s161 () Bool (not s54)) -[GOOD] (define-fun s162 () Bool (and s160 s161)) -[GOOD] (define-fun s163 () Bool (< s45 s2)) -[GOOD] (define-fun s164 () Bool (> s45 s131)) -[GOOD] (define-fun s165 () Bool (or s163 s164)) -[GOOD] (define-fun s166 () Bool (or s162 s165)) -[GOOD] (define-fun s167 () Bool (not s44)) -[GOOD] (define-fun s168 () Bool (and s166 s167)) -[GOOD] (define-fun s169 () Bool (< s35 s2)) -[GOOD] (define-fun s170 () Bool (> s35 s131)) -[GOOD] (define-fun s171 () Bool (or s169 s170)) -[GOOD] (define-fun s172 () Bool (or s168 s171)) -[GOOD] (define-fun s173 () Bool (not s34)) -[GOOD] (define-fun s174 () Bool (and s172 s173)) -[GOOD] (define-fun s175 () Bool (< s25 s2)) -[GOOD] (define-fun s176 () Bool (> s25 s131)) -[GOOD] (define-fun s177 () Bool (or s175 s176)) -[GOOD] (define-fun s178 () Bool (or s174 s177)) -[GOOD] (define-fun s179 () Bool (not s24)) -[GOOD] (define-fun s180 () Bool (and s178 s179)) -[GOOD] (define-fun s181 () Bool (< s15 s2)) -[GOOD] (define-fun s182 () Bool (> s15 s131)) -[GOOD] (define-fun s183 () Bool (or s181 s182)) -[GOOD] (define-fun s184 () Bool (or s180 s183)) -[GOOD] (define-fun s185 () Bool (not s14)) -[GOOD] (define-fun s186 () Bool (and s184 s185)) -[GOOD] (define-fun s187 () Bool (< s4 s2)) -[GOOD] (define-fun s188 () Bool (> s4 s131)) -[GOOD] (define-fun s189 () Bool (or s187 s188)) -[GOOD] (define-fun s190 () Bool (or s186 s189)) -[GOOD] (define-fun s191 () Bool (not s3)) -[GOOD] (define-fun s192 () Bool (and s190 s191)) -[GOOD] (define-fun s193 () Bool (or s133 s192)) -[GOOD] (assert s10) -[GOOD] (assert s20) -[GOOD] (assert s30) -[GOOD] (assert s40) -[GOOD] (assert s50) -[GOOD] (assert s60) -[GOOD] (assert s70) -[GOOD] (assert s80) -[GOOD] (assert s90) -[GOOD] (assert s100) -[GOOD] (assert s193) +[GOOD] (define-fun s45 () Int (seq.nth s42 s2)) +[GOOD] (define-fun s46 () Int (- s43 s5)) +[GOOD] (define-fun s47 () (Seq Int) (seq.extract s42 s5 s46)) +[GOOD] (define-fun s48 () Int (seq.len s47)) +[GOOD] (define-fun s49 () Bool (= s2 s48)) +[GOOD] (define-fun s50 () Int (seq.nth s47 s2)) +[GOOD] (define-fun s51 () Bool (<= s50 s2)) +[GOOD] (define-fun s52 () Int (ite s51 s2 s50)) +[GOOD] (define-fun s53 () Int (ite s49 s2 s52)) +[GOOD] (define-fun s54 () Bool (<= s45 s53)) +[GOOD] (define-fun s55 () Int (ite s54 s53 s45)) +[GOOD] (define-fun s56 () Int (ite s44 s2 s55)) +[GOOD] (define-fun s57 () Bool (<= s40 s56)) +[GOOD] (define-fun s58 () Int (ite s57 s56 s40)) +[GOOD] (define-fun s59 () Int (ite s39 s2 s58)) +[GOOD] (define-fun s60 () Bool (<= s35 s59)) +[GOOD] (define-fun s61 () Int (ite s60 s59 s35)) +[GOOD] (define-fun s62 () Int (ite s34 s2 s61)) +[GOOD] (define-fun s63 () Bool (<= s30 s62)) +[GOOD] (define-fun s64 () Int (ite s63 s62 s30)) +[GOOD] (define-fun s65 () Int (ite s29 s2 s64)) +[GOOD] (define-fun s66 () Bool (<= s25 s65)) +[GOOD] (define-fun s67 () Int (ite s66 s65 s25)) +[GOOD] (define-fun s68 () Int (ite s24 s2 s67)) +[GOOD] (define-fun s69 () Bool (<= s20 s68)) +[GOOD] (define-fun s70 () Int (ite s69 s68 s20)) +[GOOD] (define-fun s71 () Int (ite s19 s2 s70)) +[GOOD] (define-fun s72 () Bool (<= s15 s71)) +[GOOD] (define-fun s73 () Int (ite s72 s71 s15)) +[GOOD] (define-fun s74 () Int (ite s14 s2 s73)) +[GOOD] (define-fun s75 () Bool (<= s10 s74)) +[GOOD] (define-fun s76 () Int (ite s75 s74 s10)) +[GOOD] (define-fun s77 () Int (ite s9 s2 s76)) +[GOOD] (define-fun s78 () Bool (<= s4 s77)) +[GOOD] (define-fun s79 () Int (ite s78 s77 s4)) +[GOOD] (define-fun s80 () Int (ite s3 s2 s79)) +[GOOD] (define-fun s82 () Bool (> s80 s81)) +[GOOD] (define-fun s83 () Bool (not s82)) +[GOOD] (define-fun s84 () Bool (< s50 s2)) +[GOOD] (define-fun s85 () Bool (> s50 s81)) +[GOOD] (define-fun s86 () Bool (or s84 s85)) +[GOOD] (define-fun s87 () Bool (not s49)) +[GOOD] (define-fun s88 () Bool (and s86 s87)) +[GOOD] (define-fun s89 () Bool (< s45 s2)) +[GOOD] (define-fun s90 () Bool (> s45 s81)) +[GOOD] (define-fun s91 () Bool (or s89 s90)) +[GOOD] (define-fun s92 () Bool (or s88 s91)) +[GOOD] (define-fun s93 () Bool (not s44)) +[GOOD] (define-fun s94 () Bool (and s92 s93)) +[GOOD] (define-fun s95 () Bool (< s40 s2)) +[GOOD] (define-fun s96 () Bool (> s40 s81)) +[GOOD] (define-fun s97 () Bool (or s95 s96)) +[GOOD] (define-fun s98 () Bool (or s94 s97)) +[GOOD] (define-fun s99 () Bool (not s39)) +[GOOD] (define-fun s100 () Bool (and s98 s99)) +[GOOD] (define-fun s101 () Bool (< s35 s2)) +[GOOD] (define-fun s102 () Bool (> s35 s81)) +[GOOD] (define-fun s103 () Bool (or s101 s102)) +[GOOD] (define-fun s104 () Bool (or s100 s103)) +[GOOD] (define-fun s105 () Bool (not s34)) +[GOOD] (define-fun s106 () Bool (and s104 s105)) +[GOOD] (define-fun s107 () Bool (< s30 s2)) +[GOOD] (define-fun s108 () Bool (> s30 s81)) +[GOOD] (define-fun s109 () Bool (or s107 s108)) +[GOOD] (define-fun s110 () Bool (or s106 s109)) +[GOOD] (define-fun s111 () Bool (not s29)) +[GOOD] (define-fun s112 () Bool (and s110 s111)) +[GOOD] (define-fun s113 () Bool (< s25 s2)) +[GOOD] (define-fun s114 () Bool (> s25 s81)) +[GOOD] (define-fun s115 () Bool (or s113 s114)) +[GOOD] (define-fun s116 () Bool (or s112 s115)) +[GOOD] (define-fun s117 () Bool (not s24)) +[GOOD] (define-fun s118 () Bool (and s116 s117)) +[GOOD] (define-fun s119 () Bool (< s20 s2)) +[GOOD] (define-fun s120 () Bool (> s20 s81)) +[GOOD] (define-fun s121 () Bool (or s119 s120)) +[GOOD] (define-fun s122 () Bool (or s118 s121)) +[GOOD] (define-fun s123 () Bool (not s19)) +[GOOD] (define-fun s124 () Bool (and s122 s123)) +[GOOD] (define-fun s125 () Bool (< s15 s2)) +[GOOD] (define-fun s126 () Bool (> s15 s81)) +[GOOD] (define-fun s127 () Bool (or s125 s126)) +[GOOD] (define-fun s128 () Bool (or s124 s127)) +[GOOD] (define-fun s129 () Bool (not s14)) +[GOOD] (define-fun s130 () Bool (and s128 s129)) +[GOOD] (define-fun s131 () Bool (< s10 s2)) +[GOOD] (define-fun s132 () Bool (> s10 s81)) +[GOOD] (define-fun s133 () Bool (or s131 s132)) +[GOOD] (define-fun s134 () Bool (or s130 s133)) +[GOOD] (define-fun s135 () Bool (not s9)) +[GOOD] (define-fun s136 () Bool (and s134 s135)) +[GOOD] (define-fun s137 () Bool (< s4 s2)) +[GOOD] (define-fun s138 () Bool (> s4 s81)) +[GOOD] (define-fun s139 () Bool (or s137 s138)) +[GOOD] (define-fun s140 () Bool (or s136 s139)) +[GOOD] (define-fun s141 () Bool (not s3)) +[GOOD] (define-fun s142 () Bool (and s140 s141)) +[GOOD] (define-fun s143 () Bool (or s83 s142)) +[GOOD] (assert s143) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -14,7 +14,7 @@ [GOOD] (set-info :status sat) [GOOD] (set-info :bad what) [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -73,7 +73,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.8.5") +[RECV] (:version "4.8.6") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -104,7 +104,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.8.5") +[RECV] (:version "4.8.6") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold b/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold --- a/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold +++ b/SBVTestSuite/GoldFiles/query_ListOfMaybe.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -16,12 +16,10 @@ (just_SBVMaybe (get_just_SBVMaybe T)))))) [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 2) -[GOOD] (define-fun s6 () Int 0) -[GOOD] (define-fun s7 () Int 1) +[GOOD] (define-fun s4 () Int 0) +[GOOD] (define-fun s8 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq (SBVMaybe (_ BitVec 8)))) ; tracks user variable "lst" -[GOOD] (declare-fun s4 () (SBVMaybe (_ BitVec 8))) ; tracks user variable "__internal_sbv_s4" -[GOOD] (declare-fun s14 () (SBVMaybe (_ BitVec 8))) ; tracks user variable "__internal_sbv_s14" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -30,28 +28,17 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s5 () (Seq (SBVMaybe (_ BitVec 8))) (seq.unit s4)) -[GOOD] (define-fun s8 () (Seq (SBVMaybe (_ BitVec 8))) (seq.extract s0 s6 s7)) -[GOOD] (define-fun s9 () Bool (= s5 s8)) -[GOOD] (define-fun s10 () Bool (<= s1 s6)) -[GOOD] (define-fun s11 () Bool (or s9 s10)) -[GOOD] (define-fun s12 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s4)) -[GOOD] (define-fun s13 () Bool (ite s12 false true)) -[GOOD] (define-fun s15 () (Seq (SBVMaybe (_ BitVec 8))) (seq.unit s14)) -[GOOD] (define-fun s16 () Int (- s1 s7)) -[GOOD] (define-fun s17 () (Seq (SBVMaybe (_ BitVec 8))) (seq.extract s0 s7 s16)) -[GOOD] (define-fun s18 () (Seq (SBVMaybe (_ BitVec 8))) (seq.extract s17 s6 s7)) -[GOOD] (define-fun s19 () Bool (= s15 s18)) -[GOOD] (define-fun s20 () Int (seq.len s17)) -[GOOD] (define-fun s21 () Bool (<= s20 s6)) -[GOOD] (define-fun s22 () Bool (or s19 s21)) -[GOOD] (define-fun s23 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s14)) -[GOOD] (define-fun s24 () Bool (ite s23 true false)) +[GOOD] (define-fun s5 () (SBVMaybe (_ BitVec 8)) (seq.nth s0 s4)) +[GOOD] (define-fun s6 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s5)) +[GOOD] (define-fun s7 () Bool (ite s6 false true)) +[GOOD] (define-fun s9 () Int (- s1 s8)) +[GOOD] (define-fun s10 () (Seq (SBVMaybe (_ BitVec 8))) (seq.extract s0 s8 s9)) +[GOOD] (define-fun s11 () (SBVMaybe (_ BitVec 8)) (seq.nth s10 s4)) +[GOOD] (define-fun s12 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s11)) +[GOOD] (define-fun s13 () Bool (ite s12 true false)) [GOOD] (assert s3) -[GOOD] (assert s11) +[GOOD] (assert s7) [GOOD] (assert s13) -[GOOD] (assert s22) -[GOOD] (assert s24) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) diff --git a/SBVTestSuite/GoldFiles/query_ListOfSum.gold b/SBVTestSuite/GoldFiles/query_ListOfSum.gold --- a/SBVTestSuite/GoldFiles/query_ListOfSum.gold +++ b/SBVTestSuite/GoldFiles/query_ListOfSum.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -16,12 +16,10 @@ (right_SBVEither (get_right_SBVEither T2)))))) [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 2) -[GOOD] (define-fun s6 () Int 0) -[GOOD] (define-fun s7 () Int 1) +[GOOD] (define-fun s4 () Int 0) +[GOOD] (define-fun s8 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq (SBVEither Int (_ BitVec 8)))) ; tracks user variable "lst" -[GOOD] (declare-fun s4 () (SBVEither Int (_ BitVec 8))) ; tracks user variable "__internal_sbv_s4" -[GOOD] (declare-fun s14 () (SBVEither Int (_ BitVec 8))) ; tracks user variable "__internal_sbv_s14" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -30,28 +28,17 @@ [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2)) -[GOOD] (define-fun s5 () (Seq (SBVEither Int (_ BitVec 8))) (seq.unit s4)) -[GOOD] (define-fun s8 () (Seq (SBVEither Int (_ BitVec 8))) (seq.extract s0 s6 s7)) -[GOOD] (define-fun s9 () Bool (= s5 s8)) -[GOOD] (define-fun s10 () Bool (<= s1 s6)) -[GOOD] (define-fun s11 () Bool (or s9 s10)) -[GOOD] (define-fun s12 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s4)) -[GOOD] (define-fun s13 () Bool (ite s12 true false)) -[GOOD] (define-fun s15 () (Seq (SBVEither Int (_ BitVec 8))) (seq.unit s14)) -[GOOD] (define-fun s16 () Int (- s1 s7)) -[GOOD] (define-fun s17 () (Seq (SBVEither Int (_ BitVec 8))) (seq.extract s0 s7 s16)) -[GOOD] (define-fun s18 () (Seq (SBVEither Int (_ BitVec 8))) (seq.extract s17 s6 s7)) -[GOOD] (define-fun s19 () Bool (= s15 s18)) -[GOOD] (define-fun s20 () Int (seq.len s17)) -[GOOD] (define-fun s21 () Bool (<= s20 s6)) -[GOOD] (define-fun s22 () Bool (or s19 s21)) -[GOOD] (define-fun s23 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s14)) -[GOOD] (define-fun s24 () Bool (ite s23 false true)) +[GOOD] (define-fun s5 () (SBVEither Int (_ BitVec 8)) (seq.nth s0 s4)) +[GOOD] (define-fun s6 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s5)) +[GOOD] (define-fun s7 () Bool (ite s6 true false)) +[GOOD] (define-fun s9 () Int (- s1 s8)) +[GOOD] (define-fun s10 () (Seq (SBVEither Int (_ BitVec 8))) (seq.extract s0 s8 s9)) +[GOOD] (define-fun s11 () (SBVEither Int (_ BitVec 8)) (seq.nth s10 s4)) +[GOOD] (define-fun s12 () Bool ((_ is (left_SBVEither (Int) (SBVEither Int (_ BitVec 8)))) s11)) +[GOOD] (define-fun s13 () Bool (ite s12 false true)) [GOOD] (assert s3) -[GOOD] (assert s11) +[GOOD] (assert s7) [GOOD] (assert s13) -[GOOD] (assert s22) -[GOOD] (assert s24) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) diff --git a/SBVTestSuite/GoldFiles/query_Lists1.gold b/SBVTestSuite/GoldFiles/query_Lists1.gold --- a/SBVTestSuite/GoldFiles/query_Lists1.gold +++ b/SBVTestSuite/GoldFiles/query_Lists1.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/query_Strings1.gold b/SBVTestSuite/GoldFiles/query_Strings1.gold --- a/SBVTestSuite/GoldFiles/query_Strings1.gold +++ b/SBVTestSuite/GoldFiles/query_Strings1.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has strings, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold b/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold --- a/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold +++ b/SBVTestSuite/GoldFiles/query_sumMergeEither1.gold @@ -34,11 +34,11 @@ [SEND] (get-value (s0)) [RECV] ((s0 (left_SBVEither 0))) [SEND] (get-value (s1)) -[RECV] ((s1 (right_SBVEither false))) +[RECV] ((s1 (left_SBVEither 0))) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) *** Solver : Z3 *** Exit code: ExitSuccess FINAL OUTPUT: -(Left 0,Right False,True) +(Left 0,Left 0,False) diff --git a/SBVTestSuite/GoldFiles/query_sumMergeEither2.gold b/SBVTestSuite/GoldFiles/query_sumMergeEither2.gold --- a/SBVTestSuite/GoldFiles/query_sumMergeEither2.gold +++ b/SBVTestSuite/GoldFiles/query_sumMergeEither2.gold @@ -36,9 +36,9 @@ [SEND] (get-value (s1)) [RECV] ((s1 (right_SBVEither false))) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) *** Solver : Z3 *** Exit code: ExitSuccess FINAL OUTPUT: -(Right False,Right False,True) +(Right False,Right False,False) diff --git a/SBVTestSuite/GoldFiles/query_sumMergeMaybe1.gold b/SBVTestSuite/GoldFiles/query_sumMergeMaybe1.gold --- a/SBVTestSuite/GoldFiles/query_sumMergeMaybe1.gold +++ b/SBVTestSuite/GoldFiles/query_sumMergeMaybe1.gold @@ -34,11 +34,11 @@ [SEND] (get-value (s0)) [RECV] ((s0 nothing_SBVMaybe)) [SEND] (get-value (s1)) -[RECV] ((s1 (just_SBVMaybe 0))) +[RECV] ((s1 nothing_SBVMaybe)) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) *** Solver : Z3 *** Exit code: ExitSuccess FINAL OUTPUT: -(Nothing,Just 0,True) +(Nothing,Nothing,False) diff --git a/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold b/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold --- a/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold +++ b/SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold @@ -36,9 +36,9 @@ [SEND] (get-value (s1)) [RECV] ((s1 (just_SBVMaybe 0))) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) *** Solver : Z3 *** Exit code: ExitSuccess FINAL OUTPUT: -(Just 0,Just 0,True) +(Just 0,Just 0,False) diff --git a/SBVTestSuite/GoldFiles/query_uisatex1.gold b/SBVTestSuite/GoldFiles/query_uisatex1.gold --- a/SBVTestSuite/GoldFiles/query_uisatex1.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex1.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/query_uisatex2.gold b/SBVTestSuite/GoldFiles/query_uisatex2.gold --- a/SBVTestSuite/GoldFiles/query_uisatex2.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex2.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/reverse.gold b/SBVTestSuite/GoldFiles/reverse.gold --- a/SBVTestSuite/GoldFiles/reverse.gold +++ b/SBVTestSuite/GoldFiles/reverse.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -20,16 +20,6 @@ [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" [GOOD] (declare-fun s3 () Int) ; tracks user variable "d" -[GOOD] (declare-fun s52 () Int) ; tracks user variable "__internal_sbv_s52" -[GOOD] (declare-fun s59 () Int) ; tracks user variable "__internal_sbv_s59" -[GOOD] (declare-fun s67 () Int) ; tracks user variable "__internal_sbv_s67" -[GOOD] (declare-fun s75 () Int) ; tracks user variable "__internal_sbv_s75" -[GOOD] (declare-fun s83 () Int) ; tracks user variable "__internal_sbv_s83" -[GOOD] (declare-fun s91 () Int) ; tracks user variable "__internal_sbv_s91" -[GOOD] (declare-fun s99 () Int) ; tracks user variable "__internal_sbv_s99" -[GOOD] (declare-fun s107 () Int) ; tracks user variable "__internal_sbv_s107" -[GOOD] (declare-fun s115 () Int) ; tracks user variable "__internal_sbv_s115" -[GOOD] (declare-fun s123 () Int) ; tracks user variable "__internal_sbv_s123" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -81,90 +71,50 @@ [GOOD] (define-fun s49 () (Seq Int) (seq.extract s45 s15 s48)) [GOOD] (define-fun s50 () Int (seq.len s49)) [GOOD] (define-fun s51 () Bool (= s12 s50)) +[GOOD] (define-fun s52 () Int (seq.nth s49 s12)) [GOOD] (define-fun s53 () (Seq Int) (seq.unit s52)) -[GOOD] (define-fun s54 () (Seq Int) (seq.extract s49 s12 s15)) -[GOOD] (define-fun s55 () Bool (= s53 s54)) -[GOOD] (define-fun s56 () Bool (<= s50 s12)) -[GOOD] (define-fun s57 () Bool (or s55 s56)) -[GOOD] (define-fun s58 () (Seq Int) (ite s51 s14 s53)) +[GOOD] (define-fun s54 () (Seq Int) (ite s51 s14 s53)) +[GOOD] (define-fun s55 () Int (seq.nth s45 s12)) +[GOOD] (define-fun s56 () (Seq Int) (seq.unit s55)) +[GOOD] (define-fun s57 () (Seq Int) (seq.++ s54 s56)) +[GOOD] (define-fun s58 () (Seq Int) (ite s47 s14 s57)) +[GOOD] (define-fun s59 () Int (seq.nth s41 s12)) [GOOD] (define-fun s60 () (Seq Int) (seq.unit s59)) -[GOOD] (define-fun s61 () (Seq Int) (seq.extract s45 s12 s15)) -[GOOD] (define-fun s62 () Bool (= s60 s61)) -[GOOD] (define-fun s63 () Bool (<= s46 s12)) -[GOOD] (define-fun s64 () Bool (or s62 s63)) -[GOOD] (define-fun s65 () (Seq Int) (seq.++ s58 s60)) -[GOOD] (define-fun s66 () (Seq Int) (ite s47 s14 s65)) +[GOOD] (define-fun s61 () (Seq Int) (seq.++ s58 s60)) +[GOOD] (define-fun s62 () (Seq Int) (ite s43 s14 s61)) +[GOOD] (define-fun s63 () Int (seq.nth s37 s12)) +[GOOD] (define-fun s64 () (Seq Int) (seq.unit s63)) +[GOOD] (define-fun s65 () (Seq Int) (seq.++ s62 s64)) +[GOOD] (define-fun s66 () (Seq Int) (ite s39 s14 s65)) +[GOOD] (define-fun s67 () Int (seq.nth s33 s12)) [GOOD] (define-fun s68 () (Seq Int) (seq.unit s67)) -[GOOD] (define-fun s69 () (Seq Int) (seq.extract s41 s12 s15)) -[GOOD] (define-fun s70 () Bool (= s68 s69)) -[GOOD] (define-fun s71 () Bool (<= s42 s12)) -[GOOD] (define-fun s72 () Bool (or s70 s71)) -[GOOD] (define-fun s73 () (Seq Int) (seq.++ s66 s68)) -[GOOD] (define-fun s74 () (Seq Int) (ite s43 s14 s73)) +[GOOD] (define-fun s69 () (Seq Int) (seq.++ s66 s68)) +[GOOD] (define-fun s70 () (Seq Int) (ite s35 s14 s69)) +[GOOD] (define-fun s71 () Int (seq.nth s29 s12)) +[GOOD] (define-fun s72 () (Seq Int) (seq.unit s71)) +[GOOD] (define-fun s73 () (Seq Int) (seq.++ s70 s72)) +[GOOD] (define-fun s74 () (Seq Int) (ite s31 s14 s73)) +[GOOD] (define-fun s75 () Int (seq.nth s25 s12)) [GOOD] (define-fun s76 () (Seq Int) (seq.unit s75)) -[GOOD] (define-fun s77 () (Seq Int) (seq.extract s37 s12 s15)) -[GOOD] (define-fun s78 () Bool (= s76 s77)) -[GOOD] (define-fun s79 () Bool (<= s38 s12)) -[GOOD] (define-fun s80 () Bool (or s78 s79)) -[GOOD] (define-fun s81 () (Seq Int) (seq.++ s74 s76)) -[GOOD] (define-fun s82 () (Seq Int) (ite s39 s14 s81)) +[GOOD] (define-fun s77 () (Seq Int) (seq.++ s74 s76)) +[GOOD] (define-fun s78 () (Seq Int) (ite s27 s14 s77)) +[GOOD] (define-fun s79 () Int (seq.nth s21 s12)) +[GOOD] (define-fun s80 () (Seq Int) (seq.unit s79)) +[GOOD] (define-fun s81 () (Seq Int) (seq.++ s78 s80)) +[GOOD] (define-fun s82 () (Seq Int) (ite s23 s14 s81)) +[GOOD] (define-fun s83 () Int (seq.nth s17 s12)) [GOOD] (define-fun s84 () (Seq Int) (seq.unit s83)) -[GOOD] (define-fun s85 () (Seq Int) (seq.extract s33 s12 s15)) -[GOOD] (define-fun s86 () Bool (= s84 s85)) -[GOOD] (define-fun s87 () Bool (<= s34 s12)) -[GOOD] (define-fun s88 () Bool (or s86 s87)) -[GOOD] (define-fun s89 () (Seq Int) (seq.++ s82 s84)) -[GOOD] (define-fun s90 () (Seq Int) (ite s35 s14 s89)) -[GOOD] (define-fun s92 () (Seq Int) (seq.unit s91)) -[GOOD] (define-fun s93 () (Seq Int) (seq.extract s29 s12 s15)) -[GOOD] (define-fun s94 () Bool (= s92 s93)) -[GOOD] (define-fun s95 () Bool (<= s30 s12)) -[GOOD] (define-fun s96 () Bool (or s94 s95)) -[GOOD] (define-fun s97 () (Seq Int) (seq.++ s90 s92)) -[GOOD] (define-fun s98 () (Seq Int) (ite s31 s14 s97)) -[GOOD] (define-fun s100 () (Seq Int) (seq.unit s99)) -[GOOD] (define-fun s101 () (Seq Int) (seq.extract s25 s12 s15)) -[GOOD] (define-fun s102 () Bool (= s100 s101)) -[GOOD] (define-fun s103 () Bool (<= s26 s12)) -[GOOD] (define-fun s104 () Bool (or s102 s103)) -[GOOD] (define-fun s105 () (Seq Int) (seq.++ s98 s100)) -[GOOD] (define-fun s106 () (Seq Int) (ite s27 s14 s105)) -[GOOD] (define-fun s108 () (Seq Int) (seq.unit s107)) -[GOOD] (define-fun s109 () (Seq Int) (seq.extract s21 s12 s15)) -[GOOD] (define-fun s110 () Bool (= s108 s109)) -[GOOD] (define-fun s111 () Bool (<= s22 s12)) -[GOOD] (define-fun s112 () Bool (or s110 s111)) -[GOOD] (define-fun s113 () (Seq Int) (seq.++ s106 s108)) -[GOOD] (define-fun s114 () (Seq Int) (ite s23 s14 s113)) -[GOOD] (define-fun s116 () (Seq Int) (seq.unit s115)) -[GOOD] (define-fun s117 () (Seq Int) (seq.extract s17 s12 s15)) -[GOOD] (define-fun s118 () Bool (= s116 s117)) -[GOOD] (define-fun s119 () Bool (<= s18 s12)) -[GOOD] (define-fun s120 () Bool (or s118 s119)) -[GOOD] (define-fun s121 () (Seq Int) (seq.++ s114 s116)) -[GOOD] (define-fun s122 () (Seq Int) (ite s19 s14 s121)) -[GOOD] (define-fun s124 () (Seq Int) (seq.unit s123)) -[GOOD] (define-fun s125 () (Seq Int) (seq.extract s10 s12 s15)) -[GOOD] (define-fun s126 () Bool (= s124 s125)) -[GOOD] (define-fun s127 () Bool (<= s11 s12)) -[GOOD] (define-fun s128 () Bool (or s126 s127)) -[GOOD] (define-fun s129 () (Seq Int) (seq.++ s122 s124)) -[GOOD] (define-fun s130 () (Seq Int) (ite s13 s14 s129)) -[GOOD] (define-fun s131 () (Seq Int) (seq.++ s5 s4)) -[GOOD] (define-fun s132 () (Seq Int) (seq.++ s6 s131)) -[GOOD] (define-fun s133 () (Seq Int) (seq.++ s7 s132)) -[GOOD] (define-fun s134 () Bool (= s130 s133)) -[GOOD] (assert s57) -[GOOD] (assert s64) -[GOOD] (assert s72) -[GOOD] (assert s80) -[GOOD] (assert s88) -[GOOD] (assert s96) -[GOOD] (assert s104) -[GOOD] (assert s112) -[GOOD] (assert s120) -[GOOD] (assert s128) -[GOOD] (assert s134) +[GOOD] (define-fun s85 () (Seq Int) (seq.++ s82 s84)) +[GOOD] (define-fun s86 () (Seq Int) (ite s19 s14 s85)) +[GOOD] (define-fun s87 () Int (seq.nth s10 s12)) +[GOOD] (define-fun s88 () (Seq Int) (seq.unit s87)) +[GOOD] (define-fun s89 () (Seq Int) (seq.++ s86 s88)) +[GOOD] (define-fun s90 () (Seq Int) (ite s13 s14 s89)) +[GOOD] (define-fun s91 () (Seq Int) (seq.++ s5 s4)) +[GOOD] (define-fun s92 () (Seq Int) (seq.++ s6 s91)) +[GOOD] (define-fun s93 () (Seq Int) (seq.++ s7 s92)) +[GOOD] (define-fun s94 () Bool (= s90 s93)) +[GOOD] (assert s94) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/reverseAlt10.gold b/SBVTestSuite/GoldFiles/reverseAlt10.gold --- a/SBVTestSuite/GoldFiles/reverseAlt10.gold +++ b/SBVTestSuite/GoldFiles/reverseAlt10.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -17,26 +17,6 @@ [GOOD] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "xs" -[GOOD] (declare-fun s42 () Int) ; tracks user variable "__internal_sbv_s42" -[GOOD] (declare-fun s49 () Int) ; tracks user variable "__internal_sbv_s49" -[GOOD] (declare-fun s57 () Int) ; tracks user variable "__internal_sbv_s57" -[GOOD] (declare-fun s65 () Int) ; tracks user variable "__internal_sbv_s65" -[GOOD] (declare-fun s73 () Int) ; tracks user variable "__internal_sbv_s73" -[GOOD] (declare-fun s81 () Int) ; tracks user variable "__internal_sbv_s81" -[GOOD] (declare-fun s89 () Int) ; tracks user variable "__internal_sbv_s89" -[GOOD] (declare-fun s97 () Int) ; tracks user variable "__internal_sbv_s97" -[GOOD] (declare-fun s105 () Int) ; tracks user variable "__internal_sbv_s105" -[GOOD] (declare-fun s113 () Int) ; tracks user variable "__internal_sbv_s113" -[GOOD] (declare-fun s121 () Int) ; tracks user variable "__internal_sbv_s121" -[GOOD] (declare-fun s125 () Int) ; tracks user variable "__internal_sbv_s125" -[GOOD] (declare-fun s130 () Int) ; tracks user variable "__internal_sbv_s130" -[GOOD] (declare-fun s135 () Int) ; tracks user variable "__internal_sbv_s135" -[GOOD] (declare-fun s140 () Int) ; tracks user variable "__internal_sbv_s140" -[GOOD] (declare-fun s145 () Int) ; tracks user variable "__internal_sbv_s145" -[GOOD] (declare-fun s150 () Int) ; tracks user variable "__internal_sbv_s150" -[GOOD] (declare-fun s155 () Int) ; tracks user variable "__internal_sbv_s155" -[GOOD] (declare-fun s160 () Int) ; tracks user variable "__internal_sbv_s160" -[GOOD] (declare-fun s165 () Int) ; tracks user variable "__internal_sbv_s165" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -81,146 +61,66 @@ [GOOD] (define-fun s39 () (Seq Int) (seq.extract s35 s5 s38)) [GOOD] (define-fun s40 () Int (seq.len s39)) [GOOD] (define-fun s41 () Bool (= s2 s40)) +[GOOD] (define-fun s42 () Int (seq.nth s39 s2)) [GOOD] (define-fun s43 () (Seq Int) (seq.unit s42)) -[GOOD] (define-fun s44 () (Seq Int) (seq.extract s39 s2 s5)) -[GOOD] (define-fun s45 () Bool (= s43 s44)) -[GOOD] (define-fun s46 () Bool (<= s40 s2)) -[GOOD] (define-fun s47 () Bool (or s45 s46)) -[GOOD] (define-fun s48 () (Seq Int) (ite s41 s4 s43)) +[GOOD] (define-fun s44 () (Seq Int) (ite s41 s4 s43)) +[GOOD] (define-fun s45 () Int (seq.nth s35 s2)) +[GOOD] (define-fun s46 () (Seq Int) (seq.unit s45)) +[GOOD] (define-fun s47 () (Seq Int) (seq.++ s44 s46)) +[GOOD] (define-fun s48 () (Seq Int) (ite s37 s4 s47)) +[GOOD] (define-fun s49 () Int (seq.nth s31 s2)) [GOOD] (define-fun s50 () (Seq Int) (seq.unit s49)) -[GOOD] (define-fun s51 () (Seq Int) (seq.extract s35 s2 s5)) -[GOOD] (define-fun s52 () Bool (= s50 s51)) -[GOOD] (define-fun s53 () Bool (<= s36 s2)) -[GOOD] (define-fun s54 () Bool (or s52 s53)) -[GOOD] (define-fun s55 () (Seq Int) (seq.++ s48 s50)) -[GOOD] (define-fun s56 () (Seq Int) (ite s37 s4 s55)) +[GOOD] (define-fun s51 () (Seq Int) (seq.++ s48 s50)) +[GOOD] (define-fun s52 () (Seq Int) (ite s33 s4 s51)) +[GOOD] (define-fun s53 () Int (seq.nth s27 s2)) +[GOOD] (define-fun s54 () (Seq Int) (seq.unit s53)) +[GOOD] (define-fun s55 () (Seq Int) (seq.++ s52 s54)) +[GOOD] (define-fun s56 () (Seq Int) (ite s29 s4 s55)) +[GOOD] (define-fun s57 () Int (seq.nth s23 s2)) [GOOD] (define-fun s58 () (Seq Int) (seq.unit s57)) -[GOOD] (define-fun s59 () (Seq Int) (seq.extract s31 s2 s5)) -[GOOD] (define-fun s60 () Bool (= s58 s59)) -[GOOD] (define-fun s61 () Bool (<= s32 s2)) -[GOOD] (define-fun s62 () Bool (or s60 s61)) -[GOOD] (define-fun s63 () (Seq Int) (seq.++ s56 s58)) -[GOOD] (define-fun s64 () (Seq Int) (ite s33 s4 s63)) +[GOOD] (define-fun s59 () (Seq Int) (seq.++ s56 s58)) +[GOOD] (define-fun s60 () (Seq Int) (ite s25 s4 s59)) +[GOOD] (define-fun s61 () Int (seq.nth s19 s2)) +[GOOD] (define-fun s62 () (Seq Int) (seq.unit s61)) +[GOOD] (define-fun s63 () (Seq Int) (seq.++ s60 s62)) +[GOOD] (define-fun s64 () (Seq Int) (ite s21 s4 s63)) +[GOOD] (define-fun s65 () Int (seq.nth s15 s2)) [GOOD] (define-fun s66 () (Seq Int) (seq.unit s65)) -[GOOD] (define-fun s67 () (Seq Int) (seq.extract s27 s2 s5)) -[GOOD] (define-fun s68 () Bool (= s66 s67)) -[GOOD] (define-fun s69 () Bool (<= s28 s2)) -[GOOD] (define-fun s70 () Bool (or s68 s69)) -[GOOD] (define-fun s71 () (Seq Int) (seq.++ s64 s66)) -[GOOD] (define-fun s72 () (Seq Int) (ite s29 s4 s71)) +[GOOD] (define-fun s67 () (Seq Int) (seq.++ s64 s66)) +[GOOD] (define-fun s68 () (Seq Int) (ite s17 s4 s67)) +[GOOD] (define-fun s69 () Int (seq.nth s11 s2)) +[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) +[GOOD] (define-fun s71 () (Seq Int) (seq.++ s68 s70)) +[GOOD] (define-fun s72 () (Seq Int) (ite s13 s4 s71)) +[GOOD] (define-fun s73 () Int (seq.nth s7 s2)) [GOOD] (define-fun s74 () (Seq Int) (seq.unit s73)) -[GOOD] (define-fun s75 () (Seq Int) (seq.extract s23 s2 s5)) -[GOOD] (define-fun s76 () Bool (= s74 s75)) -[GOOD] (define-fun s77 () Bool (<= s24 s2)) -[GOOD] (define-fun s78 () Bool (or s76 s77)) -[GOOD] (define-fun s79 () (Seq Int) (seq.++ s72 s74)) -[GOOD] (define-fun s80 () (Seq Int) (ite s25 s4 s79)) -[GOOD] (define-fun s82 () (Seq Int) (seq.unit s81)) -[GOOD] (define-fun s83 () (Seq Int) (seq.extract s19 s2 s5)) -[GOOD] (define-fun s84 () Bool (= s82 s83)) -[GOOD] (define-fun s85 () Bool (<= s20 s2)) -[GOOD] (define-fun s86 () Bool (or s84 s85)) -[GOOD] (define-fun s87 () (Seq Int) (seq.++ s80 s82)) -[GOOD] (define-fun s88 () (Seq Int) (ite s21 s4 s87)) -[GOOD] (define-fun s90 () (Seq Int) (seq.unit s89)) -[GOOD] (define-fun s91 () (Seq Int) (seq.extract s15 s2 s5)) -[GOOD] (define-fun s92 () Bool (= s90 s91)) -[GOOD] (define-fun s93 () Bool (<= s16 s2)) -[GOOD] (define-fun s94 () Bool (or s92 s93)) -[GOOD] (define-fun s95 () (Seq Int) (seq.++ s88 s90)) -[GOOD] (define-fun s96 () (Seq Int) (ite s17 s4 s95)) -[GOOD] (define-fun s98 () (Seq Int) (seq.unit s97)) -[GOOD] (define-fun s99 () (Seq Int) (seq.extract s11 s2 s5)) -[GOOD] (define-fun s100 () Bool (= s98 s99)) -[GOOD] (define-fun s101 () Bool (<= s12 s2)) -[GOOD] (define-fun s102 () Bool (or s100 s101)) -[GOOD] (define-fun s103 () (Seq Int) (seq.++ s96 s98)) -[GOOD] (define-fun s104 () (Seq Int) (ite s13 s4 s103)) -[GOOD] (define-fun s106 () (Seq Int) (seq.unit s105)) -[GOOD] (define-fun s107 () (Seq Int) (seq.extract s7 s2 s5)) -[GOOD] (define-fun s108 () Bool (= s106 s107)) -[GOOD] (define-fun s109 () Bool (<= s8 s2)) -[GOOD] (define-fun s110 () Bool (or s108 s109)) -[GOOD] (define-fun s111 () (Seq Int) (seq.++ s104 s106)) -[GOOD] (define-fun s112 () (Seq Int) (ite s9 s4 s111)) -[GOOD] (define-fun s114 () (Seq Int) (seq.unit s113)) -[GOOD] (define-fun s115 () (Seq Int) (seq.extract s0 s2 s5)) -[GOOD] (define-fun s116 () Bool (= s114 s115)) -[GOOD] (define-fun s117 () Bool (<= s1 s2)) -[GOOD] (define-fun s118 () Bool (or s116 s117)) -[GOOD] (define-fun s119 () (Seq Int) (seq.++ s112 s114)) -[GOOD] (define-fun s120 () (Seq Int) (ite s3 s4 s119)) -[GOOD] (define-fun s122 () (Seq Int) (seq.unit s121)) -[GOOD] (define-fun s123 () Bool (= s115 s122)) -[GOOD] (define-fun s124 () Bool (or s117 s123)) -[GOOD] (define-fun s126 () (Seq Int) (seq.unit s125)) -[GOOD] (define-fun s127 () Bool (= s107 s126)) -[GOOD] (define-fun s128 () Bool (or s109 s127)) -[GOOD] (define-fun s129 () (Seq Int) (seq.++ s126 s122)) -[GOOD] (define-fun s131 () (Seq Int) (seq.unit s130)) -[GOOD] (define-fun s132 () Bool (= s99 s131)) -[GOOD] (define-fun s133 () Bool (or s101 s132)) -[GOOD] (define-fun s134 () (Seq Int) (seq.++ s131 s129)) -[GOOD] (define-fun s136 () (Seq Int) (seq.unit s135)) -[GOOD] (define-fun s137 () Bool (= s91 s136)) -[GOOD] (define-fun s138 () Bool (or s93 s137)) -[GOOD] (define-fun s139 () (Seq Int) (seq.++ s136 s134)) -[GOOD] (define-fun s141 () (Seq Int) (seq.unit s140)) -[GOOD] (define-fun s142 () Bool (= s83 s141)) -[GOOD] (define-fun s143 () Bool (or s85 s142)) -[GOOD] (define-fun s144 () (Seq Int) (seq.++ s141 s139)) -[GOOD] (define-fun s146 () (Seq Int) (seq.unit s145)) -[GOOD] (define-fun s147 () Bool (= s75 s146)) -[GOOD] (define-fun s148 () Bool (or s77 s147)) -[GOOD] (define-fun s149 () (Seq Int) (seq.++ s146 s144)) -[GOOD] (define-fun s151 () (Seq Int) (seq.unit s150)) -[GOOD] (define-fun s152 () Bool (= s67 s151)) -[GOOD] (define-fun s153 () Bool (or s69 s152)) -[GOOD] (define-fun s154 () (Seq Int) (seq.++ s151 s149)) -[GOOD] (define-fun s156 () (Seq Int) (seq.unit s155)) -[GOOD] (define-fun s157 () Bool (= s59 s156)) -[GOOD] (define-fun s158 () Bool (or s61 s157)) -[GOOD] (define-fun s159 () (Seq Int) (seq.++ s156 s154)) -[GOOD] (define-fun s161 () (Seq Int) (seq.unit s160)) -[GOOD] (define-fun s162 () Bool (= s51 s161)) -[GOOD] (define-fun s163 () Bool (or s53 s162)) -[GOOD] (define-fun s164 () (Seq Int) (seq.++ s161 s159)) -[GOOD] (define-fun s166 () (Seq Int) (seq.unit s165)) -[GOOD] (define-fun s167 () Bool (= s44 s166)) -[GOOD] (define-fun s168 () Bool (or s46 s167)) -[GOOD] (define-fun s169 () (Seq Int) (seq.++ s166 s164)) -[GOOD] (define-fun s170 () (Seq Int) (ite s41 s164 s169)) -[GOOD] (define-fun s171 () (Seq Int) (ite s37 s159 s170)) -[GOOD] (define-fun s172 () (Seq Int) (ite s33 s154 s171)) -[GOOD] (define-fun s173 () (Seq Int) (ite s29 s149 s172)) -[GOOD] (define-fun s174 () (Seq Int) (ite s25 s144 s173)) -[GOOD] (define-fun s175 () (Seq Int) (ite s21 s139 s174)) -[GOOD] (define-fun s176 () (Seq Int) (ite s17 s134 s175)) -[GOOD] (define-fun s177 () (Seq Int) (ite s13 s129 s176)) -[GOOD] (define-fun s178 () (Seq Int) (ite s9 s122 s177)) -[GOOD] (define-fun s179 () (Seq Int) (ite s3 s4 s178)) -[GOOD] (define-fun s180 () Bool (distinct s120 s179)) -[GOOD] (assert s47) -[GOOD] (assert s54) -[GOOD] (assert s62) -[GOOD] (assert s70) -[GOOD] (assert s78) -[GOOD] (assert s86) -[GOOD] (assert s94) -[GOOD] (assert s102) -[GOOD] (assert s110) -[GOOD] (assert s118) -[GOOD] (assert s124) -[GOOD] (assert s128) -[GOOD] (assert s133) -[GOOD] (assert s138) -[GOOD] (assert s143) -[GOOD] (assert s148) -[GOOD] (assert s153) -[GOOD] (assert s158) -[GOOD] (assert s163) -[GOOD] (assert s168) -[GOOD] (assert s180) +[GOOD] (define-fun s75 () (Seq Int) (seq.++ s72 s74)) +[GOOD] (define-fun s76 () (Seq Int) (ite s9 s4 s75)) +[GOOD] (define-fun s77 () Int (seq.nth s0 s2)) +[GOOD] (define-fun s78 () (Seq Int) (seq.unit s77)) +[GOOD] (define-fun s79 () (Seq Int) (seq.++ s76 s78)) +[GOOD] (define-fun s80 () (Seq Int) (ite s3 s4 s79)) +[GOOD] (define-fun s81 () (Seq Int) (seq.++ s74 s78)) +[GOOD] (define-fun s82 () (Seq Int) (seq.++ s70 s81)) +[GOOD] (define-fun s83 () (Seq Int) (seq.++ s66 s82)) +[GOOD] (define-fun s84 () (Seq Int) (seq.++ s62 s83)) +[GOOD] (define-fun s85 () (Seq Int) (seq.++ s58 s84)) +[GOOD] (define-fun s86 () (Seq Int) (seq.++ s54 s85)) +[GOOD] (define-fun s87 () (Seq Int) (seq.++ s50 s86)) +[GOOD] (define-fun s88 () (Seq Int) (seq.++ s46 s87)) +[GOOD] (define-fun s89 () (Seq Int) (seq.++ s43 s88)) +[GOOD] (define-fun s90 () (Seq Int) (ite s41 s88 s89)) +[GOOD] (define-fun s91 () (Seq Int) (ite s37 s87 s90)) +[GOOD] (define-fun s92 () (Seq Int) (ite s33 s86 s91)) +[GOOD] (define-fun s93 () (Seq Int) (ite s29 s85 s92)) +[GOOD] (define-fun s94 () (Seq Int) (ite s25 s84 s93)) +[GOOD] (define-fun s95 () (Seq Int) (ite s21 s83 s94)) +[GOOD] (define-fun s96 () (Seq Int) (ite s17 s82 s95)) +[GOOD] (define-fun s97 () (Seq Int) (ite s13 s81 s96)) +[GOOD] (define-fun s98 () (Seq Int) (ite s9 s78 s97)) +[GOOD] (define-fun s99 () (Seq Int) (ite s3 s4 s98)) +[GOOD] (define-fun s100 () Bool (distinct s80 s99)) +[GOOD] (assert s100) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/seqExamples2.gold b/SBVTestSuite/GoldFiles/seqExamples2.gold --- a/SBVTestSuite/GoldFiles/seqExamples2.gold +++ b/SBVTestSuite/GoldFiles/seqExamples2.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/seqExamples3.gold b/SBVTestSuite/GoldFiles/seqExamples3.gold --- a/SBVTestSuite/GoldFiles/seqExamples3.gold +++ b/SBVTestSuite/GoldFiles/seqExamples3.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/seqExamples4.gold b/SBVTestSuite/GoldFiles/seqExamples4.gold --- a/SBVTestSuite/GoldFiles/seqExamples4.gold +++ b/SBVTestSuite/GoldFiles/seqExamples4.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/seqExamples5.gold b/SBVTestSuite/GoldFiles/seqExamples5.gold --- a/SBVTestSuite/GoldFiles/seqExamples5.gold +++ b/SBVTestSuite/GoldFiles/seqExamples5.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/seqExamples6.gold b/SBVTestSuite/GoldFiles/seqExamples6.gold --- a/SBVTestSuite/GoldFiles/seqExamples6.gold +++ b/SBVTestSuite/GoldFiles/seqExamples6.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/seqExamples7.gold b/SBVTestSuite/GoldFiles/seqExamples7.gold --- a/SBVTestSuite/GoldFiles/seqExamples7.gold +++ b/SBVTestSuite/GoldFiles/seqExamples7.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/seqExamples8.gold b/SBVTestSuite/GoldFiles/seqExamples8.gold --- a/SBVTestSuite/GoldFiles/seqExamples8.gold +++ b/SBVTestSuite/GoldFiles/seqExamples8.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/set_compl1.gold b/SBVTestSuite/GoldFiles/set_compl1.gold --- a/SBVTestSuite/GoldFiles/set_compl1.gold +++ b/SBVTestSuite/GoldFiles/set_compl1.gold @@ -35,7 +35,7 @@ true) #x6f true))) -[GOOD] (define-fun s3 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) +[GOOD] (define-fun s3 () (Array (_ BitVec 8) Bool) (complement s0)) [SEND] (get-value (s3)) [RECV] ((s3 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) true) #x65 @@ -46,7 +46,7 @@ false) #x6f false))) -[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) ((_ map not) s3)) +[GOOD] (define-fun s4 () (Array (_ BitVec 8) Bool) (complement s3)) [SEND] (get-value (s4)) [RECV] ((s4 (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) false) #x65 @@ -57,10 +57,10 @@ true) #x6f true))) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) ((_ map and) s3 s0)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (intersection s3 s0)) [SEND] (get-value (s5)) [RECV] ((s5 ((as const (Array (_ BitVec 8) Bool)) false))) -[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((_ map or) s3 s0)) +[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (union s3 s0)) [SEND] (get-value (s6)) [RECV] ((s6 ((as const (Array (_ BitVec 8) Bool)) true))) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/set_delete1.gold b/SBVTestSuite/GoldFiles/set_delete1.gold --- a/SBVTestSuite/GoldFiles/set_delete1.gold +++ b/SBVTestSuite/GoldFiles/set_delete1.gold @@ -54,7 +54,7 @@ true) #x65 false))) -[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) +[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (complement s1)) [GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (store s7 s0 false)) [SEND] (get-value (s8)) [RECV] ((s8 (store (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) true) diff --git a/SBVTestSuite/GoldFiles/set_diff1.gold b/SBVTestSuite/GoldFiles/set_diff1.gold --- a/SBVTestSuite/GoldFiles/set_diff1.gold +++ b/SBVTestSuite/GoldFiles/set_diff1.gold @@ -32,18 +32,18 @@ [RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) [SEND] (get-value (s1)) [RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (difference s0 s1)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (setminus s0 s1)) [SEND] (get-value (s5)) [RECV] ((s5 ((as const (Array (_ BitVec 8) Bool)) false))) -[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) -[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (difference s0 s6)) +[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1)) +[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (setminus s0 s6)) [SEND] (get-value (s7)) [RECV] ((s7 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) -[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) -[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (difference s8 s1)) +[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0)) +[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (setminus s8 s1)) [SEND] (get-value (s9)) [RECV] ((s9 (store ((as const (Array (_ BitVec 8) Bool)) true) #x61 false))) -[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (difference s8 s6)) +[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (setminus s8 s6)) [SEND] (get-value (s10)) [RECV] ((s10 ((as const (Array (_ BitVec 8) Bool)) false))) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/set_disj1.gold b/SBVTestSuite/GoldFiles/set_disj1.gold --- a/SBVTestSuite/GoldFiles/set_disj1.gold +++ b/SBVTestSuite/GoldFiles/set_disj1.gold @@ -33,21 +33,21 @@ [SEND] (get-value (s1)) [RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) [GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((as const (Array (_ BitVec 8) Bool)) false)) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) ((_ map and) s0 s1)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (intersection s0 s1)) [GOOD] (define-fun s7 () Bool (= s5 s6)) [SEND] (get-value (s7)) [RECV] ((s7 false)) -[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) -[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) ((_ map and) s0 s8)) +[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s1)) +[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (intersection s0 s8)) [GOOD] (define-fun s10 () Bool (= s9 s6)) [SEND] (get-value (s10)) [RECV] ((s10 true)) -[GOOD] (define-fun s11 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) -[GOOD] (define-fun s12 () (Array (_ BitVec 8) Bool) ((_ map and) s11 s1)) +[GOOD] (define-fun s11 () (Array (_ BitVec 8) Bool) (complement s0)) +[GOOD] (define-fun s12 () (Array (_ BitVec 8) Bool) (intersection s11 s1)) [GOOD] (define-fun s13 () Bool (= s12 s6)) [SEND] (get-value (s13)) [RECV] ((s13 true)) -[GOOD] (define-fun s14 () (Array (_ BitVec 8) Bool) ((_ map and) s11 s8)) +[GOOD] (define-fun s14 () (Array (_ BitVec 8) Bool) (intersection s11 s8)) [GOOD] (define-fun s15 () Bool (= s14 s6)) [SEND] (get-value (s15)) [RECV] ((s15 false)) diff --git a/SBVTestSuite/GoldFiles/set_empty1.gold b/SBVTestSuite/GoldFiles/set_empty1.gold --- a/SBVTestSuite/GoldFiles/set_empty1.gold +++ b/SBVTestSuite/GoldFiles/set_empty1.gold @@ -39,7 +39,7 @@ [GOOD] (define-fun s4 () Bool (= s0 s3)) [SEND] (get-value (s4)) [RECV] ((s4 false)) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (complement s0)) [GOOD] (define-fun s6 () Bool (= s5 s3)) [SEND] (get-value (s6)) [RECV] ((s6 false)) diff --git a/SBVTestSuite/GoldFiles/set_full1.gold b/SBVTestSuite/GoldFiles/set_full1.gold --- a/SBVTestSuite/GoldFiles/set_full1.gold +++ b/SBVTestSuite/GoldFiles/set_full1.gold @@ -39,7 +39,7 @@ [GOOD] (define-fun s4 () Bool (= s0 s3)) [SEND] (get-value (s4)) [RECV] ((s4 false)) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (complement s0)) [GOOD] (define-fun s6 () Bool (= s5 s3)) [SEND] (get-value (s6)) [RECV] ((s6 false)) diff --git a/SBVTestSuite/GoldFiles/set_insert1.gold b/SBVTestSuite/GoldFiles/set_insert1.gold --- a/SBVTestSuite/GoldFiles/set_insert1.gold +++ b/SBVTestSuite/GoldFiles/set_insert1.gold @@ -54,7 +54,7 @@ true) #x65 true))) -[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) +[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (complement s1)) [GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (store s7 s0 true)) [SEND] (get-value (s8)) [RECV] ((s8 (store (store (store (store (store ((as const (Array (_ BitVec 8) Bool)) true) diff --git a/SBVTestSuite/GoldFiles/set_intersect1.gold b/SBVTestSuite/GoldFiles/set_intersect1.gold --- a/SBVTestSuite/GoldFiles/set_intersect1.gold +++ b/SBVTestSuite/GoldFiles/set_intersect1.gold @@ -32,18 +32,18 @@ [RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) [SEND] (get-value (s1)) [RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) ((_ map and) s0 s1)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (intersection s0 s1)) [SEND] (get-value (s5)) [RECV] ((s5 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) -[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) -[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) ((_ map and) s0 s6)) +[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1)) +[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (intersection s0 s6)) [SEND] (get-value (s7)) [RECV] ((s7 ((as const (Array (_ BitVec 8) Bool)) false))) -[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) -[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) ((_ map and) s8 s1)) +[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0)) +[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (intersection s8 s1)) [SEND] (get-value (s9)) [RECV] ((s9 ((as const (Array (_ BitVec 8) Bool)) false))) -[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) ((_ map and) s8 s6)) +[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (intersection s8 s6)) [SEND] (get-value (s10)) [RECV] ((s10 (store ((as const (Array (_ BitVec 8) Bool)) true) #x61 false))) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/set_member1.gold b/SBVTestSuite/GoldFiles/set_member1.gold --- a/SBVTestSuite/GoldFiles/set_member1.gold +++ b/SBVTestSuite/GoldFiles/set_member1.gold @@ -44,7 +44,7 @@ [GOOD] (define-fun s6 () Bool (select s1 s0)) [SEND] (get-value (s6)) [RECV] ((s6 true)) -[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) +[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (complement s1)) [GOOD] (define-fun s8 () Bool (select s7 s0)) [SEND] (get-value (s8)) [RECV] ((s8 false)) diff --git a/SBVTestSuite/GoldFiles/set_notMember1.gold b/SBVTestSuite/GoldFiles/set_notMember1.gold --- a/SBVTestSuite/GoldFiles/set_notMember1.gold +++ b/SBVTestSuite/GoldFiles/set_notMember1.gold @@ -45,7 +45,7 @@ [GOOD] (define-fun s7 () Bool (not s6)) [SEND] (get-value (s7)) [RECV] ((s7 false)) -[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) +[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s1)) [GOOD] (define-fun s9 () Bool (select s8 s0)) [GOOD] (define-fun s10 () Bool (not s9)) [SEND] (get-value (s10)) diff --git a/SBVTestSuite/GoldFiles/set_psubset1.gold b/SBVTestSuite/GoldFiles/set_psubset1.gold --- a/SBVTestSuite/GoldFiles/set_psubset1.gold +++ b/SBVTestSuite/GoldFiles/set_psubset1.gold @@ -38,14 +38,14 @@ [GOOD] (define-fun s8 () Bool (and s5 s7)) [SEND] (get-value (s8)) [RECV] ((s8 false)) -[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) +[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (complement s1)) [GOOD] (define-fun s10 () Bool (subset s0 s9)) [GOOD] (define-fun s11 () Bool (= s0 s9)) [GOOD] (define-fun s12 () Bool (not s11)) [GOOD] (define-fun s13 () Bool (and s10 s12)) [SEND] (get-value (s13)) [RECV] ((s13 false)) -[GOOD] (define-fun s14 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) +[GOOD] (define-fun s14 () (Array (_ BitVec 8) Bool) (complement s0)) [GOOD] (define-fun s15 () Bool (subset s14 s1)) [GOOD] (define-fun s16 () Bool (= s14 s1)) [GOOD] (define-fun s17 () Bool (not s16)) diff --git a/SBVTestSuite/GoldFiles/set_subset1.gold b/SBVTestSuite/GoldFiles/set_subset1.gold --- a/SBVTestSuite/GoldFiles/set_subset1.gold +++ b/SBVTestSuite/GoldFiles/set_subset1.gold @@ -35,11 +35,11 @@ [GOOD] (define-fun s5 () Bool (subset s0 s1)) [SEND] (get-value (s5)) [RECV] ((s5 true)) -[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) +[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1)) [GOOD] (define-fun s7 () Bool (subset s0 s6)) [SEND] (get-value (s7)) [RECV] ((s7 false)) -[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) +[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0)) [GOOD] (define-fun s9 () Bool (subset s8 s1)) [SEND] (get-value (s9)) [RECV] ((s9 false)) diff --git a/SBVTestSuite/GoldFiles/set_union1.gold b/SBVTestSuite/GoldFiles/set_union1.gold --- a/SBVTestSuite/GoldFiles/set_union1.gold +++ b/SBVTestSuite/GoldFiles/set_union1.gold @@ -32,18 +32,18 @@ [RECV] ((s0 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) [SEND] (get-value (s1)) [RECV] ((s1 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) -[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) ((_ map or) s0 s1)) +[GOOD] (define-fun s5 () (Array (_ BitVec 8) Bool) (union s0 s1)) [SEND] (get-value (s5)) [RECV] ((s5 (store ((as const (Array (_ BitVec 8) Bool)) false) #x61 true))) -[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) ((_ map not) s1)) -[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) ((_ map or) s0 s6)) +[GOOD] (define-fun s6 () (Array (_ BitVec 8) Bool) (complement s1)) +[GOOD] (define-fun s7 () (Array (_ BitVec 8) Bool) (union s0 s6)) [SEND] (get-value (s7)) [RECV] ((s7 ((as const (Array (_ BitVec 8) Bool)) true))) -[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) ((_ map not) s0)) -[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) ((_ map or) s8 s1)) +[GOOD] (define-fun s8 () (Array (_ BitVec 8) Bool) (complement s0)) +[GOOD] (define-fun s9 () (Array (_ BitVec 8) Bool) (union s8 s1)) [SEND] (get-value (s9)) [RECV] ((s9 ((as const (Array (_ BitVec 8) Bool)) true))) -[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) ((_ map or) s8 s6)) +[GOOD] (define-fun s10 () (Array (_ BitVec 8) Bool) (union s8 s6)) [SEND] (get-value (s10)) [RECV] ((s10 (store ((as const (Array (_ BitVec 8) Bool)) true) #x61 false))) *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/sort.gold b/SBVTestSuite/GoldFiles/sort.gold --- a/SBVTestSuite/GoldFiles/sort.gold +++ b/SBVTestSuite/GoldFiles/sort.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -19,15 +19,6 @@ [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" -[GOOD] (declare-fun s25 () Int) ; tracks user variable "__internal_sbv_s25" -[GOOD] (declare-fun s34 () Int) ; tracks user variable "__internal_sbv_s34" -[GOOD] (declare-fun s40 () Int) ; tracks user variable "__internal_sbv_s40" -[GOOD] (declare-fun s53 () Int) ; tracks user variable "__internal_sbv_s53" -[GOOD] (declare-fun s66 () Int) ; tracks user variable "__internal_sbv_s66" -[GOOD] (declare-fun s89 () Int) ; tracks user variable "__internal_sbv_s89" -[GOOD] (declare-fun s95 () Int) ; tracks user variable "__internal_sbv_s95" -[GOOD] (declare-fun s108 () Int) ; tracks user variable "__internal_sbv_s108" -[GOOD] (declare-fun s121 () Int) ; tracks user variable "__internal_sbv_s121" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -53,165 +44,129 @@ [GOOD] (define-fun s22 () (Seq Int) (seq.extract s18 s16 s21)) [GOOD] (define-fun s23 () Int (seq.len s22)) [GOOD] (define-fun s24 () Bool (= s13 s23)) +[GOOD] (define-fun s25 () Int (seq.nth s22 s13)) [GOOD] (define-fun s26 () (Seq Int) (seq.unit s25)) -[GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s13 s16)) -[GOOD] (define-fun s28 () Bool (= s26 s27)) -[GOOD] (define-fun s29 () Bool (<= s23 s13)) -[GOOD] (define-fun s30 () Bool (or s28 s29)) -[GOOD] (define-fun s31 () (Seq Int) (ite s24 s15 s26)) -[GOOD] (define-fun s32 () Int (seq.len s31)) -[GOOD] (define-fun s33 () Bool (= s13 s32)) -[GOOD] (define-fun s35 () (Seq Int) (seq.unit s34)) -[GOOD] (define-fun s36 () (Seq Int) (seq.extract s18 s13 s16)) -[GOOD] (define-fun s37 () Bool (= s35 s36)) -[GOOD] (define-fun s38 () Bool (<= s19 s13)) -[GOOD] (define-fun s39 () Bool (or s37 s38)) -[GOOD] (define-fun s41 () (Seq Int) (seq.unit s40)) -[GOOD] (define-fun s42 () (Seq Int) (seq.extract s31 s13 s16)) -[GOOD] (define-fun s43 () Bool (= s41 s42)) -[GOOD] (define-fun s44 () Bool (<= s32 s13)) -[GOOD] (define-fun s45 () Bool (or s43 s44)) -[GOOD] (define-fun s46 () Bool (< s34 s40)) -[GOOD] (define-fun s47 () Int (- s32 s16)) -[GOOD] (define-fun s48 () (Seq Int) (seq.extract s31 s16 s47)) -[GOOD] (define-fun s49 () (Seq Int) (seq.++ s41 s48)) -[GOOD] (define-fun s50 () (Seq Int) (seq.++ s35 s49)) -[GOOD] (define-fun s51 () Int (seq.len s48)) -[GOOD] (define-fun s52 () Bool (= s13 s51)) -[GOOD] (define-fun s54 () (Seq Int) (seq.unit s53)) -[GOOD] (define-fun s55 () (Seq Int) (seq.extract s48 s13 s16)) -[GOOD] (define-fun s56 () Bool (= s54 s55)) -[GOOD] (define-fun s57 () Bool (<= s51 s13)) -[GOOD] (define-fun s58 () Bool (or s56 s57)) -[GOOD] (define-fun s59 () Bool (< s34 s53)) -[GOOD] (define-fun s60 () Int (- s51 s16)) -[GOOD] (define-fun s61 () (Seq Int) (seq.extract s48 s16 s60)) -[GOOD] (define-fun s62 () (Seq Int) (seq.++ s54 s61)) -[GOOD] (define-fun s63 () (Seq Int) (seq.++ s35 s62)) -[GOOD] (define-fun s64 () Int (seq.len s61)) -[GOOD] (define-fun s65 () Bool (= s13 s64)) -[GOOD] (define-fun s67 () (Seq Int) (seq.unit s66)) -[GOOD] (define-fun s68 () (Seq Int) (seq.extract s61 s13 s16)) -[GOOD] (define-fun s69 () Bool (= s67 s68)) -[GOOD] (define-fun s70 () Bool (<= s64 s13)) -[GOOD] (define-fun s71 () Bool (or s69 s70)) -[GOOD] (define-fun s72 () Bool (< s34 s66)) -[GOOD] (define-fun s73 () Int (- s64 s16)) -[GOOD] (define-fun s74 () (Seq Int) (seq.extract s61 s16 s73)) -[GOOD] (define-fun s75 () (Seq Int) (seq.++ s67 s74)) -[GOOD] (define-fun s76 () (Seq Int) (seq.++ s35 s75)) -[GOOD] (define-fun s77 () (Seq Int) (seq.++ s67 s35)) -[GOOD] (define-fun s78 () (Seq Int) (ite s72 s76 s77)) -[GOOD] (define-fun s79 () (Seq Int) (ite s65 s35 s78)) -[GOOD] (define-fun s80 () (Seq Int) (seq.++ s54 s79)) -[GOOD] (define-fun s81 () (Seq Int) (ite s59 s63 s80)) -[GOOD] (define-fun s82 () (Seq Int) (ite s52 s35 s81)) -[GOOD] (define-fun s83 () (Seq Int) (seq.++ s41 s82)) -[GOOD] (define-fun s84 () (Seq Int) (ite s46 s50 s83)) -[GOOD] (define-fun s85 () (Seq Int) (ite s33 s35 s84)) -[GOOD] (define-fun s86 () (Seq Int) (ite s20 s15 s85)) -[GOOD] (define-fun s87 () Int (seq.len s86)) +[GOOD] (define-fun s27 () (Seq Int) (ite s24 s15 s26)) +[GOOD] (define-fun s28 () Int (seq.len s27)) +[GOOD] (define-fun s29 () Bool (= s13 s28)) +[GOOD] (define-fun s30 () Int (seq.nth s18 s13)) +[GOOD] (define-fun s31 () (Seq Int) (seq.unit s30)) +[GOOD] (define-fun s32 () Int (seq.nth s27 s13)) +[GOOD] (define-fun s33 () Bool (< s30 s32)) +[GOOD] (define-fun s34 () (Seq Int) (seq.unit s32)) +[GOOD] (define-fun s35 () Int (- s28 s16)) +[GOOD] (define-fun s36 () (Seq Int) (seq.extract s27 s16 s35)) +[GOOD] (define-fun s37 () (Seq Int) (seq.++ s34 s36)) +[GOOD] (define-fun s38 () (Seq Int) (seq.++ s31 s37)) +[GOOD] (define-fun s39 () Int (seq.len s36)) +[GOOD] (define-fun s40 () Bool (= s13 s39)) +[GOOD] (define-fun s41 () Int (seq.nth s36 s13)) +[GOOD] (define-fun s42 () Bool (< s30 s41)) +[GOOD] (define-fun s43 () (Seq Int) (seq.unit s41)) +[GOOD] (define-fun s44 () Int (- s39 s16)) +[GOOD] (define-fun s45 () (Seq Int) (seq.extract s36 s16 s44)) +[GOOD] (define-fun s46 () (Seq Int) (seq.++ s43 s45)) +[GOOD] (define-fun s47 () (Seq Int) (seq.++ s31 s46)) +[GOOD] (define-fun s48 () Int (seq.len s45)) +[GOOD] (define-fun s49 () Bool (= s13 s48)) +[GOOD] (define-fun s50 () Int (seq.nth s45 s13)) +[GOOD] (define-fun s51 () Bool (< s30 s50)) +[GOOD] (define-fun s52 () (Seq Int) (seq.unit s50)) +[GOOD] (define-fun s53 () Int (- s48 s16)) +[GOOD] (define-fun s54 () (Seq Int) (seq.extract s45 s16 s53)) +[GOOD] (define-fun s55 () (Seq Int) (seq.++ s52 s54)) +[GOOD] (define-fun s56 () (Seq Int) (seq.++ s31 s55)) +[GOOD] (define-fun s57 () (Seq Int) (seq.++ s52 s31)) +[GOOD] (define-fun s58 () (Seq Int) (ite s51 s56 s57)) +[GOOD] (define-fun s59 () (Seq Int) (ite s49 s31 s58)) +[GOOD] (define-fun s60 () (Seq Int) (seq.++ s43 s59)) +[GOOD] (define-fun s61 () (Seq Int) (ite s42 s47 s60)) +[GOOD] (define-fun s62 () (Seq Int) (ite s40 s31 s61)) +[GOOD] (define-fun s63 () (Seq Int) (seq.++ s34 s62)) +[GOOD] (define-fun s64 () (Seq Int) (ite s33 s38 s63)) +[GOOD] (define-fun s65 () (Seq Int) (ite s29 s31 s64)) +[GOOD] (define-fun s66 () (Seq Int) (ite s20 s15 s65)) +[GOOD] (define-fun s67 () Int (seq.len s66)) +[GOOD] (define-fun s68 () Bool (= s13 s67)) +[GOOD] (define-fun s69 () Int (seq.nth s11 s13)) +[GOOD] (define-fun s70 () (Seq Int) (seq.unit s69)) +[GOOD] (define-fun s71 () Int (seq.nth s66 s13)) +[GOOD] (define-fun s72 () Bool (< s69 s71)) +[GOOD] (define-fun s73 () (Seq Int) (seq.unit s71)) +[GOOD] (define-fun s74 () Int (- s67 s16)) +[GOOD] (define-fun s75 () (Seq Int) (seq.extract s66 s16 s74)) +[GOOD] (define-fun s76 () (Seq Int) (seq.++ s73 s75)) +[GOOD] (define-fun s77 () (Seq Int) (seq.++ s70 s76)) +[GOOD] (define-fun s78 () Int (seq.len s75)) +[GOOD] (define-fun s79 () Bool (= s13 s78)) +[GOOD] (define-fun s80 () Int (seq.nth s75 s13)) +[GOOD] (define-fun s81 () Bool (< s69 s80)) +[GOOD] (define-fun s82 () (Seq Int) (seq.unit s80)) +[GOOD] (define-fun s83 () Int (- s78 s16)) +[GOOD] (define-fun s84 () (Seq Int) (seq.extract s75 s16 s83)) +[GOOD] (define-fun s85 () (Seq Int) (seq.++ s82 s84)) +[GOOD] (define-fun s86 () (Seq Int) (seq.++ s70 s85)) +[GOOD] (define-fun s87 () Int (seq.len s84)) [GOOD] (define-fun s88 () Bool (= s13 s87)) -[GOOD] (define-fun s90 () (Seq Int) (seq.unit s89)) -[GOOD] (define-fun s91 () (Seq Int) (seq.extract s11 s13 s16)) -[GOOD] (define-fun s92 () Bool (= s90 s91)) -[GOOD] (define-fun s93 () Bool (<= s12 s13)) -[GOOD] (define-fun s94 () Bool (or s92 s93)) -[GOOD] (define-fun s96 () (Seq Int) (seq.unit s95)) -[GOOD] (define-fun s97 () (Seq Int) (seq.extract s86 s13 s16)) -[GOOD] (define-fun s98 () Bool (= s96 s97)) -[GOOD] (define-fun s99 () Bool (<= s87 s13)) -[GOOD] (define-fun s100 () Bool (or s98 s99)) -[GOOD] (define-fun s101 () Bool (< s89 s95)) -[GOOD] (define-fun s102 () Int (- s87 s16)) -[GOOD] (define-fun s103 () (Seq Int) (seq.extract s86 s16 s102)) -[GOOD] (define-fun s104 () (Seq Int) (seq.++ s96 s103)) -[GOOD] (define-fun s105 () (Seq Int) (seq.++ s90 s104)) -[GOOD] (define-fun s106 () Int (seq.len s103)) -[GOOD] (define-fun s107 () Bool (= s13 s106)) -[GOOD] (define-fun s109 () (Seq Int) (seq.unit s108)) -[GOOD] (define-fun s110 () (Seq Int) (seq.extract s103 s13 s16)) -[GOOD] (define-fun s111 () Bool (= s109 s110)) -[GOOD] (define-fun s112 () Bool (<= s106 s13)) -[GOOD] (define-fun s113 () Bool (or s111 s112)) -[GOOD] (define-fun s114 () Bool (< s89 s108)) -[GOOD] (define-fun s115 () Int (- s106 s16)) -[GOOD] (define-fun s116 () (Seq Int) (seq.extract s103 s16 s115)) -[GOOD] (define-fun s117 () (Seq Int) (seq.++ s109 s116)) -[GOOD] (define-fun s118 () (Seq Int) (seq.++ s90 s117)) -[GOOD] (define-fun s119 () Int (seq.len s116)) -[GOOD] (define-fun s120 () Bool (= s13 s119)) -[GOOD] (define-fun s122 () (Seq Int) (seq.unit s121)) -[GOOD] (define-fun s123 () (Seq Int) (seq.extract s116 s13 s16)) -[GOOD] (define-fun s124 () Bool (= s122 s123)) -[GOOD] (define-fun s125 () Bool (<= s119 s13)) -[GOOD] (define-fun s126 () Bool (or s124 s125)) -[GOOD] (define-fun s127 () Bool (< s89 s121)) -[GOOD] (define-fun s128 () Int (- s119 s16)) -[GOOD] (define-fun s129 () (Seq Int) (seq.extract s116 s16 s128)) -[GOOD] (define-fun s130 () (Seq Int) (seq.++ s122 s129)) -[GOOD] (define-fun s131 () (Seq Int) (seq.++ s90 s130)) -[GOOD] (define-fun s132 () (Seq Int) (seq.++ s122 s90)) -[GOOD] (define-fun s133 () (Seq Int) (ite s127 s131 s132)) -[GOOD] (define-fun s134 () (Seq Int) (ite s120 s90 s133)) -[GOOD] (define-fun s135 () (Seq Int) (seq.++ s109 s134)) -[GOOD] (define-fun s136 () (Seq Int) (ite s114 s118 s135)) -[GOOD] (define-fun s137 () (Seq Int) (ite s107 s90 s136)) -[GOOD] (define-fun s138 () (Seq Int) (seq.++ s96 s137)) -[GOOD] (define-fun s139 () (Seq Int) (ite s101 s105 s138)) -[GOOD] (define-fun s140 () (Seq Int) (ite s88 s90 s139)) -[GOOD] (define-fun s141 () (Seq Int) (ite s14 s15 s140)) -[GOOD] (define-fun s142 () Bool (= s11 s141)) -[GOOD] (define-fun s143 () Bool (or s6 s142)) -[GOOD] (define-fun s144 () Bool (<= s0 s2)) -[GOOD] (define-fun s145 () Bool (<= s2 s1)) -[GOOD] (define-fun s146 () Bool (and s144 s145)) -[GOOD] (define-fun s147 () Bool (not s146)) -[GOOD] (define-fun s148 () (Seq Int) (seq.++ s9 s8)) -[GOOD] (define-fun s149 () (Seq Int) (seq.++ s7 s148)) -[GOOD] (define-fun s150 () Bool (= s141 s149)) -[GOOD] (define-fun s151 () Bool (or s147 s150)) -[GOOD] (define-fun s152 () Bool (<= s1 s0)) -[GOOD] (define-fun s153 () Bool (and s144 s152)) -[GOOD] (define-fun s154 () Bool (not s153)) -[GOOD] (define-fun s155 () (Seq Int) (seq.++ s7 s9)) -[GOOD] (define-fun s156 () (Seq Int) (seq.++ s8 s155)) -[GOOD] (define-fun s157 () Bool (= s141 s156)) -[GOOD] (define-fun s158 () Bool (or s154 s157)) -[GOOD] (define-fun s159 () Bool (<= s2 s0)) -[GOOD] (define-fun s160 () Bool (and s4 s159)) -[GOOD] (define-fun s161 () Bool (not s160)) -[GOOD] (define-fun s162 () (Seq Int) (seq.++ s9 s7)) -[GOOD] (define-fun s163 () (Seq Int) (seq.++ s8 s162)) -[GOOD] (define-fun s164 () Bool (= s141 s163)) -[GOOD] (define-fun s165 () Bool (or s161 s164)) -[GOOD] (define-fun s166 () Bool (and s3 s159)) -[GOOD] (define-fun s167 () Bool (not s166)) -[GOOD] (define-fun s168 () (Seq Int) (seq.++ s7 s8)) -[GOOD] (define-fun s169 () (Seq Int) (seq.++ s9 s168)) -[GOOD] (define-fun s170 () Bool (= s141 s169)) -[GOOD] (define-fun s171 () Bool (or s167 s170)) -[GOOD] (define-fun s172 () Bool (and s145 s152)) -[GOOD] (define-fun s173 () Bool (not s172)) -[GOOD] (define-fun s174 () (Seq Int) (seq.++ s8 s7)) -[GOOD] (define-fun s175 () (Seq Int) (seq.++ s9 s174)) -[GOOD] (define-fun s176 () Bool (= s141 s175)) -[GOOD] (define-fun s177 () Bool (or s173 s176)) -[GOOD] (assert s30) -[GOOD] (assert s39) -[GOOD] (assert s45) -[GOOD] (assert s58) -[GOOD] (assert s71) -[GOOD] (assert s94) -[GOOD] (assert s100) -[GOOD] (assert s113) -[GOOD] (assert s126) -[GOOD] (assert s143) -[GOOD] (assert s151) -[GOOD] (assert s158) -[GOOD] (assert s165) -[GOOD] (assert s171) -[GOOD] (assert s177) +[GOOD] (define-fun s89 () Int (seq.nth s84 s13)) +[GOOD] (define-fun s90 () Bool (< s69 s89)) +[GOOD] (define-fun s91 () (Seq Int) (seq.unit s89)) +[GOOD] (define-fun s92 () Int (- s87 s16)) +[GOOD] (define-fun s93 () (Seq Int) (seq.extract s84 s16 s92)) +[GOOD] (define-fun s94 () (Seq Int) (seq.++ s91 s93)) +[GOOD] (define-fun s95 () (Seq Int) (seq.++ s70 s94)) +[GOOD] (define-fun s96 () (Seq Int) (seq.++ s91 s70)) +[GOOD] (define-fun s97 () (Seq Int) (ite s90 s95 s96)) +[GOOD] (define-fun s98 () (Seq Int) (ite s88 s70 s97)) +[GOOD] (define-fun s99 () (Seq Int) (seq.++ s82 s98)) +[GOOD] (define-fun s100 () (Seq Int) (ite s81 s86 s99)) +[GOOD] (define-fun s101 () (Seq Int) (ite s79 s70 s100)) +[GOOD] (define-fun s102 () (Seq Int) (seq.++ s73 s101)) +[GOOD] (define-fun s103 () (Seq Int) (ite s72 s77 s102)) +[GOOD] (define-fun s104 () (Seq Int) (ite s68 s70 s103)) +[GOOD] (define-fun s105 () (Seq Int) (ite s14 s15 s104)) +[GOOD] (define-fun s106 () Bool (= s11 s105)) +[GOOD] (define-fun s107 () Bool (or s6 s106)) +[GOOD] (define-fun s108 () Bool (<= s0 s2)) +[GOOD] (define-fun s109 () Bool (<= s2 s1)) +[GOOD] (define-fun s110 () Bool (and s108 s109)) +[GOOD] (define-fun s111 () Bool (not s110)) +[GOOD] (define-fun s112 () (Seq Int) (seq.++ s9 s8)) +[GOOD] (define-fun s113 () (Seq Int) (seq.++ s7 s112)) +[GOOD] (define-fun s114 () Bool (= s105 s113)) +[GOOD] (define-fun s115 () Bool (or s111 s114)) +[GOOD] (define-fun s116 () Bool (<= s1 s0)) +[GOOD] (define-fun s117 () Bool (and s108 s116)) +[GOOD] (define-fun s118 () Bool (not s117)) +[GOOD] (define-fun s119 () (Seq Int) (seq.++ s7 s9)) +[GOOD] (define-fun s120 () (Seq Int) (seq.++ s8 s119)) +[GOOD] (define-fun s121 () Bool (= s105 s120)) +[GOOD] (define-fun s122 () Bool (or s118 s121)) +[GOOD] (define-fun s123 () Bool (<= s2 s0)) +[GOOD] (define-fun s124 () Bool (and s4 s123)) +[GOOD] (define-fun s125 () Bool (not s124)) +[GOOD] (define-fun s126 () (Seq Int) (seq.++ s9 s7)) +[GOOD] (define-fun s127 () (Seq Int) (seq.++ s8 s126)) +[GOOD] (define-fun s128 () Bool (= s105 s127)) +[GOOD] (define-fun s129 () Bool (or s125 s128)) +[GOOD] (define-fun s130 () Bool (and s3 s123)) +[GOOD] (define-fun s131 () Bool (not s130)) +[GOOD] (define-fun s132 () (Seq Int) (seq.++ s7 s8)) +[GOOD] (define-fun s133 () (Seq Int) (seq.++ s9 s132)) +[GOOD] (define-fun s134 () Bool (= s105 s133)) +[GOOD] (define-fun s135 () Bool (or s131 s134)) +[GOOD] (define-fun s136 () Bool (and s109 s116)) +[GOOD] (define-fun s137 () Bool (not s136)) +[GOOD] (define-fun s138 () (Seq Int) (seq.++ s8 s7)) +[GOOD] (define-fun s139 () (Seq Int) (seq.++ s9 s138)) +[GOOD] (define-fun s140 () Bool (= s105 s139)) +[GOOD] (define-fun s141 () Bool (or s137 s140)) +[GOOD] (assert s107) +[GOOD] (assert s115) +[GOOD] (assert s122) +[GOOD] (assert s129) +[GOOD] (assert s135) +[GOOD] (assert s141) [SEND] (check-sat) [RECV] sat *** Solver : Z3 diff --git a/SBVTestSuite/GoldFiles/strExamples10.gold b/SBVTestSuite/GoldFiles/strExamples10.gold --- a/SBVTestSuite/GoldFiles/strExamples10.gold +++ b/SBVTestSuite/GoldFiles/strExamples10.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples11.gold b/SBVTestSuite/GoldFiles/strExamples11.gold --- a/SBVTestSuite/GoldFiles/strExamples11.gold +++ b/SBVTestSuite/GoldFiles/strExamples11.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples12.gold b/SBVTestSuite/GoldFiles/strExamples12.gold --- a/SBVTestSuite/GoldFiles/strExamples12.gold +++ b/SBVTestSuite/GoldFiles/strExamples12.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples13.gold b/SBVTestSuite/GoldFiles/strExamples13.gold --- a/SBVTestSuite/GoldFiles/strExamples13.gold +++ b/SBVTestSuite/GoldFiles/strExamples13.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples2.gold b/SBVTestSuite/GoldFiles/strExamples2.gold --- a/SBVTestSuite/GoldFiles/strExamples2.gold +++ b/SBVTestSuite/GoldFiles/strExamples2.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has strings, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples3.gold b/SBVTestSuite/GoldFiles/strExamples3.gold --- a/SBVTestSuite/GoldFiles/strExamples3.gold +++ b/SBVTestSuite/GoldFiles/strExamples3.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has strings, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples4.gold b/SBVTestSuite/GoldFiles/strExamples4.gold --- a/SBVTestSuite/GoldFiles/strExamples4.gold +++ b/SBVTestSuite/GoldFiles/strExamples4.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples5.gold b/SBVTestSuite/GoldFiles/strExamples5.gold --- a/SBVTestSuite/GoldFiles/strExamples5.gold +++ b/SBVTestSuite/GoldFiles/strExamples5.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has strings, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples6.gold b/SBVTestSuite/GoldFiles/strExamples6.gold --- a/SBVTestSuite/GoldFiles/strExamples6.gold +++ b/SBVTestSuite/GoldFiles/strExamples6.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has strings, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples7.gold b/SBVTestSuite/GoldFiles/strExamples7.gold --- a/SBVTestSuite/GoldFiles/strExamples7.gold +++ b/SBVTestSuite/GoldFiles/strExamples7.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has strings, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples8.gold b/SBVTestSuite/GoldFiles/strExamples8.gold --- a/SBVTestSuite/GoldFiles/strExamples8.gold +++ b/SBVTestSuite/GoldFiles/strExamples8.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/strExamples9.gold b/SBVTestSuite/GoldFiles/strExamples9.gold --- a/SBVTestSuite/GoldFiles/strExamples9.gold +++ b/SBVTestSuite/GoldFiles/strExamples9.gold @@ -5,7 +5,7 @@ [GOOD] (set-option :smtlib2_compliant true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-models true) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- diff --git a/SBVTestSuite/GoldFiles/sumMergeEither1.gold b/SBVTestSuite/GoldFiles/sumMergeEither1.gold --- a/SBVTestSuite/GoldFiles/sumMergeEither1.gold +++ b/SBVTestSuite/GoldFiles/sumMergeEither1.gold @@ -34,10 +34,10 @@ [SEND] (get-value (s0)) [RECV] ((s0 (left_SBVEither 0))) [SEND] (get-value (s1)) -[RECV] ((s1 (right_SBVEither false))) +[RECV] ((s1 (left_SBVEither 0))) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Left 0 :: Either Integer Bool),("s1",Right False :: Either Integer Bool),("s2",True :: Bool)], modelUIFuns = []} +MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Left 0 :: Either Integer Bool),("s1",Left 0 :: Either Integer Bool),("s2",False :: Bool)], modelUIFuns = []} DONE.*** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/sumMergeEither2.gold b/SBVTestSuite/GoldFiles/sumMergeEither2.gold --- a/SBVTestSuite/GoldFiles/sumMergeEither2.gold +++ b/SBVTestSuite/GoldFiles/sumMergeEither2.gold @@ -36,8 +36,8 @@ [SEND] (get-value (s1)) [RECV] ((s1 (right_SBVEither false))) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Right False :: Either Integer Bool),("s1",Right False :: Either Integer Bool),("s2",True :: Bool)], modelUIFuns = []} +MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Right False :: Either Integer Bool),("s1",Right False :: Either Integer Bool),("s2",False :: Bool)], modelUIFuns = []} DONE.*** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/sumMergeMaybe1.gold b/SBVTestSuite/GoldFiles/sumMergeMaybe1.gold --- a/SBVTestSuite/GoldFiles/sumMergeMaybe1.gold +++ b/SBVTestSuite/GoldFiles/sumMergeMaybe1.gold @@ -34,10 +34,10 @@ [SEND] (get-value (s0)) [RECV] ((s0 nothing_SBVMaybe)) [SEND] (get-value (s1)) -[RECV] ((s1 (just_SBVMaybe 0))) +[RECV] ((s1 nothing_SBVMaybe)) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Nothing :: Maybe Integer),("s1",Just 0 :: Maybe Integer),("s2",True :: Bool)], modelUIFuns = []} +MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Nothing :: Maybe Integer),("s1",Nothing :: Maybe Integer),("s2",False :: Bool)], modelUIFuns = []} DONE.*** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold b/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold --- a/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold +++ b/SBVTestSuite/GoldFiles/sumMergeMaybe2.gold @@ -36,8 +36,8 @@ [SEND] (get-value (s1)) [RECV] ((s1 (just_SBVMaybe 0))) [SEND] (get-value (s2)) -[RECV] ((s2 true)) +[RECV] ((s2 false)) -MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Just 0 :: Maybe Integer),("s1",Just 0 :: Maybe Integer),("s2",True :: Bool)], modelUIFuns = []} +MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("s0",Just 0 :: Maybe Integer),("s1",Just 0 :: Maybe Integer),("s2",False :: Bool)], modelUIFuns = []} DONE.*** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/tuple_enum.gold b/SBVTestSuite/GoldFiles/tuple_enum.gold --- a/SBVTestSuite/GoldFiles/tuple_enum.gold +++ b/SBVTestSuite/GoldFiles/tuple_enum.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] (declare-datatypes ((E 0)) (((A) (B) (C)))) [GOOD] (define-fun E_constrIndex ((x E)) Int @@ -19,19 +19,16 @@ (proj_2_SBVTuple2 T2)))))) [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- -[GOOD] (define-fun s5 () Int 1) -[GOOD] (define-fun s16 () Int 3) -[GOOD] (define-fun s20 () Int 2) -[GOOD] (define-fun s30 () Int 6) -[GOOD] (define-fun s34 () Int 4) -[GOOD] (define-fun s26 () E C) -[GOOD] (define-fun s12 () (Seq Bool) (seq.unit true)) +[GOOD] (define-fun s3 () Int 1) +[GOOD] (define-fun s11 () Int 3) +[GOOD] (define-fun s13 () Int 2) +[GOOD] (define-fun s20 () Int 6) +[GOOD] (define-fun s22 () Int 4) +[GOOD] (define-fun s16 () E C) +[GOOD] (define-fun s6 () (Seq Bool) (seq.unit true)) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq (SBVTuple2 E (Seq Bool)))) ; tracks user variable "v1" [GOOD] (declare-fun s1 () Bool) ; tracks user variable "q" -[GOOD] (declare-fun s3 () (SBVTuple2 E (Seq Bool))) ; tracks user variable "__internal_sbv_s3" -[GOOD] (declare-fun s18 () (SBVTuple2 E (Seq Bool))) ; tracks user variable "__internal_sbv_s18" -[GOOD] (declare-fun s32 () Bool) ; tracks user variable "__internal_sbv_s32" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- @@ -39,54 +36,39 @@ [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- [GOOD] (define-fun s2 () Bool (not s1)) -[GOOD] (define-fun s4 () (Seq (SBVTuple2 E (Seq Bool))) (seq.unit s3)) -[GOOD] (define-fun s6 () (Seq (SBVTuple2 E (Seq Bool))) (seq.extract s0 s5 s5)) -[GOOD] (define-fun s7 () Bool (= s4 s6)) -[GOOD] (define-fun s8 () Int (seq.len s0)) -[GOOD] (define-fun s9 () Bool (<= s8 s5)) -[GOOD] (define-fun s10 () Bool (or s7 s9)) -[GOOD] (define-fun s11 () (Seq Bool) (proj_2_SBVTuple2 s3)) -[GOOD] (define-fun s13 () (Seq Bool) (seq.unit s1)) -[GOOD] (define-fun s14 () (Seq Bool) (seq.++ s12 s13)) -[GOOD] (define-fun s15 () Bool (= s11 s14)) -[GOOD] (define-fun s17 () Bool (= s8 s16)) -[GOOD] (define-fun s19 () (Seq (SBVTuple2 E (Seq Bool))) (seq.unit s18)) -[GOOD] (define-fun s21 () (Seq (SBVTuple2 E (Seq Bool))) (seq.extract s0 s20 s5)) -[GOOD] (define-fun s22 () Bool (= s19 s21)) -[GOOD] (define-fun s23 () Bool (<= s8 s20)) -[GOOD] (define-fun s24 () Bool (or s22 s23)) -[GOOD] (define-fun s25 () E (proj_1_SBVTuple2 s18)) -[GOOD] (define-fun s27 () Bool (= s25 s26)) -[GOOD] (define-fun s28 () (Seq Bool) (proj_2_SBVTuple2 s18)) -[GOOD] (define-fun s29 () Int (seq.len s28)) -[GOOD] (define-fun s31 () Bool (= s29 s30)) -[GOOD] (define-fun s33 () (Seq Bool) (seq.unit s32)) -[GOOD] (define-fun s35 () (Seq Bool) (seq.extract s28 s34 s5)) -[GOOD] (define-fun s36 () Bool (= s33 s35)) -[GOOD] (define-fun s37 () Bool (<= s29 s34)) -[GOOD] (define-fun s38 () Bool (or s36 s37)) +[GOOD] (define-fun s4 () (SBVTuple2 E (Seq Bool)) (seq.nth s0 s3)) +[GOOD] (define-fun s5 () (Seq Bool) (proj_2_SBVTuple2 s4)) +[GOOD] (define-fun s7 () (Seq Bool) (seq.unit s1)) +[GOOD] (define-fun s8 () (Seq Bool) (seq.++ s6 s7)) +[GOOD] (define-fun s9 () Bool (= s5 s8)) +[GOOD] (define-fun s10 () Int (seq.len s0)) +[GOOD] (define-fun s12 () Bool (= s10 s11)) +[GOOD] (define-fun s14 () (SBVTuple2 E (Seq Bool)) (seq.nth s0 s13)) +[GOOD] (define-fun s15 () E (proj_1_SBVTuple2 s14)) +[GOOD] (define-fun s17 () Bool (= s15 s16)) +[GOOD] (define-fun s18 () (Seq Bool) (proj_2_SBVTuple2 s14)) +[GOOD] (define-fun s19 () Int (seq.len s18)) +[GOOD] (define-fun s21 () Bool (= s19 s20)) +[GOOD] (define-fun s23 () Bool (seq.nth s18 s22)) [GOOD] (assert s2) -[GOOD] (assert s10) -[GOOD] (assert s15) +[GOOD] (assert s9) +[GOOD] (assert s12) [GOOD] (assert s17) -[GOOD] (assert s24) -[GOOD] (assert s27) -[GOOD] (assert s31) -[GOOD] (assert s38) -[GOOD] (assert s32) +[GOOD] (assert s21) +[GOOD] (assert s23) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (declare-datatypes ((SBVTuple3 3)) ((par (T1 T2 T3) ((mkSBVTuple3 (proj_1_SBVTuple3 T1) (proj_2_SBVTuple3 T2) (proj_3_SBVTuple3 T3)))))) -[GOOD] (declare-fun s39 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E (_ BitVec 8) (_ FloatingPoint 8 24)))) -[GOOD] (define-fun s40 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E (_ BitVec 8) (_ FloatingPoint 8 24))) (mkSBVTuple2 #x05 (mkSBVTuple3 C #x41 ((_ to_fp 8 24) roundNearestTiesToEven (/ 8514437.0 1048576.0))))) -[GOOD] (define-fun s41 () Bool (= s39 s40)) -[GOOD] (assert s41) -[GOOD] (define-fun s42 () (Seq (SBVTuple2 E (Seq Bool))) (seq.++ (seq.unit (mkSBVTuple2 B (as seq.empty (Seq Bool)))) (seq.unit (mkSBVTuple2 A (seq.++ (seq.unit true) (seq.unit false)))) (seq.unit (mkSBVTuple2 C (seq.++ (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit true) (seq.unit false)))))) -[GOOD] (define-fun s43 () Bool (= s0 s42)) -[GOOD] (assert s43) +[GOOD] (declare-fun s24 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E (_ BitVec 8) (_ FloatingPoint 8 24)))) +[GOOD] (define-fun s25 () (SBVTuple2 (_ BitVec 8) (SBVTuple3 E (_ BitVec 8) (_ FloatingPoint 8 24))) (mkSBVTuple2 #x05 (mkSBVTuple3 C #x41 ((_ to_fp 8 24) roundNearestTiesToEven (/ 8514437.0 1048576.0))))) +[GOOD] (define-fun s26 () Bool (= s24 s25)) +[GOOD] (assert s26) +[GOOD] (define-fun s27 () (Seq (SBVTuple2 E (Seq Bool))) (seq.++ (seq.unit (mkSBVTuple2 B (as seq.empty (Seq Bool)))) (seq.unit (mkSBVTuple2 A (seq.++ (seq.unit true) (seq.unit false)))) (seq.unit (mkSBVTuple2 C (seq.++ (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit false) (seq.unit true) (seq.unit false)))))) +[GOOD] (define-fun s28 () Bool (= s0 s27)) +[GOOD] (assert s28) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -100,8 +82,8 @@ (seq.++ (seq.unit false) (seq.++ (seq.unit true) (seq.unit false)))))))))))) -[SEND] (get-value (s39)) -[RECV] ((s39 (mkSBVTuple2 #x05 (mkSBVTuple3 C #x41 (fp #b0 #x82 #b00000011110101110000101))))) +[SEND] (get-value (s24)) +[RECV] ((s24 (mkSBVTuple2 #x05 (mkSBVTuple3 C #x41 (fp #b0 #x82 #b00000011110101110000101))))) *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/tuple_list.gold b/SBVTestSuite/GoldFiles/tuple_list.gold --- a/SBVTestSuite/GoldFiles/tuple_list.gold +++ b/SBVTestSuite/GoldFiles/tuple_list.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) @@ -15,75 +15,44 @@ (proj_2_SBVTuple2 T2)))))) [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- -[GOOD] (define-fun s3 () Int 0) -[GOOD] (define-fun s4 () Int 1) -[GOOD] (define-fun s11 () Int 2) -[GOOD] (define-fun s30 () Int 4) -[GOOD] (define-fun s38 () Int 5) -[GOOD] (define-fun s28 () String "foo") -[GOOD] (define-fun s49 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.++ (seq.unit (mkSBVTuple2 2 (as seq.empty (Seq (SBVTuple2 Int String))))) (seq.unit (mkSBVTuple2 1 (seq.++ (seq.unit (mkSBVTuple2 3 "foo")) (seq.unit (mkSBVTuple2 0 "bar")) (seq.unit (mkSBVTuple2 (- 1) "baz")) (seq.unit (mkSBVTuple2 (- 2) "quux")) (seq.unit (mkSBVTuple2 (- 3) "enough"))))) (seq.unit (mkSBVTuple2 (- 4) (as seq.empty (Seq (SBVTuple2 Int String))))) (seq.unit (mkSBVTuple2 (- 5) (as seq.empty (Seq (SBVTuple2 Int String))))))) +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s4 () Int 2) +[GOOD] (define-fun s6 () Int 1) +[GOOD] (define-fun s14 () Int 4) +[GOOD] (define-fun s17 () Int 5) +[GOOD] (define-fun s11 () String "foo") +[GOOD] (define-fun s23 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.++ (seq.unit (mkSBVTuple2 2 (as seq.empty (Seq (SBVTuple2 Int String))))) (seq.unit (mkSBVTuple2 1 (seq.++ (seq.unit (mkSBVTuple2 3 "foo")) (seq.unit (mkSBVTuple2 0 "bar")) (seq.unit (mkSBVTuple2 (- 1) "baz")) (seq.unit (mkSBVTuple2 (- 2) "quux")) (seq.unit (mkSBVTuple2 (- 3) "enough"))))) (seq.unit (mkSBVTuple2 (- 4) (as seq.empty (Seq (SBVTuple2 Int String))))) (seq.unit (mkSBVTuple2 (- 5) (as seq.empty (Seq (SBVTuple2 Int String))))))) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String))))) ; tracks user variable "lst" -[GOOD] (declare-fun s1 () (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) ; tracks user variable "__internal_sbv_s1" -[GOOD] (declare-fun s13 () (SBVTuple2 Int String)) ; tracks user variable "__internal_sbv_s13" -[GOOD] (declare-fun s15 () (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) ; tracks user variable "__internal_sbv_s15" -[GOOD] (declare-fun s32 () (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) ; tracks user variable "__internal_sbv_s32" -[GOOD] (declare-fun s40 () (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) ; tracks user variable "__internal_sbv_s40" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- -[GOOD] (define-fun s2 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.unit s1)) -[GOOD] (define-fun s5 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.extract s0 s3 s4)) -[GOOD] (define-fun s6 () Bool (= s2 s5)) -[GOOD] (define-fun s7 () Int (seq.len s0)) -[GOOD] (define-fun s8 () Bool (<= s7 s3)) -[GOOD] (define-fun s9 () Bool (or s6 s8)) -[GOOD] (define-fun s10 () Int (proj_1_SBVTuple2 s1)) +[GOOD] (define-fun s2 () (SBVTuple2 Int (Seq (SBVTuple2 Int String))) (seq.nth s0 s1)) +[GOOD] (define-fun s3 () Int (proj_1_SBVTuple2 s2)) +[GOOD] (define-fun s5 () Bool (= s3 s4)) +[GOOD] (define-fun s7 () (SBVTuple2 Int (Seq (SBVTuple2 Int String))) (seq.nth s0 s6)) +[GOOD] (define-fun s8 () (Seq (SBVTuple2 Int String)) (proj_2_SBVTuple2 s7)) +[GOOD] (define-fun s9 () (SBVTuple2 Int String) (seq.nth s8 s1)) +[GOOD] (define-fun s10 () String (proj_2_SBVTuple2 s9)) [GOOD] (define-fun s12 () Bool (= s10 s11)) -[GOOD] (define-fun s14 () (Seq (SBVTuple2 Int String)) (seq.unit s13)) -[GOOD] (define-fun s16 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.unit s15)) -[GOOD] (define-fun s17 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.extract s0 s4 s4)) +[GOOD] (define-fun s13 () Int (seq.len s0)) +[GOOD] (define-fun s15 () Bool (= s13 s14)) +[GOOD] (define-fun s16 () Int (seq.len s8)) [GOOD] (define-fun s18 () Bool (= s16 s17)) -[GOOD] (define-fun s19 () Bool (<= s7 s4)) -[GOOD] (define-fun s20 () Bool (or s18 s19)) -[GOOD] (define-fun s21 () (Seq (SBVTuple2 Int String)) (proj_2_SBVTuple2 s15)) -[GOOD] (define-fun s22 () (Seq (SBVTuple2 Int String)) (seq.extract s21 s3 s4)) -[GOOD] (define-fun s23 () Bool (= s14 s22)) -[GOOD] (define-fun s24 () Int (seq.len s21)) -[GOOD] (define-fun s25 () Bool (<= s24 s3)) -[GOOD] (define-fun s26 () Bool (or s23 s25)) -[GOOD] (define-fun s27 () String (proj_2_SBVTuple2 s13)) -[GOOD] (define-fun s29 () Bool (= s27 s28)) -[GOOD] (define-fun s31 () Bool (= s7 s30)) -[GOOD] (define-fun s33 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.unit s32)) -[GOOD] (define-fun s34 () Bool (= s17 s33)) -[GOOD] (define-fun s35 () Bool (or s19 s34)) -[GOOD] (define-fun s36 () (Seq (SBVTuple2 Int String)) (proj_2_SBVTuple2 s32)) -[GOOD] (define-fun s37 () Int (seq.len s36)) -[GOOD] (define-fun s39 () Bool (= s37 s38)) -[GOOD] (define-fun s41 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.unit s40)) -[GOOD] (define-fun s42 () (Seq (SBVTuple2 Int (Seq (SBVTuple2 Int String)))) (seq.extract s0 s11 s4)) -[GOOD] (define-fun s43 () Bool (= s41 s42)) -[GOOD] (define-fun s44 () Bool (<= s7 s11)) -[GOOD] (define-fun s45 () Bool (or s43 s44)) -[GOOD] (define-fun s46 () (Seq (SBVTuple2 Int String)) (proj_2_SBVTuple2 s40)) -[GOOD] (define-fun s47 () Int (seq.len s46)) -[GOOD] (define-fun s48 () Bool (= s3 s47)) -[GOOD] (define-fun s50 () Bool (= s0 s49)) -[GOOD] (assert s9) +[GOOD] (define-fun s19 () (SBVTuple2 Int (Seq (SBVTuple2 Int String))) (seq.nth s0 s4)) +[GOOD] (define-fun s20 () (Seq (SBVTuple2 Int String)) (proj_2_SBVTuple2 s19)) +[GOOD] (define-fun s21 () Int (seq.len s20)) +[GOOD] (define-fun s22 () Bool (= s1 s21)) +[GOOD] (define-fun s24 () Bool (= s0 s23)) +[GOOD] (assert s5) [GOOD] (assert s12) -[GOOD] (assert s20) -[GOOD] (assert s26) -[GOOD] (assert s29) -[GOOD] (assert s31) -[GOOD] (assert s35) -[GOOD] (assert s39) -[GOOD] (assert s45) -[GOOD] (assert s48) -[GOOD] (assert s50) +[GOOD] (assert s15) +[GOOD] (assert s18) +[GOOD] (assert s22) +[GOOD] (assert s24) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) diff --git a/SBVTestSuite/GoldFiles/tuple_nested.gold b/SBVTestSuite/GoldFiles/tuple_nested.gold --- a/SBVTestSuite/GoldFiles/tuple_nested.gold +++ b/SBVTestSuite/GoldFiles/tuple_nested.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) diff --git a/SBVTestSuite/GoldFiles/tuple_swap.gold b/SBVTestSuite/GoldFiles/tuple_swap.gold --- a/SBVTestSuite/GoldFiles/tuple_swap.gold +++ b/SBVTestSuite/GoldFiles/tuple_swap.gold @@ -36,11 +36,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple3 1 2 0))) +[RECV] ((s0 (mkSBVTuple3 0 7719 1))) [SEND] (get-value (s1)) -[RECV] ((s1 (mkSBVTuple3 2 1 3))) +[RECV] ((s1 (mkSBVTuple3 7719 0 2))) *** Solver : Z3 *** Exit code: ExitSuccess - FINAL: ((1,2,0),(2,1,3)) + FINAL: ((0,7719,1),(7719,0,2)) DONE! diff --git a/SBVTestSuite/GoldFiles/tuple_twoTwo.gold b/SBVTestSuite/GoldFiles/tuple_twoTwo.gold --- a/SBVTestSuite/GoldFiles/tuple_twoTwo.gold +++ b/SBVTestSuite/GoldFiles/tuple_twoTwo.gold @@ -7,7 +7,7 @@ [GOOD] (set-option :produce-models true) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) -[GOOD] (set-logic ALL) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 8.2 +Version: 8.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 @@ -63,7 +63,7 @@ TypeSynonymInstances UndecidableInstances ViewPatterns - Build-Depends : base >= 4.9 && < 5 + Build-Depends : base >= 4.11 && < 5 , crackNum >= 2.3 , ghc, QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time @@ -224,7 +224,7 @@ TemplateHaskell TupleSections TypeApplications - Build-depends : base >= 4.9, filepath, syb, crackNum >= 2.3 + Build-depends : base >= 4.11, filepath, syb, crackNum >= 2.3 , sbv, directory, random, mtl, containers , template-haskell, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, QuickCheck Hs-Source-Dirs : SBVTestSuite