-
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
incorrect unsat answer on VC #6270
Comments
running with solver.axioms2files=true produces a ton of files (I had to fix a few bugs in how the files are generated). Some of the files are SAT (z3 returns unknown, but it is really SAT), which pinpoints the bug. The next step is to break or log more at the offending lemma (for me it is lemma number 10465 when using smt.random_seed=3). |
Turns out the theory axioms all double checked.
It produces
|
The command-line doesn't repro well with the above API based minimization.
The bug appears to be that MBQI introduces fresh distinct values for elements in the domain of zero_8_t. |
Not sure, but the following minimization/reduction might be of help:
|
great! thanks for the fix and the fantastic investigation, looks like it was a fun one... |
Z3 4.10 immediately returns unsat on the VC below, which should be satisfiable (although it's hard to check due to the encoding). Other provers return unknown immediately, and any slight change to the VC also makes Z3 return unknown. For example, removing the first declaration for datatype int__ref (which is unused) causes Z3 to return unknown immediately. Or removing the assertion on line 36 giving the value of (unused) constant two_power_size_minus_one also causes Z3 to return unknown immediately.
I reduced the VC as much as I could, but every new removal seems to make the problem go away.
Can I do something on my side to help diagnose the issue further?
The text was updated successfully, but these errors were encountered: