test/regress/regress0/bug239.smtv1.smt2

   1 (set-option :incremental false)
   2 (set-info :status sat)
   3 (set-logic QF_LRA)
   4 (declare-fun v0 () Real)
   5 (declare-fun v1 () Real)
   6 (declare-fun v2 () Real)
   7 (check-sat-assuming ( (let ((_let_0 (* v1 5.0))) (let ((_let_1 (- v0 (- v2 v1)))) (let ((_let_2 (* v0 (/ (- 5) 1)))) (let ((_let_3 (+ (- v0) _let_0))) (let ((_let_4 (/ 0 (- 2)))) (let ((_let_5 (<= v2 _let_0))) (let ((_let_6 (<= _let_2 _let_2))) (let ((_let_7 (= _let_2 _let_3))) (let ((_let_8 (<= _let_0 _let_4))) (let ((_let_9 (> _let_4 v1))) (let ((_let_10 (= (- v0) _let_2))) (let ((_let_11 (>= (- v0) _let_3))) (let ((_let_12 (< _let_1 v2))) (let ((_let_13 (= (+ v0 v1) _let_0))) (let ((_let_14 (distinct (/ 0 (- 5)) _let_2))) (let ((_let_15 (ite _let_10 v2 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1))))) (let ((_let_16 (ite _let_14 (/ 0 (- 5)) (/ 0 (- 5))))) (let ((_let_17 (ite _let_8 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1)) v0))) (let ((_let_18 (ite (< v0 _let_1) (- v2 v1) _let_1))) (let ((_let_19 (ite _let_11 _let_2 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1))))) (let ((_let_20 (ite _let_13 v1 (- v0)))) (let ((_let_21 (ite _let_11 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1)) (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1))))) (let ((_let_22 (ite _let_13 v0 _let_4))) (let ((_let_23 (ite (>= _let_1 (- v0)) (ite _let_9 _let_0 _let_2) v2))) (let ((_let_24 (ite _let_6 (+ v0 v1) v2))) (let ((_let_25 (ite _let_9 _let_2 _let_0))) (let ((_let_26 (ite _let_12 (ite _let_10 _let_4 _let_16) v2))) (let ((_let_27 (ite (< v0 _let_1) v1 _let_0))) (let ((_let_28 (distinct _let_4 _let_26))) (let ((_let_29 (< (- v0) (- v0)))) (let ((_let_30 (=> (> (ite _let_7 (- v0) _let_3) _let_0) (< (- v2 v1) _let_25)))) (=> (= (=> _let_28 (< _let_16 (- v0))) (or (and (xor (= (<= (ite _let_14 _let_4 v1) _let_3) (> v2 (- v2 v1))) (= (not (distinct _let_21 _let_23)) (> (- v0) (ite _let_9 _let_0 _let_2)))) (ite (<= (ite _let_10 _let_4 _let_16) _let_19) (>= v0 (/ 0 (- 5))) (= (= _let_27 _let_15) (> _let_4 (+ v0 v1))))) (or (and _let_30 _let_30) (= (or (<= (- v0) v0) (not _let_28)) (ite (xor (< _let_2 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1))) (= _let_27 v0)) (xor _let_7 (= (<= _let_24 _let_19) (>= _let_2 _let_24))) (> _let_22 _let_0)))))) (and (and (or (or (< v1 _let_2) (= (- v2 v1) _let_16)) (= (=> (or (>= _let_1 (- v0)) (distinct _let_17 _let_27)) (not (=> (> _let_16 v2) (= (ite _let_10 _let_4 _let_16) _let_21)))) (xor (= (>= (ite _let_10 _let_4 _let_16) _let_17) (or (= (>= _let_23 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1))) (distinct (ite _let_9 _let_0 _let_2) _let_22)) (= _let_17 v0))) (and (=> (= _let_18 _let_20) (>= _let_21 _let_26)) (<= (/ 0 (- 5)) (- v2 v1)))))) (not (distinct _let_1 (- v2 v1)))) (xor (=> (distinct _let_4 _let_25) (or (xor (or (or (= _let_27 _let_2) (= _let_25 _let_4)) (= (= _let_19 _let_0) (=> (ite _let_5 (<= _let_16 _let_24) (<= _let_2 v0)) _let_10))) (and (<= v1 (/ 0 (- 5))) (< _let_22 _let_27))) (xor (and (= (/ 0 (- 5)) _let_26) (>= _let_20 (ite (distinct _let_1 (- v2 v1)) _let_3 (+ v0 v1)))) (not (>= (ite _let_5 _let_27 _let_3) _let_15))))) (or (or (and (= (- v2 v1) v0) (= _let_20 _let_16)) (not (= (< v2 (/ 0 (- 5))) (= (or (>= _let_2 _let_23) _let_13) (=> _let_9 (xor (<= _let_18 _let_26) (>= (- v0) _let_17))))))) (ite (ite (= (>= v2 _let_4) (= (< (/ 0 (- 5)) _let_0) (ite (distinct (- v0) _let_1) (= _let_18 (- v2 v1)) (= _let_16 _let_15)))) (or (< v0 _let_1) (=> _let_29 _let_29)) (=> (< _let_15 _let_4) (ite (xor _let_14 _let_8) _let_11 (distinct _let_27 _let_27)))) (and (xor (= _let_2 (- v2 v1)) (< _let_26 v2)) _let_6) (or _let_12 (< _let_23 v0)))))))))))))))))))))))))))))))))))))) ))