Bug in SMTInterpol version 2.1-218-g29b232d

bug.smt2

(set-logic QF_UFLIRA)
(set-option :verbosity 2)
(define-fun T ((%init Bool) ($x$0 Real) ($y$0 Int) ($ok1$0 Bool) ($ok2$0 Bool) ($x$1 Real) ($y$1 Int) ($ok1$1 Bool) ($ok2$1 Bool)) Bool (and (= $ok1$1 (= (div $y$1 5) (to_int (/ (to_real $y$1) (/ 50 10))))) (= $ok2$1 (= (div (to_int $x$1) 5) (to_int (/ $x$1 (/ 50 10)))))))
(declare-fun %init () Bool)
(declare-fun $x$~1 () Real)
(declare-fun $y$~1 () Int)
(declare-fun $ok1$~1 () Bool)
(declare-fun $ok2$~1 () Bool)
(declare-fun $x$0 () Real)
(declare-fun $y$0 () Int)
(declare-fun $ok1$0 () Bool)
(declare-fun $ok2$0 () Bool)
(assert (T true $x$~1 $y$~1 $ok1$~1 $ok2$~1 $x$0 $y$0 $ok1$0 $ok2$0))
(push 1)
(assert (not (and $ok1$0 $ok2$0)))
(check-sat)
(pop 1)
(assert $ok1$0)
(assert $ok2$0)
(declare-fun $x$1 () Real)
(declare-fun $y$1 () Int)
(declare-fun $ok1$1 () Bool)
(declare-fun $ok2$1 () Bool)
(assert (T false $x$0 $y$0 $ok1$0 $ok2$0 $x$1 $y$1 $ok1$1 $ok2$1))
(push 1)
(assert (not (and $ok1$1 $ok2$1)))
(check-sat)
(pop 1)
(assert $ok1$1)
(assert $ok2$1)
(declare-fun $x$2 () Real)
(declare-fun $y$2 () Int)
(declare-fun $ok1$2 () Bool)
(declare-fun $ok2$2 () Bool)
(assert (T false $x$1 $y$1 $ok1$1 $ok2$1 $x$2 $y$2 $ok1$2 $ok2$2))
(push 1)
(assert (not (and $ok1$2 $ok2$2)))
(check-sat)
(pop 1)
(assert $ok1$2)
(assert $ok2$2)
(declare-fun $x$3 () Real)
(declare-fun $y$3 () Int)
(declare-fun $ok1$3 () Bool)
(declare-fun $ok2$3 () Bool)
(assert (T false $x$2 $y$2 $ok1$2 $ok2$2 $x$3 $y$3 $ok1$3 $ok2$3))
(push 1)
(assert (not (and $ok1$3 $ok2$3)))
(check-sat)
(pop 1)
(assert $ok1$3)
(assert $ok2$3)
(declare-fun $x$4 () Real)
(declare-fun $y$4 () Int)
(declare-fun $ok1$4 () Bool)
(declare-fun $ok2$4 () Bool)
(assert (T false $x$3 $y$3 $ok1$3 $ok2$3 $x$4 $y$4 $ok1$4 $ok2$4))
(push 1)
(assert (not (and $ok1$4 $ok2$4)))
(check-sat)
(pop 1)
(assert $ok1$4)
(assert $ok2$4)
(declare-fun $x$5 () Real)
(declare-fun $y$5 () Int)
(declare-fun $ok1$5 () Bool)
(declare-fun $ok2$5 () Bool)
(assert (T false $x$4 $y$4 $ok1$4 $ok2$4 $x$5 $y$5 $ok1$5 $ok2$5))
(push 1)
(assert (not (and $ok1$5 $ok2$5)))
(check-sat)
(pop 1)
(assert $ok1$5)
(assert $ok2$5)
(declare-fun $x$6 () Real)
(declare-fun $y$6 () Int)
(declare-fun $ok1$6 () Bool)
(declare-fun $ok2$6 () Bool)
(assert (T false $x$5 $y$5 $ok1$5 $ok2$5 $x$6 $y$6 $ok1$6 $ok2$6))
(push 1)
(assert (not (and $ok1$6 $ok2$6)))
(check-sat)
(pop 1)
(assert $ok1$6)
(assert $ok2$6)
(declare-fun $x$7 () Real)
(declare-fun $y$7 () Int)
(declare-fun $ok1$7 () Bool)
(declare-fun $ok2$7 () Bool)
(assert (T false $x$6 $y$6 $ok1$6 $ok2$6 $x$7 $y$7 $ok1$7 $ok2$7))
(push 1)
(assert (not (and $ok1$7 $ok2$7)))
(check-sat)
(pop 1)
(assert $ok1$7)
(assert $ok2$7)
(declare-fun $x$8 () Real)
(declare-fun $y$8 () Int)
(declare-fun $ok1$8 () Bool)
(declare-fun $ok2$8 () Bool)
(assert (T false $x$7 $y$7 $ok1$7 $ok2$7 $x$8 $y$8 $ok1$8 $ok2$8))
(push 1)
(assert (not (and $ok1$8 $ok2$8)))
(check-sat)
(pop 1)
(assert $ok1$8)
(assert $ok2$8)
(declare-fun $x$9 () Real)
(declare-fun $y$9 () Int)
(declare-fun $ok1$9 () Bool)
(declare-fun $ok2$9 () Bool)
(assert (T false $x$8 $y$8 $ok1$8 $ok2$8 $x$9 $y$9 $ok1$9 $ok2$9))
(push 1)
(assert (not (and $ok1$9 $ok2$9)))
(check-sat)
(get-model)