-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Consolidated] Invalid model for integer formulas #4923
Comments
Another formula
A simpler formula
|
Another one
|
|
|
|
|
NikolajBjorner
added a commit
that referenced
this issue
Jan 9, 2021
#4923 (comment) - this is abuse of tactic and logic setting. Tactics are not part of SMTLIB standards, logics are, but you are disabling bit-vector reasoning in QF_AUFLIA. On the other hand, bit-vectors are introduced by eq2bv. |
Similar to other bugs: abuse of qffd is on your own. |
Remaining bug is: #4923 (comment) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi, for the following formula
z3 799de71
In debug build, the formula triggers an assertion error
The text was updated successfully, but these errors were encountered: