bug.smt2

(set-logic QF_UFLIRA)

(declare-fun i1 () Int)
(declare-fun i2 () Int)

(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)

(declare-fun r1 () Real)
(declare-fun r2 () Real)
(declare-fun r3 () Real)
(declare-fun r4 () Real)

(define-fun T ((i1 Int) (i2 Int) (b1 Bool) (b2 Bool) (b3 Bool) (r1 Real) (r2 Real) (r3 Real) (r4 Real)) Bool
  (and
    (= b1 (> (* 82000082 (- i2 2000002)) (* 71000071 (- i1 21000021))))
    (= b2 (> (* 23000023 (- i2 95000095)) (* (- 0 88000088) (- i1 24000024))))
    (= b3 (and (<= (to_real i1) 100000000)
               (>= (to_real i1) (- 0 100000000))
               (<= (to_real i2) 100000000)
               (>= (to_real i2) (- 0 100000000))))
    (= r1 (+ (* (- (to_real i1) (/ 7383010391 100)) (/ 175130129 100)) (* (- (to_real i2) (/ 5816381767 100)) (- 0 (/ 180962975 100)))))
    (= r2 (+ (* (- (to_real i1) (/ 6135550551 100)) (- 0 (/ 375585701 100))) (* (- (to_real i2) (/ 4335022594 100)) (/ 315625622 100))))
    (= r3 (+ (* (- (to_real i1) (/ 6102838334 100)) (- 0 (/ 23464538 100))) (* (- (to_real i2) (/ 4296168199 100)) (- 0 (/ 27891245 100)))))
    (= r4 (+ (* (- (to_real i1) (/ 6087351739 100)) (- 0 (/ 23464538 100))) (* (- (to_real i2) (/ 4277759977 100)) (- 0 (/ 27891245 100)))))))

(assert (not (=> (and b3
                      (>= r1 0)
                      (>= r2 0)
                      (> r3 0)
                      (<= r4 0))
                 (not (and b1 b2)))))

(assert (T i1 i2 b1 b2 b3 r1 r2 r3 r4))

(check-sat)