path: root/test/regress/regress2/bug148.smtv1.smt2

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(check-sat-assuming ( (let ((_let_0 (/ 12 12))) (let ((_let_1 (+ (- (- v0) (+ (+ v0 v0) (- v0))) _let_0))) (let ((_let_2 (/ 1 (- 12)))) (let ((_let_3 (> (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))))) (let ((_let_4 (distinct (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0)))) (let ((_let_5 (<= (- (- v0) (+ (+ v0 v0) (- v0))) (- (- v0) (+ (+ v0 v0) (- v0)))))) (let ((_let_6 (distinct _let_0 v0))) (let ((_let_7 (>= _let_1 v0))) (let ((_let_8 (<= (+ (+ v0 v0) (- v0)) (- v0)))) (let ((_let_9 (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) v0 _let_0))) (let ((_let_10 (ite _let_7 (- (- v0) (+ (+ v0 v0) (- v0))) v0))) (let ((_let_11 (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) _let_1 v0))) (let ((_let_12 (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (- (- v0) (+ (+ v0 v0) (- v0))) (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2)))) (let ((_let_13 (ite _let_7 _let_0 _let_1))) (let ((_let_14 (ite _let_5 (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (* (+ (+ v0 v0) (- v0)) 12.0) (- (- v0) (+ (+ v0 v0) (- v0)))) _let_0))) (let ((_let_15 (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (* (+ (+ v0 v0) (- v0)) 12.0) (+ (+ v0 v0) (- v0))))) (let ((_let_16 (ite (<= _let_0 (- (- v0) (+ (+ v0 v0) (- v0)))) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0))) _let_12))) (let ((_let_17 (ite (<= _let_2 (+ v0 v0)) _let_11 (- (- (- v0) (+ (+ v0 v0) (- v0))))))) (let ((_let_18 (=> (and (not (=> (xor (=> _let_3 (=> (ite (= (< _let_9 (+ (+ v0 v0) (- v0))) (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0))) (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (=> (=> (<= _let_1 _let_12) (<= _let_0 (- (- v0) (+ (+ v0 v0) (- v0))))) (< (+ v0 v0) (+ (+ v0 v0) (- v0))))) (xor (>= _let_14 v0) (<= _let_12 _let_16)))) (not (and (or (<= _let_2 (+ v0 v0)) (< (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) _let_14)) (> _let_2 v0)))) (ite (or (xor (> (- (- v0) (+ (+ v0 v0) (- v0))) _let_17) (or (or (<= _let_9 _let_9) (<= (+ v0 v0) (- v0))) (distinct _let_9 _let_0))) (= (ite _let_3 (- v0) (+ v0 v0)) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0)))) (=> (= (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0)))) (or (or (< (- (- v0) (+ (+ v0 v0) (- v0))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) _let_0 _let_10)) (< (ite _let_4 _let_12 _let_11) _let_14)) (<= (ite _let_6 _let_11 _let_16) _let_16))) (not (< (- (- (- v0) (+ (+ v0 v0) (- v0)))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0))))))) (not (=> (xor (=> _let_3 (=> (ite (= (< _let_9 (+ (+ v0 v0) (- v0))) (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0))) (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (=> (=> (<= _let_1 _let_12) (<= _let_0 (- (- v0) (+ (+ v0 v0) (- v0))))) (< (+ v0 v0) (+ (+ v0 v0) (- v0))))) (xor (>= _let_14 v0) (<= _let_12 _let_16)))) (not (and (or (<= _let_2 (+ v0 v0)) (< (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) _let_14)) (> _let_2 v0)))) (ite (or (xor (> (- (- v0) (+ (+ v0 v0) (- v0))) _let_17) (or (or (<= _let_9 _let_9) (<= (+ v0 v0) (- v0))) (distinct _let_9 _let_0))) (= (ite _let_3 (- v0) (+ v0 v0)) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0)))) (=> (= (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0)))) (or (or (< (- (- v0) (+ (+ v0 v0) (- v0))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) _let_0 _let_10)) (< (ite _let_4 _let_12 _let_11) _let_14)) (<= (ite _let_6 _let_11 _let_16) _let_16))) (not (< (- (- (- v0) (+ (+ v0 v0) (- v0)))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0)))))))) (and (not (=> (xor (=> _let_3 (=> (ite (= (< _let_9 (+ (+ v0 v0) (- v0))) (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0))) (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (=> (=> (<= _let_1 _let_12) (<= _let_0 (- (- v0) (+ (+ v0 v0) (- v0))))) (< (+ v0 v0) (+ (+ v0 v0) (- v0))))) (xor (>= _let_14 v0) (<= _let_12 _let_16)))) (not (and (or (<= _let_2 (+ v0 v0)) (< (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) _let_14)) (> _let_2 v0)))) (ite (or (xor (> (- (- v0) (+ (+ v0 v0) (- v0))) _let_17) (or (or (<= _let_9 _let_9) (<= (+ v0 v0) (- v0))) (distinct _let_9 _let_0))) (= (ite _let_3 (- v0) (+ v0 v0)) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0)))) (=> (= (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0)))) (or (or (< (- (- v0) (+ (+ v0 v0) (- v0))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) _let_0 _let_10)) (< (ite _let_4 _let_12 _let_11) _let_14)) (<= (ite _let_6 _let_11 _let_16) _let_16))) (not (< (- (- (- v0) (+ (+ v0 v0) (- v0)))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0))))))) (not (=> (xor (=> _let_3 (=> (ite (= (< _let_9 (+ (+ v0 v0) (- v0))) (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0))) (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (=> (=> (<= _let_1 _let_12) (<= _let_0 (- (- v0) (+ (+ v0 v0) (- v0))))) (< (+ v0 v0) (+ (+ v0 v0) (- v0))))) (xor (>= _let_14 v0) (<= _let_12 _let_16)))) (not (and (or (<= _let_2 (+ v0 v0)) (< (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) _let_14)) (> _let_2 v0)))) (ite (or (xor (> (- (- v0) (+ (+ v0 v0) (- v0))) _let_17) (or (or (<= _let_9 _let_9) (<= (+ v0 v0) (- v0))) (distinct _let_9 _let_0))) (= (ite _let_3 (- v0) (+ v0 v0)) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0)))) (=> (= (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (- v0) _let_2) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0)))) (or (or (< (- (- v0) (+ (+ v0 v0) (- v0))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) _let_0 _let_10)) (< (ite _let_4 _let_12 _let_11) _let_14)) (<= (ite _let_6 _let_11 _let_16) _let_16))) (not (< (- (- (- v0) (+ (+ v0 v0) (- v0)))) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0))))))))))) (let ((_let_19 (or (= (xor (ite _let_4 _let_4 (=> (= (> (- (- (- v0) (+ (+ v0 v0) (- v0)))) _let_16) (= (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (* (+ (+ v0 v0) (- v0)) 12.0) (- (- v0) (+ (+ v0 v0) (- v0)))) _let_16)) (distinct (* (+ (+ v0 v0) (- v0)) 12.0) _let_9))) (and (distinct _let_11 _let_15) (distinct _let_11 _let_15))) (xor (and (or (distinct _let_1 _let_17) _let_8) (or (distinct _let_1 _let_17) _let_8)) (= (=> (xor (ite (and (or (= (<= (+ v0 v0) _let_14) (and _let_6 (or (< _let_13 _let_12) (ite (<= (- v0) (- v0)) (ite _let_7 (>= (ite _let_4 _let_12 _let_11) (- v0)) (<= _let_13 _let_10)) (<= (- v0) (- v0)))))) (>= _let_11 _let_15)) (or (>= _let_2 (- (- v0) (+ (+ v0 v0) (- v0)))) (< _let_14 (+ v0 v0)))) (< (ite _let_6 _let_11 _let_16) (ite _let_8 _let_1 (+ v0 v0))) (xor (and (xor (=> _let_5 (>= (- (- v0) (+ (+ v0 v0) (- v0))) (* (+ (+ v0 v0) (- v0)) 12.0))) (>= v0 _let_13)) (> _let_0 _let_17)) (= (> (+ (+ v0 v0) (- v0)) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0))) (> (+ (+ v0 v0) (- v0)) _let_12)))) (> _let_0 (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0))))) (and (>= _let_2 _let_0) (=> (<= v0 _let_9) (distinct _let_16 _let_0)))) (and (>= v0 _let_10) (not (> (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0))) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0))))))))) (= (xor (ite _let_4 _let_4 (=> (= (> (- (- (- v0) (+ (+ v0 v0) (- v0)))) _let_16) (= (ite (> _let_1 (* (+ (+ v0 v0) (- v0)) 12.0)) (* (+ (+ v0 v0) (- v0)) 12.0) (- (- v0) (+ (+ v0 v0) (- v0)))) _let_16)) (distinct (* (+ (+ v0 v0) (- v0)) 12.0) _let_9))) (and (distinct _let_11 _let_15) (distinct _let_11 _let_15))) (xor (and (or (distinct _let_1 _let_17) _let_8) (or (distinct _let_1 _let_17) _let_8)) (= (=> (xor (ite (and (or (= (<= (+ v0 v0) _let_14) (and _let_6 (or (< _let_13 _let_12) (ite (<= (- v0) (- v0)) (ite _let_7 (>= (ite _let_4 _let_12 _let_11) (- v0)) (<= _let_13 _let_10)) (<= (- v0) (- v0)))))) (>= _let_11 _let_15)) (or (>= _let_2 (- (- v0) (+ (+ v0 v0) (- v0)))) (< _let_14 (+ v0 v0)))) (< (ite _let_6 _let_11 _let_16) (ite _let_8 _let_1 (+ v0 v0))) (xor (and (xor (=> _let_5 (>= (- (- v0) (+ (+ v0 v0) (- v0))) (* (+ (+ v0 v0) (- v0)) 12.0))) (>= v0 _let_13)) (> _let_0 _let_17)) (= (> (+ (+ v0 v0) (- v0)) (ite (< (+ v0 v0) (+ (+ v0 v0) (- v0))) (- (- (- v0) (+ (+ v0 v0) (- v0)))) (- v0))) (> (+ (+ v0 v0) (- v0)) _let_12)))) (> _let_0 (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0))))) (and (>= _let_2 _let_0) (=> (<= v0 _let_9) (distinct _let_16 _let_0)))) (and (>= v0 _let_10) (not (> (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0))) (ite (distinct (* (+ (+ v0 v0) (- v0)) 12.0) (- (- (- v0) (+ (+ v0 v0) (- v0))))) (+ (+ v0 v0) (- v0)) (+ (+ v0 v0) (- v0)))))))))))) (=> (or _let_18 _let_18) (=> _let_19 _let_19)))))))))))))))))))))) ))