sbv-14.1: SBVTestSuite/GoldFiles/query_uisatex1.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 :produce-models true)
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Int 2)
[GOOD] (define-fun s3 () Int 12)
[GOOD] (define-fun s5 () Int 3)
[GOOD] (define-fun s7 () Int 75)
[GOOD] (define-fun s9 () Int (- 3))
[GOOD] (define-fun s11 () Int 9)
[GOOD] (define-fun s14 () Int 1)
[GOOD] (define-fun s21 () Int 5)
[GOOD] (define-fun s23 () Int 7)
[GOOD] (define-fun s25 () Int 6)
[GOOD] (define-fun s29 () (_ FloatingPoint 8 24) (fp #b0 #b10000010 #b00010011001100110011010))
[GOOD] (define-fun s32 () (_ FloatingPoint 8 24) (fp #b0 #b10000010 #b00110011001100110011010))
[GOOD] (define-fun s33 () Int 121)
[GOOD] (define-fun s38 () Int 8)
[GOOD] (define-fun s40 () (_ FloatingPoint 8 24) (_ +oo 8 24))
[GOOD] (define-fun s42 () String (_ char #x63))
[GOOD] (define-fun s43 () String "hey")
[GOOD] (define-fun s45 () (_ FloatingPoint 8 24) (fp #b0 #b10000101 #b00111000000000000000000))
[GOOD] (define-fun s47 () String "tey")
[GOOD] (define-fun s49 () (_ FloatingPoint 8 24) (fp #b0 #b10000101 #b01110000000000000000000))
[GOOD] (define-fun s51 () String (_ char #x72))
[GOOD] (define-fun s52 () String "foo")
[GOOD] (define-fun s54 () (_ FloatingPoint 8 24) (fp #b0 #b10000000 #b11000000000000000000000))
[GOOD] (define-fun s56 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
[GOOD] (define-fun s57 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit (fp #b0 #b10000010 #b00000110011001100110011)) (seq.unit (fp #b0 #b10000000 #b10000000000000000000000))))
[GOOD] (define-fun s60 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5)))
[GOOD] (define-fun s61 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit (fp #b0 #b10000010 #b00000110011001100110011)) (seq.unit (fp #b0 #b10000010 #b00100000000000000000000))))
[GOOD] (define-fun s63 () Int 21)
[GOOD] (define-fun s65 () (Seq Int) (seq.unit 5))
[GOOD] (define-fun s66 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit (fp #b0 #b10000010 #b00000110011001100110011)) (seq.unit (_ +zero 8 24))))
[GOOD] (define-fun s68 () Int 210)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Int)
[GOOD] (declare-fun s17 () Bool) ; tracks user variable "__internal_sbv_s17"
[GOOD] (declare-fun s18 () Int) ; tracks user variable "__internal_sbv_s18"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] (declare-fun q1 (Int) Int)
[GOOD] (declare-fun q2 (Bool Int) Int)
[GOOD] (declare-fun q3 ((_ FloatingPoint 8 24) Bool Int) (_ FloatingPoint 8 24))
[GOOD] (declare-fun q4 (String String) (_ FloatingPoint 8 24))
[GOOD] (declare-fun q5 ((Seq Int) (Seq (_ FloatingPoint 8 24))) Int)
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Int (q1 s1))
[GOOD] (define-fun s4 () Bool (= s2 s3))
[GOOD] (define-fun s6 () Int (q1 s5))
[GOOD] (define-fun s8 () Bool (= s6 s7))
[GOOD] (define-fun s10 () Int (q1 s9))
[GOOD] (define-fun s12 () Bool (= s10 s11))
[GOOD] (define-fun s13 () Int (q1 s0))
[GOOD] (define-fun s15 () Int (+ s0 s14))
[GOOD] (define-fun s16 () Bool (= s13 s15))
[GOOD] (define-fun s19 () Int (q2 s17 s18))
[GOOD] (define-fun s20 () Int (q2 true s5))
[GOOD] (define-fun s22 () Bool (= s20 s21))
[GOOD] (define-fun s24 () Int (q2 false s23))
[GOOD] (define-fun s26 () Bool (= s24 s25))
[GOOD] (define-fun s27 () Int (q2 false s3))
[GOOD] (define-fun s28 () Bool (= s5 s27))
[GOOD] (define-fun s30 () (_ FloatingPoint 8 24) (q3 s29 true s3))
[GOOD] (define-fun s31 () Bool (fp.eq s29 s30))
[GOOD] (define-fun s34 () (_ FloatingPoint 8 24) (q3 s32 true s33))
[GOOD] (define-fun s35 () Bool (fp.isZero s34))
[GOOD] (define-fun s36 () Bool (fp.isNegative s34))
[GOOD] (define-fun s37 () Bool (and s35 s36))
[GOOD] (define-fun s39 () (_ FloatingPoint 8 24) (q3 s32 false s38))
[GOOD] (define-fun s41 () Bool (fp.eq s39 s40))
[GOOD] (define-fun s44 () (_ FloatingPoint 8 24) (q4 s42 s43))
[GOOD] (define-fun s46 () Bool (fp.eq s44 s45))
[GOOD] (define-fun s48 () (_ FloatingPoint 8 24) (q4 s42 s47))
[GOOD] (define-fun s50 () Bool (fp.eq s48 s49))
[GOOD] (define-fun s53 () (_ FloatingPoint 8 24) (q4 s51 s52))
[GOOD] (define-fun s55 () Bool (fp.eq s53 s54))
[GOOD] (define-fun s58 () Int (q5 s56 s57))
[GOOD] (define-fun s59 () Bool (= s23 s58))
[GOOD] (define-fun s62 () Int (q5 s60 s61))
[GOOD] (define-fun s64 () Bool (= s62 s63))
[GOOD] (define-fun s67 () Int (q5 s65 s66))
[GOOD] (define-fun s69 () Bool (= s67 s68))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s4)
[GOOD] (assert s8)
[GOOD] (assert s12)
[GOOD] (assert s16)
[GOOD] (assert s22)
[GOOD] (assert s26)
[GOOD] (assert s28)
[GOOD] (assert s31)
[GOOD] (assert s37)
[GOOD] (assert s41)
[GOOD] (assert s46)
[GOOD] (assert s50)
[GOOD] (assert s55)
[GOOD] (assert s59)
[GOOD] (assert s64)
[GOOD] (assert s69)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 0))
[SEND] (get-value (s17))
[RECV] ((s17 false))
[SEND] (get-value (s18))
[RECV] ((s18 0))
[GOOD] (set-option :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def true )
[SEND] (get-value (q1))
[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) 0 1)))
[SEND] (get-value (q2))
[RECV] ((q2 (store (store ((as const (Array Bool Int Int)) 5) false 7 6) false 12 3)))
[SEND] (get-value (q3))
[RECV] ((q3 (store (store ((as const
(Array (_ FloatingPoint 8 24)
Bool
Int
(_ FloatingPoint 8 24)))
(fp #b0 #x82 #b00010011001100110011010))
(fp #b0 #x82 #b00110011001100110011010)
true
121
(_ -zero 8 24))
(fp #b0 #x82 #b00110011001100110011010)
false
8
(_ +oo 8 24))))
[SEND] (get-value (q4))
[RECV] ((q4 (store (store ((as const (Array String String (_ FloatingPoint 8 24)))
(fp #b0 #x85 #b00111000000000000000000))
"c"
"tey"
(fp #b0 #x85 #b01110000000000000000000))
"r"
"foo"
(fp #b0 #x80 #b11000000000000000000000))))
[SEND] (get-value (q5))
[RECV] ((q5 (store (store ((as const (Array (Seq Int) (Seq (_ FloatingPoint 8 24)) Int)) 7)
(seq.++ (seq.unit 9) (seq.unit 5))
(seq.++ (seq.unit (fp #b0 #x82 #b00000110011001100110011))
(seq.unit (fp #b0 #x82 #b00100000000000000000000)))
21)
(seq.unit 5)
(seq.++ (seq.unit (fp #b0 #x82 #b00000110011001100110011))
(seq.unit (_ +zero 8 24)))
210)))
*** Solver : Z3
*** Exit code: ExitSuccess
FINAL:
Satisfiable. Model:
s0 = 0 :: Integer
q1 :: Integer -> Integer
q1 0 = 1
q1 (-3) = 9
q1 3 = 75
q1 _ = 12
q2 :: Bool -> Integer -> Integer
q2 False 12 = 3
q2 False 7 = 6
q2 _ _ = 5
q3 :: Float -> Bool -> Integer -> Float
q3 9.6 False 8 = Infinity
q3 9.6 True 121 = -0.0
q3 _ _ _ = 8.6
q4 :: Char -> String -> Float
q4 'r' "foo" = 3.5
q4 'c' "tey" = 92.0
q4 _ _ = 78.0
q5 :: [Integer] -> [Float] -> Integer
q5 [5] [8.2,0.0] = 210
q5 [9,5] [8.2,9.0] = 21
q5 _ _ = 7
DONE!