New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

Floating point exception on integer formula #4910

Closed

rainoftime opened this issue Dec 20, 2020 · 0 comments

Contributor

rainoftime commented Dec 20, 2020 •

edited

Loading

Hi, for the following formula,
z3 359d66b

(declare-fun v2 () Bool)
(assert (< (ite (> 1 (ite v2 1 2)) 0 3) 1))
(check-sat)
(check-sat-using (then simplify qffd))

./z3  file.smt2 
unsat
Floating point exception

The text was updated successfully, but these errors were encountered:

NikolajBjorner closed this as completed in

8e0a2c9

# for free to join this conversation on GitHub. Already have an account? # to comment