-
Notifications
You must be signed in to change notification settings - Fork 42
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.
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
Enable using cvc5
SMT solver in Kore
#3905
Comments
@goodlyrottenapple experiment reveals that there are roadblocks in integrating CVC5 into Kore:
More context could be found in this Slack thread. @goodlyrottenapple please add any other information you think is relevant. |
The investigation also revealed that the way we encode data-types is similarly incompatible with CVC5; we are currently using |
We have evidence (see Slack thread) that CVC5 is more successful than Z3 in dealing with some non-linear arithmetic problems arising in rules' side condition in
kasmer
andkontrol
.We have for a long time considered adding CVC5 as an alternative/companion solver to Z3.
We should start with the simplest possible implementation: use CVC5 instead of Z3, controlled by the
--smt-solver
command line option.The text was updated successfully, but these errors were encountered: