Skip to content

Support bitwuzla, cvc5, z3 as solver attribute values #4218

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 22 commits into from
Jul 15, 2025
Merged

Support bitwuzla, cvc5, z3 as solver attribute values #4218

merged 22 commits into from
Jul 15, 2025

Conversation

@tautschnig
Copy link
Member

@tautschnig tautschnig commented Jul 11, 2025 •
edited
Loading

Adds support for solver attribute values bitwuzla, cvc5, and z3 to make CBMC use the corresponding SMT solver.

Use Z3 for selected tests when running regression tests with the following rationale: The tests loop_assigns_for_vec.rs and assert-postconditions.rs previously required more than 8 GB of memory on Ubuntu/x86 and solved in 1:15 minutes and 25 seconds, respectively. When using Z3 as back-end solver, they complete in 35 and 2 seconds (2.5 GB and 150 MB), respectively.

Use CVC5 for the test from issue #4226.

We are not testing Bitwuzla support in CI at this point (though it has been confirmed to work locally), because Bitwuzla only releases binaries for some of our CI platforms, and we cannot even build Bitwuzla from source on Ubuntu 22.04 (meson is too old).

Resolves: #3277
Resolves: #4226

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

@tautschnig
Install and use Z3 for memory-intensive regression tests
c5d4f2f 
The tests loop_assigns_for_vec.rs and assert-postconditions.rs
previously required more than 8 GB of memory on Ubuntu/x86 and solved in
1:15 minutes and 25 seconds, respectively. When using Z3 as back-end
solver, they complete in 35 and 2 seconds (2.5 GB and 150 MB),
respectively.
@tautschnig tautschnig self-assigned this Jul 11, 2025
@tautschnig
Copy link
Member Author

tautschnig commented Jul 14, 2025 •
edited
Loading

I'm inclined to mark this ready-for-review given the recurring problem of (spurious) CI failures as seen in, e.g, #4202. What I'd really like to do, however, is making Z3, CVC5, Bitwuzla first-class solvers in Kani just like, e.g., Kissat is. Unless someone beats me to it I'll try to take care of this tomorrow. Edit: done.

@tautschnig tautschnig changed the title Install and use Z3 for memory-intensive regression tests Support bitwuzla, cvc5, z3 as solver attribute values Jul 15, 2025
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jul 15, 2025
@tautschnig tautschnig marked this pull request as ready for review July 15, 2025 11:23
@tautschnig tautschnig requested a review from a team as a code owner July 15, 2025 11:23
@tautschnig tautschnig mentioned this pull request Jul 15, 2025
Closed
carolynzech
carolynzech approved these changes Jul 15, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Can you add a Bitwuzla test as a sanity check? It doesn't need to be an improvement over the default in any way, just something to demonstrate that someone could actually specify this attribute and it would work.

@tautschnig
Copy link
Member Author

Thanks! Can you add a Bitwuzla test as a sanity check? It doesn't need to be an improvement over the default in any way, just something to demonstrate that someone could actually specify this attribute and it would work.

Will do, but it will require us building from source on macos-13 runners as https://github.com/bitwuzla/bitwuzla/releases does not include binaries for macOS-x86_64.

@tautschnig tautschnig self-assigned this Jul 15, 2025
@tautschnig
Revert "fix os"
262025e 
This reverts commit 6909008.
@tautschnig
Revert "DEBUG"
655c435 
This reverts commit 93da97e.
@tautschnig
Revert "Test Bitwuzla"
af31cfe 
This reverts commit ee3378f.
@tautschnig
Copy link
Member Author

Thanks! Can you add a Bitwuzla test as a sanity check? It doesn't need to be an improvement over the default in any way, just something to demonstrate that someone could actually specify this attribute and it would work.

Will do, but it will require us building from source on macos-13 runners as https://github.com/bitwuzla/bitwuzla/releases does not include binaries for macOS-x86_64.

So I tried, but I am now backtracking on this, see also the (updated) note in the PR description: we cannot build Bitwuzla from source on Ubuntu 22.04, and I don't think this is worth any extra gymnastics.

@tautschnig tautschnig enabled auto-merge July 15, 2025 18:45
@tautschnig tautschnig added this pull request to the merge queue Jul 15, 2025
Merged via the queue into model-checking:main with commit ab7c438 Jul 15, 2025
26 of 27 checks passed
@tautschnig tautschnig deleted the use-z3 branch July 15, 2025 20:15
@zhassan-aws
Copy link
Contributor

Can the new attribute values be used in Kani releases?

@tautschnig
Copy link
Member Author

Can the new attribute values be used in Kani releases?

Unlike Kissat, users will still need to install those solvers themselves. I pondered including the solvers in the release bundle, but then decided to defer questions about licensing and the size of the release bundle. So we could certainly change that, but I think some additional care is required.

@zhassan-aws
Copy link
Contributor

I see. In this case, I would prefer if we invoke those solvers using --cbmc-args --z3 in the added regression tests instead of via the solver attribute. IMO, it would be undesirable to provide options that don't work out of the box (not a good UX).

