test.z3

(set-option :global-declarations true)
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic ALL)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s3 () Real (/ 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0 1.0))
(define-fun s57 () Real 0.0)
(define-fun s82 () Real (/ 1.0 2.0))
(define-fun s96 () String "Write succeeded")
; --- skolem constants ---
(declare-fun s0 () String)
(declare-fun s1 () String)
(declare-fun s2 () Real)
(declare-fun s22 () Real)
(declare-fun s36 () Real)
(declare-fun s43 () Real)
(declare-fun s51 () Bool)
(declare-fun s52 () String)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
(declare-fun cells__accounts2__balance (String) Real)
; --- user given axioms ---
; --- formula ---
(define-fun s23 () Real (* s3 s22))
(define-fun s24 () Int (to_int s23))
(define-fun s25 () Real (to_real s24))
(define-fun s26 () Real (/ s25 s3))
(define-fun s27 () Bool (= s22 s26))
; (define-fun s27 () Bool true)
(define-fun s37 () Real (* s3 s36))
(define-fun s38 () Int (to_int s37))
(define-fun s39 () Real (to_real s38))
(define-fun s40 () Real (/ s39 s3))
(define-fun s41 () Bool (= s36 s40))
; (define-fun s41 () Bool true)
(define-fun s44 () Real (* s3 s43))
(define-fun s45 () Int (to_int s44))
(define-fun s46 () Real (to_real s45))
(define-fun s47 () Real (/ s46 s3))
(define-fun s48 () Bool (= s43 s47))
; (define-fun s48 () Bool true)
(define-fun s55 () Real (cells__accounts2__balance s0))
(define-fun s56 () Bool (= s22 s55))
(define-fun s58 () Bool (< s57 s55))
(define-fun s59 () Bool (= s55 s57))
(define-fun s60 () Bool (or s58 s59))
(define-fun s63 () Real (cells__accounts2__balance s1))
(define-fun s65 () Bool (< s57 s63))
(define-fun s66 () Bool (= s57 s63))
(define-fun s67 () Bool (or s65 s66))
(define-fun s69 () Bool (< s57 s2))
(define-fun s71 () Bool (< s2 s55))
(define-fun s72 () Bool (= s2 s55))
(define-fun s73 () Bool (or s71 s72))
(define-fun s75 () Bool (= s0 s1))
(define-fun s76 () Bool (not s75))
(define-fun s77 () Bool (= s51 s76))
(define-fun s79 () Real (- s2))
(define-fun s80 () Real (+ s55 s79))
(define-fun s81 () Real (* s3 s80))
(define-fun s83 () Real (+ s81 s82))
(define-fun s84 () Int (to_int s83))
(define-fun s85 () Real (to_real s84))
(define-fun s86 () Real (/ s85 s3))
(define-fun s87 () Bool (= s36 s86))
(define-fun s89 () Real (+ s2 s63))
(define-fun s90 () Real (* s3 s89))
(define-fun s91 () Real (+ s82 s90))
(define-fun s92 () Int (to_int s91))
(define-fun s93 () Real (to_real s92))
(define-fun s94 () Real (/ s93 s3))
(define-fun s95 () Bool (= s43 s94))
(define-fun s97 () Bool (= s52 s96))
(define-fun s98 () Bool (and s69 s73))
(define-fun s99 () Bool (and s76 s98))
(define-fun s100 () Bool (not s99))
(define-fun s101 () Real (- s55))
(define-fun s102 () Real (+ s86 s101))
(define-fun s103 () Real (ite s75 s86 s63))
(define-fun s104 () Real (- s103))
(define-fun s105 () Real (+ s94 s104))
(define-fun s106 () Real (+ s102 s105))
(define-fun s107 () Bool (= s57 s106))
(define-fun s108 () Bool (or s100 s107))
(assert s27)
(assert s41)
(assert s48)
(assert s56)
(assert s60)
(assert s67)
(assert s77)
(assert s87)
(assert s95)
(assert s97)
(assert (not s108))
(check-sat)
(get-info :reason-unknown)