** 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!