packages feed

sbv 8.2 → 8.3

raw patch · 77 files changed

+1081/−1742 lines, 77 files

Files

CHANGES.md view
@@ -1,7 +1,22 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* 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
Data/SBV/Client.hs view
@@ -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
Data/SBV/Control/Utils.hs view
@@ -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
Data/SBV/Core/Symbolic.hs view
@@ -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 {
Data/SBV/List.hs view
@@ -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 <http://github.com/Z3Prover/z3/issues/1302>-        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
Data/SBV/Provers/CVC4.hs view
@@ -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
Data/SBV/SMT/SMTLib2.hs view
@@ -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) ++ ")"
Data/SBV/Set.hs view
@@ -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.
Data/SBV/String.hs view
@@ -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 <http://github.com/Z3Prover/z3/issues/1302>-        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 <http://cvc4.cs.stanford.edu/wiki/Strings> 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
SBVTestSuite/GoldFiles/foldlABC1.gold view
@@ -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
SBVTestSuite/GoldFiles/foldlABC2.gold view
@@ -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
SBVTestSuite/GoldFiles/foldlABC3.gold view
@@ -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
SBVTestSuite/GoldFiles/foldrAB1.gold view
@@ -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
SBVTestSuite/GoldFiles/foldrAB2.gold view
@@ -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
SBVTestSuite/GoldFiles/foldrAB3.gold view
@@ -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
− SBVTestSuite/GoldFiles/listSum.gold 
@@ -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
− SBVTestSuite/GoldFiles/makePair.gold 
@@ -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
SBVTestSuite/GoldFiles/mapNoFailure.gold view
@@ -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
SBVTestSuite/GoldFiles/mapWithFailure.gold view
@@ -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
SBVTestSuite/GoldFiles/maxlWithFailure.gold view
@@ -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
SBVTestSuite/GoldFiles/maxrWithFailure.gold view
@@ -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
SBVTestSuite/GoldFiles/query1.gold view
@@ -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)
SBVTestSuite/GoldFiles/query_ListOfMaybe.gold view
@@ -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))
SBVTestSuite/GoldFiles/query_ListOfSum.gold view
@@ -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))
SBVTestSuite/GoldFiles/query_Lists1.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/query_Strings1.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/query_sumMergeEither1.gold view
@@ -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)
SBVTestSuite/GoldFiles/query_sumMergeEither2.gold view
@@ -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)
SBVTestSuite/GoldFiles/query_sumMergeMaybe1.gold view
@@ -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)
SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold view
@@ -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)
SBVTestSuite/GoldFiles/query_uisatex1.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/query_uisatex2.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/reverse.gold view
@@ -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
SBVTestSuite/GoldFiles/reverseAlt10.gold view
@@ -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
SBVTestSuite/GoldFiles/seqExamples2.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/seqExamples3.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/seqExamples4.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/seqExamples5.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/seqExamples6.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/seqExamples7.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/seqExamples8.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/set_compl1.gold view
@@ -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
SBVTestSuite/GoldFiles/set_delete1.gold view
@@ -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)
SBVTestSuite/GoldFiles/set_diff1.gold view
@@ -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
SBVTestSuite/GoldFiles/set_disj1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_empty1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_full1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_insert1.gold view
@@ -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)
SBVTestSuite/GoldFiles/set_intersect1.gold view
@@ -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
SBVTestSuite/GoldFiles/set_member1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_notMember1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_psubset1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_subset1.gold view
@@ -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))
SBVTestSuite/GoldFiles/set_union1.gold view
@@ -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
SBVTestSuite/GoldFiles/sort.gold view
@@ -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
SBVTestSuite/GoldFiles/strExamples10.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples11.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples12.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples13.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples2.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples3.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples4.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples5.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples6.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples7.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples8.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/strExamples9.gold view
@@ -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 ---
SBVTestSuite/GoldFiles/sumMergeEither1.gold view
@@ -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
SBVTestSuite/GoldFiles/sumMergeEither2.gold view
@@ -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
SBVTestSuite/GoldFiles/sumMergeMaybe1.gold view
@@ -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
SBVTestSuite/GoldFiles/sumMergeMaybe2.gold view
@@ -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
SBVTestSuite/GoldFiles/tuple_enum.gold view
@@ -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
SBVTestSuite/GoldFiles/tuple_list.gold view
@@ -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))
SBVTestSuite/GoldFiles/tuple_nested.gold view
@@ -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)
SBVTestSuite/GoldFiles/tuple_swap.gold view
@@ -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!
SBVTestSuite/GoldFiles/tuple_twoTwo.gold view
@@ -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)
sbv.cabal view
@@ -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