@rajath-mk rajath-mk mentioned this pull request Aug 6, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Aug 7, 2025
@rajath-mk @zhassan-aws
bump kani vesion 0.65.0 (#4274)
677c791 
from the autogenerated : 

## What's Changed
* Ensure that contract closures are FnOnce by @vonaka in
#4151
* Adjust sized hierarchy for Kani's memory predicates by @tautschnig in
#4193
* Update to Rust edition 2024 by @tautschnig in
#4197
* `ptr_offset_from`: Replace arithmetic over pointers by offset
arithmetic by @tautschnig in
#4180
* Automatic cargo update to 2025-07-07 by @github-actions[bot] in
#4208
* Bump tests/perf/s2n-quic from `b8f8cca` to `8715fdf` by
@dependabot[bot] in #4209
* Upgrade Rust toolchain to 2025-07-04 by @tautschnig in
#4199
* Upgrade Rust toolchain to 2025-07-10 by @thanhnguyen-aws in
#4215
* Update CBMC dependency to 6.7.1 by @tautschnig in
#4178
* Split compiler flags to avoid dependency recompilation by
@AlexanderPortland in #4211
* Fix the bug that assign clause cannot be inferred for the inner loop
of nested loops by @thanhnguyen-aws in
#4179
* Upgrade Rust toolchain to 2025-07-11 by @thanhnguyen-aws in
#4219
* Automatic toolchain upgrade to nightly-2025-07-12 by
@github-actions[bot] in #4222
* Fix bug: `goto-cc` crash when there are two quantifers in one proof by
@thanhnguyen-aws in #4221
* Automatic toolchain upgrade to nightly-2025-07-13 by
@github-actions[bot] in #4223
* Automatic cargo update to 2025-07-14 by @github-actions[bot] in
#4224
* Cleanup links to issues that have been addressed by @tautschnig in
#4200
* Selectively enable and fix (slow) Tokio tests by @tautschnig in
#4203
* Bump tests/perf/s2n-quic from `32ba87d` to `1cbd879` by
@dependabot[bot] in #4227
* Implement support for Cargo.toml's default-members by @tautschnig in
#4201
* Do not invoke memset with count of zero by @tautschnig in
#4205
* Support bitwuzla, cvc5, z3 as solver attribute values by @tautschnig
in #4218
* Use CBMC's shuffle_vector expression by @tautschnig in
#4204
* Move tests from slow/kani back to regular suite by @tautschnig in
#4202
* Automatic toolchain upgrade to nightly-2025-07-14 by
@github-actions[bot] in #4225
* Enable GitHub Linux/Arm runners in CI by @tautschnig in
#3841
* Automatic cargo update to 2025-07-21 by @github-actions[bot] in
#4231
* Skip codegen for unneeded harnesses by @AlexanderPortland in
#4213
* Strongly type differing compiler args for clarity by
@AlexanderPortland in #4220
* Remove StableMIR ICE workaround by @carolynzech in
#4235
* Fix bug: Kani unwinds loops with contract in generic function (with -Z
loop-contracts) by @thanhnguyen-aws in
#4232
* Automatic cargo update to 2025-07-28 by @github-actions[bot] in
#4238
* Bump tests/perf/s2n-quic from `1cbd879` to `4938450` by
@dependabot[bot] in #4242
* Upgrade Rust toolchain to 2025-07-21 by @tautschnig in
#4241
* Remove `pretty_ty` and use rustc_public's formatter instead by
@tautschnig in #4243
* Upgrade Rust toolchain to 2025-07-24 by @tautschnig in
#4244
* Documentation cleanup of UB detected by Kani by @tautschnig in
#4245
* Upgrade Rust toolchain to 2025-07-29 by @tautschnig in
#4247
* Automatic toolchain upgrade to nightly-2025-07-30 by
@github-actions[bot] in #4253
* Add unstable option prove-safety-only by @tautschnig in
#4239
* Set bits_per_byte in byte_extract expressions by @tautschnig in
#4255
* `KaniAttributes` Path Resolution Refactor by @carolynzech in
#4249
* Automatic toolchain upgrade to nightly-2025-07-31 by
@github-actions[bot] in #4256
* Support contracts & stubs in trait implementations (partial fix) by
@carolynzech in #4250
* [Breaking Changes] Remove unstable list feature and default memory
checks by @carolynzech in
#4258
* Upgrade Rust toolchain to 2025-08-01 by @tautschnig in
#4261
* Autoharness: add support for references by @tautschnig in
#4234
* Turn off debug assertions under `--prove-safety-only` by @tautschnig
in #4262
* Automatic toolchain upgrade to nightly-2025-08-02 by
@github-actions[bot] in #4264
* Automatic toolchain upgrade to nightly-2025-08-03 by
@github-actions[bot] in #4265
* Automatic cargo update to 2025-08-04 by @github-actions[bot] in
#4267
* Automatic toolchain upgrade to nightly-2025-08-04 by
@github-actions[bot] in #4266
* Introduce thread pool for writing goto binaries in parallel by
@AlexanderPortland in #4236
* Major-version update cargo dependencies by @tautschnig in
#4240
* Bump tests/perf/s2n-quic from `4938450` to `8f510f0` by
@dependabot[bot] in #4270
* Automatic toolchain upgrade to nightly-2025-08-05 by
@github-actions[bot] in #4271
* Automatic toolchain upgrade to nightly-2025-08-06 by
@github-actions[bot] in #4272
* Avoid updating irrelevant symbols when handling quantifiers by
@AlexanderPortland in #4268
* Lazily evaluate debug info by @AlexanderPortland in
#4269
* Clone a template `BodyTransformer` to avoid re-initialization by
@AlexanderPortland in #4259
* Ensuring that MIR constants are marked as static consts by @vonaka in
#4233
* Fix release job dependencies by @tautschnig in
#4273

## New Contributors
* @vonaka made their first contribution in
#4151

**Full Changelog**:
kani-0.64.0...kani-0.65.0

---------

Co-authored-by: Zyad Hassan <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@carolynzech carolynzech carolynzech approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@tautschnig tautschnig

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Incorrect verification results when using quantifiers with arbitrary range Add support to Z3

3 participants

@tautschnig @zhassan-aws @carolynzech