SMT back-end: add support for Bitwuzla and CVC 5 #7519
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds support for two actively developed SMT solvers, with the caveat that these do not currently pass all regression tests (Bitwuzla fails two tests, CVC 5 times out on one and fails on nine others). Some performance data running (in
regression/cbmc
, for varying values of<SOLVER>
):Note that the following data has bias: it only has the subset of tests that all back-ends are expected to be able to solve. That is, some SMT solver may be faster on this minimum common set of tests, but might be unable to solve tests that another (possibly slower) solver can handle.
--bitwuzla
for<SOLVER>
):--cvc5
for<SOLVER>
):--z3
for<SOLVER>
):--cprover-smt2
for<SOLVER>
):<SOLVER>
):