Skip to content

Conversation

@zhassan-aws
Copy link
Contributor

Description of changes:

Update nightly CBMC latest workflow to build CBMC with cadical. Without this, regressions that run cadical (e.g. https://github.com/model-checking/kani/blob/035225ca362b0a80c807af0f567c3513237cb0ee/tests/ui/solver-attribute/cadical/test.rs) fail.

Resolved issues:

Fixes nightly CBMC latest regressions.

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

I couldn't get this to work through just adding -Dsat_impl="minisat2;cadical to this line:

cmake -S . -Bbuild -DWITH_JBMC=OFF

because the cadical configure step failed on macos-11. This needs investigation.

Testing:

  • How is this change tested? Regressions passed in my fork.

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@zhassan-aws zhassan-aws requested a review from a team as a code owner March 6, 2023 07:07
@adpaco-aws adpaco-aws assigned karkhaz and unassigned karkhaz Mar 6, 2023
@zhassan-aws zhassan-aws merged commit 1a52d34 into model-checking:main Mar 7, 2023
@zhassan-aws zhassan-aws deleted the cadical-nightly branch March 7, 2023 00:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

No open projects
Status: No status

Development

Successfully merging this pull request may close these issues.

3 participants