sbv-14.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] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 0)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[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] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] ; User defined ADT: BinOp
[GOOD] (declare-datatype BinOp (
(Plus)
(Minus)
(Times)
))
[GOOD] (declare-fun s16 () BinOp)
[GOOD] (declare-fun s17 () (_ FloatingPoint 15 113))
[GOOD] (declare-fun s18 () (_ FloatingPoint 15 113))
[GOOD] (assert s3)
[GOOD] (define-fun s19 () (_ BitVec 8) #x01)
[GOOD] (define-fun s20 () Bool (= s4 s19))
[GOOD] (assert s20)
[GOOD] (define-fun s21 () (_ BitVec 16) #x0002)
[GOOD] (define-fun s22 () Bool (= s5 s21))
[GOOD] (assert s22)
[GOOD] (define-fun s23 () (_ BitVec 32) #x00000003)
[GOOD] (define-fun s24 () Bool (= s6 s23))
[GOOD] (assert s24)
[GOOD] (define-fun s25 () (_ BitVec 64) #x0000000000000004)
[GOOD] (define-fun s26 () Bool (= s7 s25))
[GOOD] (assert s26)
[GOOD] (define-fun s27 () (_ BitVec 8) #x05)
[GOOD] (define-fun s28 () Bool (= s8 s27))
[GOOD] (assert s28)
[GOOD] (define-fun s29 () (_ BitVec 16) #x0006)
[GOOD] (define-fun s30 () Bool (= s9 s29))
[GOOD] (assert s30)
[GOOD] (define-fun s31 () (_ BitVec 32) #x00000007)
[GOOD] (define-fun s32 () Bool (= s10 s31))
[GOOD] (assert s32)
[GOOD] (define-fun s33 () (_ BitVec 64) #x0000000000000008)
[GOOD] (define-fun s34 () Bool (= s11 s33))
[GOOD] (assert s34)
[GOOD] (define-fun s35 () (_ FloatingPoint 8 24) (fp #b0 #b10000010 #b00100000000000000000000))
[GOOD] (define-fun s36 () Bool (fp.eq s12 s35))
[GOOD] (assert s36)
[GOOD] (define-fun s37 () (_ FloatingPoint 11 53) (fp #b0 #b10000000010 #b0100000000000000000000000000000000000000000000000000))
[GOOD] (define-fun s38 () Bool (fp.eq s13 s37))
[GOOD] (assert s38)
[GOOD] (define-fun s39 () Real (/ 11.0 1.0))
[GOOD] (define-fun s40 () Bool (= s14 s39))
[GOOD] (assert s40)
[GOOD] (define-fun s41 () Int 12)
[GOOD] (define-fun s42 () Bool (= s15 s41))
[GOOD] (assert s42)
[GOOD] (define-fun s43 () BinOp (as Plus BinOp))
[GOOD] (define-fun s44 () Bool (= s16 s43))
[GOOD] (assert s44)
[GOOD] (define-fun s45 () Bool (fp.eq s17 s18))
[GOOD] (assert s45)
[GOOD] (define-fun s46 () Bool (= s17 s18))
[GOOD] (define-fun s47 () Bool (not s46))
[GOOD] (assert s47)
[GOOD] (define-fun s48 () Bool (fp.isPositive s17))
[GOOD] (assert s48)
[GOOD] (declare-fun s49 () (Array Int Int))
[GOOD] (declare-fun s50 () Int)
[GOOD] (declare-fun s51 () Bool)
[GOOD] (define-fun s53 () Int 2)
[GOOD] (define-fun s52 () Int (select s49 s50))
[GOOD] (define-fun s54 () Bool (= s52 s53))
[GOOD] (assert s54)
[GOOD] (declare-fun s55 () Int)
[GOOD] (define-fun s56 () Int 42)
[GOOD] (define-fun s57 () Bool (= s55 s56))
[GOOD] (assert s57)
[GOOD] (define-fun s58 () Int 1)
[GOOD] (define-fun s59 () Bool (= s50 s58))
[GOOD] (assert s59)
[GOOD] (define-fun s60 () Bool (not s51))
[GOOD] (assert s60)
[GOOD] (declare-fun s61 () String)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (declare-fun s62 () (Seq Int))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (declare-fun s63 () (Seq (Seq Int)))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (declare-fun s64 () (Seq (_ BitVec 8)))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (declare-fun s65 () (Seq (Seq (_ BitVec 16))))
[GOOD] (define-fun s66 () String "hello")
[GOOD] (define-fun s67 () Bool (= s61 s66))
[GOOD] (assert s67)
[GOOD] (define-fun s68 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))
[GOOD] (define-fun s69 () Bool (= s62 s68))
[GOOD] (assert s69)
[GOOD] (define-fun s70 () (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 s71 () Bool (= s63 s70))
[GOOD] (assert s71)
[GOOD] (define-fun s72 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02)))
[GOOD] (define-fun s73 () Bool (= s64 s72))
[GOOD] (assert s73)
[GOOD] (define-fun s74 () (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 s75 () Bool (= s65 s74))
[GOOD] (assert s75)
[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)))
[GOOD] (set-option :pp.decimal false)
[SEND] (get-value (s14))
[RECV] ((s14 11.0))
[GOOD] (set-option :pp.decimal true)
[GOOD] (set-option :pp.decimal_precision 16)
[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 (s49))
[RECV] ((s49 ((as const (Array Int Int)) 2)))
[SEND] (get-value (s50))
[RECV] ((s50 1))
[SEND] (get-value (s51))
[RECV] ((s51 false))
[SEND] (get-value (s55))
[RECV] ((s55 42))
[SEND] (get-value (s61))
[RECV] ((s61 "hello"))
[SEND] (get-value (s62))
[RECV] ((s62 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))))
[SEND] (get-value (s63))
[RECV] ((s63 (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))))))
[SEND] (get-value (s64))
[RECV] ((s64 (seq.++ (seq.unit #x01) (seq.unit #x02))))
[SEND] (get-value (s65))
[RECV] ((s65 (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))))))
[SEND] (get-value (s17))
[RECV] ((s17 (_ +zero 15 113)))
[SEND] (get-value (s18))
[RECV] ((s18 (_ -zero 15 113)))
*** 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
vSArray = ([], 2) :: Array Integer Integer
i1 = 1 :: Integer
i2 = False :: Bool
mustBe42 = 42 :: Integer
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]]
vQuad = 0.0 :: FloatingPoint 15 113
wQuad = -0.0 :: FloatingPoint 15 113
DONE!