sbv-8.2: SBVTestSuite/GoldFiles/query_uisatex2.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-logic ALL)
[GOOD] ; --- uninterpreted sorts ---
[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 s17 () Int 0)
[GOOD] (define-fun s20 () Int 5)
[GOOD] (define-fun s22 () Int 7)
[GOOD] (define-fun s24 () Int 6)
[GOOD] (define-fun s32 () Int 121)
[GOOD] (define-fun s37 () Int 8)
[GOOD] (define-fun s62 () Int 21)
[GOOD] (define-fun s67 () Int 210)
[GOOD] (define-fun s28 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0)))
[GOOD] (define-fun s31 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0)))
[GOOD] (define-fun s39 () (_ FloatingPoint 8 24) (_ +oo 8 24))
[GOOD] (define-fun s44 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0)))
[GOOD] (define-fun s48 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))
[GOOD] (define-fun s53 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0)))
[GOOD] (define-fun s41 () (_ BitVec 8) #x63)
[GOOD] (define-fun s50 () (_ BitVec 8) #x72)
[GOOD] (define-fun s42 () String "hey")
[GOOD] (define-fun s46 () String "tey")
[GOOD] (define-fun s51 () String "foo")
[GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
[GOOD] (define-fun s59 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5)))
[GOOD] (define-fun s64 () (Seq Int) (seq.unit 5))
[GOOD] (define-fun s56 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0)))))
[GOOD] (define-fun s60 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))))
[GOOD] (define-fun s65 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24))))
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int)
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[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 ((_ BitVec 8) String) (_ FloatingPoint 8 24))
[GOOD] (declare-fun q5 ((Seq Int) (Seq (_ FloatingPoint 8 24))) Int)
[GOOD] (declare-fun q6 (Int) Bool)
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[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 s18 () Int (q2 false s17))
[GOOD] (define-fun s19 () Int (q2 true s5))
[GOOD] (define-fun s21 () Bool (= s19 s20))
[GOOD] (define-fun s23 () Int (q2 false s22))
[GOOD] (define-fun s25 () Bool (= s23 s24))
[GOOD] (define-fun s26 () Int (q2 false s3))
[GOOD] (define-fun s27 () Bool (= s5 s26))
[GOOD] (define-fun s29 () (_ FloatingPoint 8 24) (q3 s28 true s3))
[GOOD] (define-fun s30 () Bool (fp.eq s28 s29))
[GOOD] (define-fun s33 () (_ FloatingPoint 8 24) (q3 s31 true s32))
[GOOD] (define-fun s34 () Bool (fp.isZero s33))
[GOOD] (define-fun s35 () Bool (fp.isNegative s33))
[GOOD] (define-fun s36 () Bool (and s34 s35))
[GOOD] (define-fun s38 () (_ FloatingPoint 8 24) (q3 s31 false s37))
[GOOD] (define-fun s40 () Bool (fp.eq s38 s39))
[GOOD] (define-fun s43 () (_ FloatingPoint 8 24) (q4 s41 s42))
[GOOD] (define-fun s45 () Bool (fp.eq s43 s44))
[GOOD] (define-fun s47 () (_ FloatingPoint 8 24) (q4 s41 s46))
[GOOD] (define-fun s49 () Bool (fp.eq s47 s48))
[GOOD] (define-fun s52 () (_ FloatingPoint 8 24) (q4 s50 s51))
[GOOD] (define-fun s54 () Bool (fp.eq s52 s53))
[GOOD] (define-fun s57 () Int (q5 s55 s56))
[GOOD] (define-fun s58 () Bool (= s22 s57))
[GOOD] (define-fun s61 () Int (q5 s59 s60))
[GOOD] (define-fun s63 () Bool (= s61 s62))
[GOOD] (define-fun s66 () Int (q5 s64 s65))
[GOOD] (define-fun s68 () Bool (= s66 s67))
[GOOD] (define-fun s69 () Bool (q6 s17))
[GOOD] (define-fun s70 () Bool (not s69))
[GOOD] (define-fun s71 () Bool (or s69 s70))
[GOOD] (assert s4)
[GOOD] (assert s8)
[GOOD] (assert s12)
[GOOD] (assert s16)
[GOOD] (assert s21)
[GOOD] (assert s25)
[GOOD] (assert s27)
[GOOD] (assert s30)
[GOOD] (assert s36)
[GOOD] (assert s40)
[GOOD] (assert s45)
[GOOD] (assert s49)
[GOOD] (assert s54)
[GOOD] (assert s58)
[GOOD] (assert s63)
[GOOD] (assert s68)
[GOOD] (assert s71)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Int))
(ite (= x!1 0) 1 (ite (= x!1 (- 3)) 9 (ite (= x!1 3) 75 12))))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Int))
(ite (and (not x!1) (= x!2 12)) 3 (ite (and (not x!1) (= x!2 7)) 6 5)))))
[SEND] (get-value (q3))
[RECV] ((q3 (lambda ((x!1 (_ FloatingPoint 8 24)) (x!2 Bool) (x!3 Int))
(ite (and (= x!1 (fp #b0 #x82 #b00110011001100110011010)) (not x!2) (= x!3 8))
(_ +oo 8 24)
(ite (and (= x!1 (fp #b0 #x82 #b00110011001100110011010))
x!2
(= x!3 121))
(_ -zero 8 24)
(fp #b0 #x82 #b00010011001100110011010))))))
[SEND] (get-value (q4))
[RECV] ((q4 (lambda ((x!1 (_ BitVec 8)) (x!2 String))
(ite (and (= x!1 #x72) (= x!2 "foo"))
(fp #b0 #x80 #b11000000000000000000000)
(ite (and (= x!1 #x63) (= x!2 "tey"))
(fp #b0 #x85 #b01110000000000000000000)
(fp #b0 #x85 #b00111000000000000000000))))))
[SEND] (get-value (q5))
[RECV] ((q5 (lambda ((x!1 (Seq Int)) (x!2 (Seq (_ FloatingPoint 8 24))))
(ite (and (= x!1 (seq.unit 5))
(= x!2
(seq.++ (seq.unit (fp #b0 #x82 #b00000110011001100110011))
(seq.unit (_ +zero 8 24)))))
210
(ite (and (= x!1 (seq.++ (seq.unit 9) (seq.unit 5)))
(= x!2
(seq.++ (seq.unit (fp #b0 #x82 #b00000110011001100110011))
(seq.unit (fp #b0 #x82 #b00100000000000000000000)))))
21
7)))))
[SEND] (get-value (q6))
[RECV] ((q6 ((as const Array) false)))
*** Solver : Z3
*** Exit code: ExitSuccess
FINAL:
(([(0,1),(-3,9),(3,75)],12),([((False,12),3),((False,7),6)],5),([((9.6,False,8),Infinity),((9.6,True,121),-0.0)],8.6),([(('r',"foo"),3.5),(('c',"tey"),92.0)],78.0),([(([5],[8.2,0.0]),210),(([9,5],[8.2,9.0]),21)],7),([],False))
DONE!