z3-err

[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-logic ALL)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)
[GOOD] (define-fun s_1 () Bool true)
[GOOD] (define-fun s3 () Real (/ 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0 1.0))
[GOOD] (define-fun s57 () Real 0.0)
[GOOD] (define-fun s82 () Real (/ 1.0 2.0))
[GOOD] (define-fun s96 () String "Write succeeded")
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () String)
[GOOD] (declare-fun s1 () String)
[GOOD] (declare-fun s2 () Real)
[GOOD] (declare-fun s9 () Real)
[GOOD] (declare-fun s15 () Real)
[GOOD] (declare-fun s21 () String)
[GOOD] (declare-fun s22 () Real)
[GOOD] (declare-fun s28 () String)
[GOOD] (declare-fun s29 () Real)
[GOOD] (declare-fun s35 () String)
[GOOD] (declare-fun s36 () Real)
[GOOD] (declare-fun s42 () String)
[GOOD] (declare-fun s43 () Real)
[GOOD] (declare-fun s49 () Bool)
[GOOD] (declare-fun s50 () Bool)
[GOOD] (declare-fun s51 () Bool)
[GOOD] (declare-fun s52 () String)
[GOOD] (declare-fun s53 () Bool)
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] (declare-fun cells__accounts2__balance (String) Real)
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s4 () Real (* s2 s3))
[GOOD] (define-fun s5 () Int (to_int s4))
[GOOD] (define-fun s6 () Real (to_real s5))
[GOOD] (define-fun s7 () Real (/ s6 s3))
[GOOD] (define-fun s8 () Bool (= s2 s7))
[GOOD] (define-fun s10 () Real (* s3 s9))
[GOOD] (define-fun s11 () Int (to_int s10))
[GOOD] (define-fun s12 () Real (to_real s11))
[GOOD] (define-fun s13 () Real (/ s12 s3))
[GOOD] (define-fun s14 () Bool (= s9 s13))
[GOOD] (define-fun s16 () Real (* s3 s15))
[GOOD] (define-fun s17 () Int (to_int s16))
[GOOD] (define-fun s18 () Real (to_real s17))
[GOOD] (define-fun s19 () Real (/ s18 s3))
[GOOD] (define-fun s20 () Bool (= s15 s19))
[GOOD] (define-fun s23 () Real (* s3 s22))
[GOOD] (define-fun s24 () Int (to_int s23))
[GOOD] (define-fun s25 () Real (to_real s24))
[GOOD] (define-fun s26 () Real (/ s25 s3))
[GOOD] (define-fun s27 () Bool (= s22 s26))
[GOOD] (define-fun s30 () Real (* s3 s29))
[GOOD] (define-fun s31 () Int (to_int s30))
[GOOD] (define-fun s32 () Real (to_real s31))
[GOOD] (define-fun s33 () Real (/ s32 s3))
[GOOD] (define-fun s34 () Bool (= s29 s33))
[GOOD] (define-fun s37 () Real (* s3 s36))
[GOOD] (define-fun s38 () Int (to_int s37))
[GOOD] (define-fun s39 () Real (to_real s38))
[GOOD] (define-fun s40 () Real (/ s39 s3))
[GOOD] (define-fun s41 () Bool (= s36 s40))
[GOOD] (define-fun s44 () Real (* s3 s43))
[GOOD] (define-fun s45 () Int (to_int s44))
[GOOD] (define-fun s46 () Real (to_real s45))
[GOOD] (define-fun s47 () Real (/ s46 s3))
[GOOD] (define-fun s48 () Bool (= s43 s47))
[GOOD] (define-fun s54 () Bool (= s0 s21))
[GOOD] (define-fun s55 () Real (cells__accounts2__balance s0))
[GOOD] (define-fun s56 () Bool (= s22 s55))
[GOOD] (define-fun s58 () Bool (< s57 s55))
[GOOD] (define-fun s59 () Bool (= s55 s57))
[GOOD] (define-fun s60 () Bool (or s58 s59))
[GOOD] (define-fun s61 () Bool (= s9 s55))
[GOOD] (define-fun s62 () Bool (= s1 s28))
[GOOD] (define-fun s63 () Real (cells__accounts2__balance s1))
[GOOD] (define-fun s64 () Bool (= s29 s63))
[GOOD] (define-fun s65 () Bool (< s57 s63))
[GOOD] (define-fun s66 () Bool (= s57 s63))
[GOOD] (define-fun s67 () Bool (or s65 s66))
[GOOD] (define-fun s68 () Bool (= s15 s63))
[GOOD] (define-fun s69 () Bool (< s57 s2))
[GOOD] (define-fun s70 () Bool (= s49 s69))
[GOOD] (define-fun s71 () Bool (< s2 s55))
[GOOD] (define-fun s72 () Bool (= s2 s55))
[GOOD] (define-fun s73 () Bool (or s71 s72))
[GOOD] (define-fun s74 () Bool (= s50 s73))
[GOOD] (define-fun s75 () Bool (= s0 s1))
[GOOD] (define-fun s76 () Bool (not s75))
[GOOD] (define-fun s77 () Bool (= s51 s76))
[GOOD] (define-fun s78 () Bool (= s0 s35))
[GOOD] (define-fun s79 () Real (- s2))
[GOOD] (define-fun s80 () Real (+ s55 s79))
[GOOD] (define-fun s81 () Real (* s3 s80))
[GOOD] (define-fun s83 () Real (+ s81 s82))
[GOOD] (define-fun s84 () Int (to_int s83))
[GOOD] (define-fun s85 () Real (to_real s84))
[GOOD] (define-fun s86 () Real (/ s85 s3))
[GOOD] (define-fun s87 () Bool (= s36 s86))
[GOOD] (define-fun s88 () Bool (= s1 s42))
[GOOD] (define-fun s89 () Real (+ s2 s63))
[GOOD] (define-fun s90 () Real (* s3 s89))
[GOOD] (define-fun s91 () Real (+ s82 s90))
[GOOD] (define-fun s92 () Int (to_int s91))
[GOOD] (define-fun s93 () Real (to_real s92))
[GOOD] (define-fun s94 () Real (/ s93 s3))
[GOOD] (define-fun s95 () Bool (= s43 s94))
[GOOD] (define-fun s97 () Bool (= s52 s96))
[GOOD] (define-fun s98 () Bool (and s69 s73))
[GOOD] (define-fun s99 () Bool (and s76 s98))
[GOOD] (define-fun s100 () Bool (not s99))
[GOOD] (define-fun s101 () Real (- s55))
[GOOD] (define-fun s102 () Real (+ s86 s101))
[GOOD] (define-fun s103 () Real (ite s75 s86 s63))
[GOOD] (define-fun s104 () Real (- s103))
[GOOD] (define-fun s105 () Real (+ s94 s104))
[GOOD] (define-fun s106 () Real (+ s102 s105))
[GOOD] (define-fun s107 () Bool (= s57 s106))
[GOOD] (define-fun s108 () Bool (or s100 s107))
[GOOD] (assert s8)
[GOOD] (assert s14)
[GOOD] (assert s20)
[GOOD] (assert s27)
[GOOD] (assert s34)
[GOOD] (assert s41)
[GOOD] (assert s48)
[GOOD] (assert s53)
[GOOD] (assert s54)
[GOOD] (assert s56)
[GOOD] (assert s60)
[GOOD] (assert s61)
[GOOD] (assert s62)
[GOOD] (assert s64)
[GOOD] (assert s67)
[GOOD] (assert s68)
[GOOD] (assert s70)
[GOOD] (assert s74)
[GOOD] (assert s77)
[GOOD] (assert s78)
[GOOD] (assert s87)
[GOOD] (assert s88)
[GOOD] (assert s95)
[GOOD] (assert s97)
[GOOD] (assert (not s108))
[SEND] (check-sat)
[RECV] unknown
[SEND] (get-info :reason-unknown)
[RECV] (:reason-unknown "Sort mismatch at argument #2 for function (declare-fun >= (Real Real) Bool) supplied sort is Int")