-
Notifications
You must be signed in to change notification settings - Fork 260
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
Unsound verification with /proverOpt:O:smt.arith.solver=6 #4053
Comments
So far, I've reduced this to the following SMT-Lib file that Z3 says is unsat, but I believe shouldn't be.
Interestingly, If I remove the various quantified axioms about maps at the beginning, which aren't being used by the main asssertion, Z3 instead doesn't return. (This is with Z3 4.12.1.) |
Thanks for investigating this! It indeed looks interesting. May I know how to obtain such an SMT-Lib file from the Dafny code? So that I could also investigate further when I encounter such cases. |
The |
It seems that if I put everything before the |
|
An interesting additional data point. I generated SMT-Lib from the original problem above with Boogie's predicate, argument, and monomorphic encodings of the problem. All yield However, the reduced problem I posted above yields |
Another data point: the reduced axiom prefix I posted above only yields |
Narrowing this down further, if I take the SMT-Lib files produced by the monomorphic encoding and argument encoding of polymorphic types and comment out the actual verification problem at the end they become easily This is perhaps additional incentive to switch to the argument-based (or monomorphized) encoding of Boogie's polymorphic types when used from Dafny. I had already been experimenting with making that switch, because it seems to improve performance. Improving soundness as a side effect would be nice! :) |
I have three things to add. Quantifier modesIn Aaron's reduced SMT file above, there are no ground terms other than the To get Z3 to use the trigger mode, one needs to do two things: turn off Z3's auto-config and turn off Z3's model-based quantifier instantiation ( I don't know if the real numbers in @muchang's example provided those ground terms. Or could it be that A corrected encodingI corrected the encoding by hand, and that caused Z3 no longer to output One part is to change the 2-ary map type from
to
The 3 arguments to The other part is to add an antecedent to the previous
to make it:
I think Z3 will pick the trigger I stated here explicitly, but I'm not certain, so it seems best to add it manually. Here is the input I then fed to Z3:
The inconsistencyI didn't check all the details with the encoding above, here I think the proof of Suppose we're given variables
Note that in the SMT Lib input, Suppose further that we have a variable If we select from an Thus, we have that As the final blow, let's now pick The two previous paragraphs give the contradiction. |
Thanks for digging into the problem more deeply, @RustanLeino! I have indeed found that MBQI is significant in this problem. For the smallest reproducing example I can find, MBQI needs to be enabled for Z3 to report The Boogie source for my smaller example is in a Boogie issue here. |
Add type-constraining antecedents for each argument of a function when generating the type axiom for that function. These seem to have been intentionally but incorrectly left out in the original implementation. This fixes the missing antecedent issue in #735 and dafny-lang/dafny#4053 but does not yet fix the missing type constructor parameters. I have yet to track down exactly why those are left out.
The missing antecedents to function axioms are fixed in boogie-org/boogie#749. I thought that would fix this issue, since the smaller Boogie example I extracted from this that was giving unsound results is fixed by that PR. However, the example above is still verified by Dafny (when using Just to double-check the result we should expect, I translated the Dafny example above to SMT-Lib by hand (without any of the extraneous stuff Dafny includes), yielding the following.
I get |
I increasingly think the remaining unsoundness is a bug in Z3 which has since been fixed. I've taken the SMT-Lib output from this example and begun removing pieces of it such that it still results in
Removing any of those results in Z4 4.12.1 reporting Looking through the Z3 commit history, there do seem to be real arithmetic fixes that are in any release >= 4.12.2. At this point I think the right move to fix this issue is to update Dafny to use Z3 4.12.4 by default. It also includes some changes that are likely to improve performance, when enabled. |
With the latest Dafny (728433a as I write this), this issue no longer occurs. However, there is almost certainly a soundness bug in 4.12.1, as described above, which is no longer present in newer versions. In addition to that, though, there's also an open soundness bug in Z3 that also affects the NRA theory. My inclination is to leave this issue open until a Z3 release comes out that has resolved that issue and we've adopted that version. My reasoning is that, although the code snippet above doesn't trigger the issue, we know there is one in Z3, and therefore it may be possible to come to an unsound result through some other path. |
Dafny version
4.1.0
Code to produce this issue
Command to run and resulting output
What happened?
According to the previous discussion (#3869), using
/proverOpt:O:smt.arith.solver=6
performs better than the default setting.However, in this case,
/proverOpt:O:smt.arith.solver=6
produces an unsound result.Removing the irrelevant code (like deleting
assert true
or transforming0.0 <= 0.0
totrue
) yields the correct result.What type of operating system are you experiencing the problem on?
Linux
The text was updated successfully, but these errors were encountered: