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

(factor) Segfault on QF_NRA formula #4736

Closed

wintered opened this issue Oct 14, 2020 · 0 comments

wintered commented Oct 14, 2020

Hi,
on the following formula, Z3 throws a segfault.

[540] % z3release small.smt2
Segmentation fault
[541] % 
[541] % cat small.smt2
(declare-const a Real)
(assert (> (- (* 2.0 a) (* a a)) 1.0 1.0))
(apply factor)
[542]

OS: Ubuntu 18.04
Commit: 2841796

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

NikolajBjorner closed this as completed in

0e1def5

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