Investigate best setting for Z3 parameter smt.qi.eager_threshold
#3558
Labels
area: performance
Performance issues
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: z3
Issue is in Z3
Comments
atomb
added
the
kind: enhancement
|
Can we start with documenting how the parameter theoretically affects Dafny's verification? |
atomb
added a commit
that referenced
this issue
Feb 28, 2023
The updates the default version of Z3 to 4.12.1 and updates superficial aspects of the tests (error order, counterexample values, occasional command-line option tweaks) to work with it. Those test changes have some minor caveats: * Some of the tests in `DafnyTestGeneration.Test` check very specific things about the solver results that I don't think are required of valid results. I've commented out what I think are the overly-restrictive checks, but they should really be replaced with similar but less restrictive ones. @Dargones, do you have any thoughts? * Some tests require specific settings of the Z3 parameter `smt.qi.eager_threshold` to succeed, but there isn't a single value that allows them all to succeed. There's even one test I had to split into two files to give two values of this parameter. Let's investigate whether the current value is a good one, in general. Tracked as #3558. * Dafny is now able to prove an assertion in `Fuel.dfy` that it shouldn't be able to, according to comments in the file. I don't think this is technically either a soundness or incompleteness issue, but it's a strange behavior. Edit: it turns out that the latest nightly of Z3 goes back to being unable to prove that assertion. * One test (`github-issues/github-issue-2174.dfy`) requires a special setting of the arithmetic solver. This is something we should investigate further on other code bases. Issue #3501 tracks that investigation. * The `BitvectorsMore` test was missing errors since there were too many in one method. It had `/errorLimit:10`, but that wasn't even high enough. A newer solver version resulted in the order of errors changing, causing known errors to be hidden and previously untracked errors to be revealed. A higher error limit solves this. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Summary
A different setting of the Z3 parameter
smt.qi.eager_thresholdmay perform better, on average, than the current one.Background and Motivation
Dafny has set the Z3 parameter
smt.qi.eager_thresholdto 100 for its entire GitHub history, but has a comment saying "TODO: try lowering". Several tests have required lower values to go through. With the upgrade to Z3 4.12.1, more tests require custom settings for this parameter, though there doesn't seem to be a single value that works well for all of them.Proposed Feature
Is there a value that would be generally better than 100, even if not for these few tricky tests? Let's do some experiments to find out. And, if there is a better value, let's use that instead.
Alternatives
No response
The text was updated successfully, but these errors were encountered: