Parity in Counterexample-Related Z3 Options for Command-Line vs Language Server #4792
Conversation
| @@ -84,25 +84,6 @@ internal enum Status { Success, Failure, Untested } | |||
| /// Setup DafnyOptions to prepare for counterexample extraction | |||
| /// </summary> | |||
| private static void SetupForCounterexamples(DafnyOptions options) { | |||
| // Figure out the Z3 version in use: | |||
There was a problem hiding this comment.
Nice that this isn't necessary anymore!
|
Noting as we discussed earlier: let's not merge this until after 4.4 since it changes verification behavior. |
|
The PR is now ready to be merged. Note that it does update the Boogie version and Z3 options used for verification. |
|
@atomb, it appears that this PR might affect the way some assertion violations are reported by Dafny. In particular, I had to update this test's expected output. Does that appear to be a desirable change in behavior? This is the only test so affected. As far as I understand, the new changes cause an additional {:captureState} assumption to be inserted in the beginning of the method -- hence the change in expected output. I am not quite sure why the difference shows up for this particular test but nowhere else. For what it is worth, when I attempt verifying this test in the VS Code, the IDE reports an error at the same location where the command line will report it once this PR is merged. So the PR definitely improves parity between the two. |
| @@ -1146,6 +1147,13 @@ public enum IncludesModes { | |||
| SetZ3Option("type_check", "true"); | |||
| SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering | |||
| SetZ3Option("smt.delay_units", "true"); | |||
| SetZ3Option("model_evaluator.completion", "true"); | |||
There was a problem hiding this comment.
Do these Z3 options not significantly change verification behavior?
There was a problem hiding this comment.
They are on by default in the Language Server already, so I don't think they should.
There was a problem hiding this comment.
What does it matter whether they're on in the language server? They may still cause different verification behavior on the CLI.
There was a problem hiding this comment.
These options are meant to only affect the way Z3 processes its counterexample model, so the result of verification will stay the same. I believe @atomb looked into variability data as well, so there are no unexpected performance-related problems. The fact that these options have been used by the Language Server for over two years just means that there are no bugs (that we know of) associated with these options.
Description
The language server supports counterexample extraction by default but command line Dafny does not, which leads to a mismatch in Z3 options. This PR ensures parity between counterexample-related options and updates counterexample extraction command line interface so that it works out of the box without requiring additional options.
How has this been tested?
There are existing tests for counterexamples that this PR should pass.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.