sbv-8.1: SBVTestSuite/GoldFiles/freshVars.gold
** 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 :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 0)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] (assert s2)
[GOOD] (declare-fun s3 () Bool)
[GOOD] (declare-fun s4 () (_ BitVec 8))
[GOOD] (declare-fun s5 () (_ BitVec 16))
[GOOD] (declare-fun s6 () (_ BitVec 32))
[GOOD] (declare-fun s7 () (_ BitVec 64))
[GOOD] (declare-fun s8 () (_ BitVec 8))
[GOOD] (declare-fun s9 () (_ BitVec 16))
[GOOD] (declare-fun s10 () (_ BitVec 32))
[GOOD] (declare-fun s11 () (_ BitVec 64))
[GOOD] (declare-fun s12 () (_ FloatingPoint 8 24))
[GOOD] (declare-fun s13 () (_ FloatingPoint 11 53))
[GOOD] (declare-fun s14 () Real)
[GOOD] (declare-fun s15 () Int)
[GOOD] (declare-datatypes ((BinOp 0)) (((Plus) (Minus) (Times))))
[GOOD] (define-fun BinOp_constrIndex ((x BinOp)) Int
(ite (= x Plus) 0 (ite (= x Minus) 1 2))
)
[GOOD] (declare-fun s16 () BinOp)
[GOOD] (assert s3)
[GOOD] (define-fun s17 () (_ BitVec 8) #x01)
[GOOD] (define-fun s18 () Bool (= s4 s17))
[GOOD] (assert s18)
[GOOD] (define-fun s19 () (_ BitVec 16) #x0002)
[GOOD] (define-fun s20 () Bool (= s5 s19))
[GOOD] (assert s20)
[GOOD] (define-fun s21 () (_ BitVec 32) #x00000003)
[GOOD] (define-fun s22 () Bool (= s6 s21))
[GOOD] (assert s22)
[GOOD] (define-fun s23 () (_ BitVec 64) #x0000000000000004)
[GOOD] (define-fun s24 () Bool (= s7 s23))
[GOOD] (assert s24)
[GOOD] (define-fun s25 () (_ BitVec 8) #x05)
[GOOD] (define-fun s26 () Bool (= s8 s25))
[GOOD] (assert s26)
[GOOD] (define-fun s27 () (_ BitVec 16) #x0006)
[GOOD] (define-fun s28 () Bool (= s9 s27))
[GOOD] (assert s28)
[GOOD] (define-fun s29 () (_ BitVec 32) #x00000007)
[GOOD] (define-fun s30 () Bool (= s10 s29))
[GOOD] (assert s30)
[GOOD] (define-fun s31 () (_ BitVec 64) #x0000000000000008)
[GOOD] (define-fun s32 () Bool (= s11 s31))
[GOOD] (assert s32)
[GOOD] (define-fun s33 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))
[GOOD] (define-fun s34 () Bool (fp.eq s12 s33))
[GOOD] (assert s34)
[GOOD] (define-fun s35 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) roundNearestTiesToEven (/ 10.0 1.0)))
[GOOD] (define-fun s36 () Bool (fp.eq s13 s35))
[GOOD] (assert s36)
[GOOD] (define-fun s37 () Real (/ 11.0 1.0))
[GOOD] (define-fun s38 () Bool (= s14 s37))
[GOOD] (assert s38)
[GOOD] (define-fun s39 () Int 12)
[GOOD] (define-fun s40 () Bool (= s15 s39))
[GOOD] (assert s40)
[GOOD] (define-fun s41 () BinOp Plus)
[GOOD] (define-fun s42 () Bool (= s16 s41))
[GOOD] (assert s42)
[GOOD] (declare-fun array_0 () (Array Int Int))
[GOOD] (declare-fun s43 () Int)
[GOOD] (declare-fun s44 () Bool)
[GOOD] (define-fun s46 () Int 2)
[GOOD] (define-fun s45 () Int (select array_0 s43))
[GOOD] (define-fun s47 () Bool (= s45 s46))
[GOOD] (assert s47)
[GOOD] (define-fun s49 () (_ BitVec 8) #x61)
[GOOD] (declare-fun vFArray_uninitializedRead (Bool) (_ BitVec 8))
[GOOD] (define-fun s48 () (_ BitVec 8) (vFArray_uninitializedRead s44))
[GOOD] (define-fun s50 () Bool (= s48 s49))
[GOOD] (assert s50)
[GOOD] (define-fun s51 () Int 42)
[GOOD] (define-fun array_1 () (Array Int Int) ((as const (Array Int Int)) 42))
[GOOD] (declare-fun s52 () Int)
[GOOD] (declare-fun s53 () (_ BitVec 8))
[GOOD] (define-fun s54 () Int 96)
[GOOD] (define-fun s55 () Int (select array_1 s54))
[GOOD] (define-fun s56 () Bool (= s52 s55))
[GOOD] (assert s56)
[GOOD] (define-fun s57 () (_ BitVec 8) #x58)
[GOOD] (define-fun s58 () Bool (= s53 s57))
[GOOD] (assert s58)
[GOOD] (define-fun s59 () Int 1)
[GOOD] (define-fun s60 () Bool (= s43 s59))
[GOOD] (assert s60)
[GOOD] (define-fun s61 () Bool (not s44))
[GOOD] (assert s61)
[GOOD] (declare-fun s62 () String)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (declare-fun s63 () (Seq Int))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (declare-fun s64 () (Seq (Seq Int)))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (declare-fun s65 () (Seq (_ BitVec 8)))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (declare-fun s66 () (Seq (Seq (_ BitVec 16))))
[GOOD] (define-fun s67 () String "hello")
[GOOD] (define-fun s68 () Bool (= s62 s67))
[GOOD] (assert s68)
[GOOD] (define-fun s69 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))
[GOOD] (define-fun s70 () Bool (= s63 s69))
[GOOD] (assert s70)
[GOOD] (define-fun s71 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))))
[GOOD] (define-fun s72 () Bool (= s64 s71))
[GOOD] (assert s72)
[GOOD] (define-fun s73 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02)))
[GOOD] (define-fun s74 () Bool (= s65 s73))
[GOOD] (assert s74)
[GOOD] (define-fun s75 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006)))))
[GOOD] (define-fun s76 () Bool (= s66 s75))
[GOOD] (assert s76)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 0))
[SEND] (get-value (s3))
[RECV] ((s3 true))
[SEND] (get-value (s4))
[RECV] ((s4 #x01))
[SEND] (get-value (s5))
[RECV] ((s5 #x0002))
[SEND] (get-value (s6))
[RECV] ((s6 #x00000003))
[SEND] (get-value (s7))
[RECV] ((s7 #x0000000000000004))
[SEND] (get-value (s8))
[RECV] ((s8 #x05))
[SEND] (get-value (s9))
[RECV] ((s9 #x0006))
[SEND] (get-value (s10))
[RECV] ((s10 #x00000007))
[SEND] (get-value (s11))
[RECV] ((s11 #x0000000000000008))
[SEND] (get-value (s12))
[RECV] ((s12 (fp #b0 #x82 #b00100000000000000000000)))
[SEND] (get-value (s13))
[RECV] ((s13 (fp #b0 #b10000000010 #x4000000000000)))
[SEND] (get-value (s14))
[RECV] ((s14 11.0))
[SEND] (get-value (s15))
[RECV] ((s15 12))
[SEND] (get-value (s16))
[RECV] ((s16 Plus))
[SEND] (get-value (s43))
[RECV] ((s43 1))
[SEND] (get-value (s44))
[RECV] ((s44 false))
[SEND] (get-value (s52))
[RECV] ((s52 42))
[SEND] (get-value (s53))
[RECV] ((s53 #x58))
[SEND] (get-value (s62))
[RECV] ((s62 "hello"))
[SEND] (get-value (s63))
[RECV] ((s63 (seq.++ (seq.unit 1) (seq.++ (seq.unit 2) (seq.++ (seq.unit 3) (seq.unit 4))))))
[SEND] (get-value (s64))
[RECV] ((s64 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.++ (seq.unit 2) (seq.unit 3))))
(seq.unit (seq.++ (seq.unit 4)
(seq.++ (seq.unit 5)
(seq.++ (seq.unit 6) (seq.unit 7))))))))
[SEND] (get-value (s65))
[RECV] ((s65 "\x01\x02"))
[SEND] (get-value (s66))
[RECV] ((s66 (seq.++ (seq.unit (seq.++ (seq.unit #x0001)
(seq.++ (seq.unit #x0002) (seq.unit #x0003))))
(seq.++ (seq.unit (as seq.empty (Seq (_ BitVec 16))))
(seq.unit (seq.++ (seq.unit #x0004)
(seq.++ (seq.unit #x0005) (seq.unit #x0006))))))))
*** Solver : Z3
*** Exit code: ExitSuccess
FINAL:Satisfiable. Model:
a = 0 :: Integer
vBool = True :: Bool
vWord8 = 1 :: Word8
s5 = 2 :: Word16
s6 = 3 :: Word32
vWord64 = 4 :: Word64
vInt8 = 5 :: Int8
s9 = 6 :: Int16
s10 = 7 :: Int32
vInt64 = 8 :: Int64
vFloat = 9.0 :: Float
s13 = 10.0 :: Double
s14 = 11.0 :: Real
vInteger = 12 :: Integer
vBinOp = Plus :: BinOp
i1 = 1 :: Integer
i2 = False :: Bool
mustBe42 = 42 :: Integer
mustBeX = 'X' :: Char
vString = "hello" :: String
vList1 = [1,2,3,4] :: [Integer]
vList2 = [[1,2,3],[4,5,6,7]] :: [[Integer]]
vList3 = [1,2] :: [Word8]
vList4 = [[1,2,3],[],[4,5,6]] :: [[Word16]]
DONE!