-
Notifications
You must be signed in to change notification settings - Fork 41
Warn on missing SMT solvers if flag is set #3600
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
Conversation
|
Fails as cvc4 is not available on Github Actions. @WolframPfeifer |
|
Migration to cvc5 as far as possible. |
|
Agreed at meeting: Retire CVC4 support. Migrate test cases to CVC5 is possible, drop otherwise. |
|
wait for #3592 |
|
#3592 is merged into main, I updated this PR. Also, I migrated the CVC4 test case to cvc5, so this PR should be merge-ready now. |
|
We need an additional reviewer, since @wadoon and I both have committed to this PR ... |
Currently, if SMT solvers are not available during testing, these test cases will be silently ignored---a behavior acceptable on local machines, but not on CI.
On CI, this is firstly ensured by executing
z3andcvc5on command-line. This ensures installation, but not that KeY finds the executable.This PR changes the behavior of SMT test cases to failing if SMT solvers are not present, and an additional flag is set.
This flag is set iff the environment variables sets
failIfSmtSolverIsUnavailableorGITHUB_ACTIONStotrue.Type of pull request
Ensuring quality