Skip to content

[SMT] Add "--incremental" flag to cvc5 to avoid crash#12

Closed
dobios wants to merge 3 commits intocucapra:mainfrom
dobios:main
Closed

[SMT] Add "--incremental" flag to cvc5 to avoid crash#12
dobios wants to merge 3 commits intocucapra:mainfrom
dobios:main

Conversation

@dobios
Copy link
Copy Markdown
Contributor

@dobios dobios commented Apr 7, 2026

I tried running the cvc5 backend and ran into:

Running `<file_name>.btor2 --solver cvc5`

thread 'main' (95116) panicked at tools/bmc/src/main.rs:89:6:
called `Result::unwrap()` on an `Err` value: FromSolver("cvc5", "\"Cannot make multiple queries unless incremental solving is enabled

It seems that cvc5 was the only backend that didn't have incremental solving enabled so I added that option to the solver and now it runs.

@ekiwi
Copy link
Copy Markdown
Collaborator

ekiwi commented Apr 8, 2026

Could you add a CVC5 test to CI so that we can catch this in the future?

  1. add an setup-cvc5 similar to our setup-yices action here
  2. add cvc5 to this step in our ci:

@dobios
Copy link
Copy Markdown
Contributor Author

dobios commented Apr 8, 2026

If you want to merge this, i have another PR to test the new CI (just to make it easier to debug)

@ekiwi
Copy link
Copy Markdown
Collaborator

ekiwi commented Apr 8, 2026

I think this change was also included in your other PR. If I am wrong, feel free to re-open.

@ekiwi ekiwi closed this Apr 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants