** 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] ; --- 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 s21 () Int 5) [GOOD] (define-fun s23 () Int 7) [GOOD] (define-fun s25 () Int 6) [GOOD] (define-fun s29 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0))) [GOOD] (define-fun s32 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0))) [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) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) [GOOD] (define-fun s47 () String "tey") [GOOD] (define-fun s49 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0))) [GOOD] (define-fun s51 () String (_ char #x72)) [GOOD] (define-fun s52 () String "foo") [GOOD] (define-fun s54 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) [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 ((_ 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 Int) (seq.++ (seq.unit 9) (seq.unit 5))) [GOOD] (define-fun s61 () (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 s63 () Int 21) [GOOD] (define-fun s65 () (Seq Int) (seq.unit 5)) [GOOD] (define-fun s66 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (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] (declare-fun s70 () Int) ; tracks user variable "__internal_sbv_s70" [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] (declare-fun q6 (Int) Bool) [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] (define-fun s71 () Bool (q6 s70)) [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 (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))) [SEND] (get-value (q6)) [RECV] ((q6 (_ as-array q6))) *** Solver : Z3 *** Exit code: ExitSuccess FINAL: (Right ([(0,1),(-3,9),(3,75)],12),Right ([((False,12),3),((False,7),6)],5),Right ([((9.6,False,8),Infinity),((9.6,True,121),-0.0)],8.6),Right ([(('r',"foo"),3.5),(('c',"tey"),92.0)],78.0),Right ([(([5],[8.2,0.0]),210),(([9,5],[8.2,9.0]),21)],7),Right ([],False)) DONE!