Refutation soundness issue on LIRA formula

[rainoftime]

Hi, for the following instance,
ostrich 2b3eb9b yields unsat,
but z3 and cvc4 return sat

(declare-const v0 Bool)
(declare-const i1 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r7 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const v1 Bool)
(declare-const i11 Int)
(assert (exists ((q0 Real) (q1 Int) (q2 Bool)) (and (> 6188.141477 r10) (= q2 q2 q2 v0 q2 q2 (> r7 3046306.76 6188.141477 153479756.0 r3) v1 v1 q2 q2) (<= i5 50))))
(assert (or (exists ((q0 Real) (q1 Int) (q2 Bool)) (=> (= 6188.141477 r0 6188.141477) (> 50 q1))) (exists ((q0 Real) (q1 Int) (q2 Bool)) v0)))
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const r12 Real)
(declare-const v4 Bool)
(declare-const r13 Real)
(assert (exists ((q3 Bool) (q4 Int) (q5 Bool) (q6 Int)) (>= 72 72)))
(declare-const v5 Bool)
(declare-const r14 Real)
(declare-const i12 Int)
(declare-const v6 Bool)
(declare-const i13 Int)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const r15 Real)
(assert (not (forall ((q7 Real) (q8 Real) (q9 Real)) (not (< 6.0 q9)))))
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i14 Int)
(declare-const r16 Real)
(declare-const r17 Real)
(declare-const v12 Bool)
(declare-const r18 Real)
(declare-const r19 Real)
(declare-const v13 Bool)
(declare-const r20 Real)
(declare-const r21 Real)
(declare-const r22 Real)
(declare-const r23 Real)
(declare-const r24 Real)
(declare-const r25 Real)
(declare-const r26 Real)
(declare-const r27 Real)
(assert (not (forall ((q10 Real) (q11 Bool) (q12 Bool) (q13 Bool)) (not (not (> 33 (abs (to_int (* 3046306.76 90232.0 (- r0 (to_real i4) 90232.0 r12)))) 314 165 (to_int (/ r7 3046306.76))))))))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (>= 72 72) (>= 72 72) false))
(assert (or (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) false))
(assert (or (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) (>= 72 72) (= (/ r7 3046306.76) 6.0) false))
(assert (or (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (>= 72 72) (>= 72 72) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (>= 72 72) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (= (/ r7 3046306.76) 6.0) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (>= 72 72) (= (/ r7 3046306.76) 6.0) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (>= 72 72) false))
(assert (or (= (/ r7 3046306.76) 6.0) false))
(assert (or (>= 72 72) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) (>= 72 72) (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(assert (or (and (is_int 90232.0) (is_int 90232.0) (<= 33 96) (<= 33 96) (<= 33 96) (not (is_int r3)) (<= 33 96) (is_int 90232.0)) false))
(check-sat)