Skip to content

Change default SMT solver from z3 to cvc5 #401

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
Merged
MikaelMayer merged 16 commits into from
Feb 12, 2026
Merged

Change default SMT solver from z3 to cvc5 #401

MikaelMayer merged 16 commits into from
Feb 12, 2026

Conversation

@MikaelMayer
Copy link
Contributor

@MikaelMayer MikaelMayer commented Feb 9, 2026 •
edited
Loading

Change default SMT solver from z3 to cvc5

This PR updates the default SMT solver throughout the codebase from z3 to cvc5. The changes include:

  • Updated defaultSolver in Strata/Languages/Core/Options.lean
  • Updated default solver parameter in Strata/Languages/B3/Verifier/State.lean
  • Updated solver references in StrataMain.lean for Laurel analysis
  • Updated all test files to use cvc5 instead of z3

Files that check for both z3 and cvc5 (like Strata/DL/Imperative/SMTUtils.lean and Strata/Languages/Core/Verifier.lean) were left unchanged as they handle both solvers.

@MikaelMayer
Change default SMT solver from z3 to cvc5
b5e4e74
@MikaelMayer
Update RemoveIrrelevantAxioms test expectations for cvc5
492f40a
@MikaelMayer
Revert "Update RemoveIrrelevantAxioms test expectations for cvc5"
12c1720 
This reverts commit 492f40a.
@MikaelMayer
Update RemoveIrrelevantAxioms test: cvc5 produces different (but vali…
78b1558 
…d) counterexample models than z3
@MikaelMayer
Make RemoveIrrelevantAxioms test solver-agnostic by normalizing model…
a109877 
… values
@MikaelMayer
Update Quantifiers test: cvc5 cannot prove assert_2 (quantifier insta…
afeb5ba 
…ntiation difference)
@MikaelMayer
Update Quantifiers test: assert_3 is provable by both z3 and cvc5
155101f
@MikaelMayer
Update Quantifiers test: assert_5 is provable by cvc5
476a83b
@MikaelMayer
Update Quantifiers test: assert_6 is provable by cvc5
f0fb76e
@MikaelMayer
Fix Quantifiers test summary: 12 passed, 2 failed
ee6bb78
@MikaelMayer MikaelMayer marked this pull request as ready for review February 11, 2026 17:24
@MikaelMayer MikaelMayer requested a review from a team as a code owner February 11, 2026 17:24
shigoel
shigoel reviewed Feb 11, 2026
View reviewed changes
Copy link
Contributor

@shigoel shigoel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, except for one comment.

shigoel
shigoel reviewed Feb 12, 2026
View reviewed changes
MikaelMayer
MikaelMayer commented Feb 12, 2026
View reviewed changes
atomb
atomb approved these changes Feb 12, 2026
View reviewed changes
@MikaelMayer MikaelMayer added this pull request to the merge queue Feb 12, 2026
Merged via the queue into main with commit 4d832fc Feb 12, 2026
15 checks passed
@MikaelMayer MikaelMayer deleted the change-default-verifier-to-cvc5 branch February 12, 2026 19:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@atomb atomb atomb approved these changes

@shigoel shigoel shigoel approved these changes

@aqjune-aws aqjune-aws aqjune-aws approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@MikaelMayer @atomb @shigoel @aqjune-aws