Hi,
For this formula,
(declare-fun a () Int)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< a 0))
(assert (= (/ 2.0 b c) 1.0))
(check-sat)
(check-sat)
Two (check-sat)s give different answers:
[504] % z3 small.smt2
unknown
sat
[505] %
[505] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< a 0))
(assert (= (/ 2.0 b c) 1.0))
(check-sat)
(check-sat)
[506] %
Changing a's type to Real or changing 2.0 to 1.0 makes it disappear.
OS: Ubuntu 18.04
Revision: 1ac365c
Hi,
For this formula,
Two (check-sat)s give different answers:
Changing a's type to Real or changing 2.0 to 1.0 makes it disappear.
OS: Ubuntu 18.04
Revision: 1ac365c