Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Test regression with Z3 4.8.10 #1107

Open
robdockins opened this issue Mar 15, 2021 · 4 comments
Open

Test regression with Z3 4.8.10 #1107

robdockins opened this issue Mar 15, 2021 · 4 comments
Labels
prover Issues related to :sat and :prove upstream Tracking bugs in external tools/libraries we depend on What4/SBV Cases where there is a significant performance difference between What4 and SBV

Comments

@robdockins
Copy link
Contributor

The tests/regression/negshift.icry test no longer completes in a reasonable amount of time with Z3 version 4.8.10, whereas the proof completes in about 3 seconds with Z3 4.8.9.
@robdockins robdockins added upstream Tracking bugs in external tools/libraries we depend on prover Issues related to :sat and :prove labels Mar 15, 2021
@robdockins
Copy link
Contributor Author

Also noteworthy, the What4 backends do much worse than the SBV backends on this problem.

@robdockins
Copy link
Contributor Author

CF Z3Prover/z3#5106

@robdockins robdockins added the What4/SBV Cases where there is a significant performance difference between What4 and SBV label Mar 23, 2021
@robdockins
Copy link
Contributor Author

Upstream bug is fixed via Z3Prover/z3@6aa766a

@robdockins
Copy link
Contributor Author

Z3 4.8.11 has fixed this regression.

@brianhuffman brianhuffman mentioned this issue Sep 3, 2021
Open
This was referenced Jan 14, 2022
Merged
Merged
Closed
RyanGlScott added a commit that referenced this issue Jan 14, 2022
@RyanGlScott
CI: Update what4-solvers to use Z3 4.8.14
3b9eafb 
The previous `what4-solvers` snapshot used Z3 4.8.10, which is known to cause
severe performance regressions with the `negshift` regression test. See #1107.
This updates to a more recent `what4-solvers` snapshot that uses Z3 4.8.14
instead, which is known to work more reliably with `negshift`.
@RyanGlScott RyanGlScott mentioned this issue Nov 21, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
prover Issues related to :sat and :prove upstream Tracking bugs in external tools/libraries we depend on What4/SBV Cases where there is a significant performance difference between What4 and SBV
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@robdockins