z3.rs and the Rust bindings for the Z3 theorem prover

Three crates, one workspace

The repository contains high-level and low-level Rust bindings for the Z3 solver, and it is organised as a Cargo workspace with four members:

[workspace]
members = ["z3", "z3-sys", "z3-src", "xtask"]
resolver = "3"

The z3 crate provides the high-level bindings and is built on top of, and wraps, the z3-sys crate. The documentation is blunt about which one you want: this is the crate you'll want to use 99% of the time.

The z3-sys crate provides the raw, unsafe, low-level C API that Z3 exposes. It is the FFI layer, and it is where the awkward parts of binding a C++ solver live.

The z3-src crate contains the Z3 source distribution and the logic to handle vendored builds. That is a distinctive thing for a binding repository to carry: rather than assuming a system Z3 is installed, this workspace can compile the solver itself as part of your build, which turns a runtime prerequisite into a build step.

The fourth member, xtask, is the conventional Cargo pattern for build and release automation that has to run before the normal build.

The topic list names the shape of the project precisely: ffi-bindings, rust, rust-bindings, smt, smt-solver and logic-programming. The recent releases are released as a set, with z3-v0.21.1, z3-sys-v0.13.1 and z3-src-v501.0.1 all dated 2026-09-23, which is the correct pattern for a workspace where the three crates have to move in step.

The primary language is Rust, the default branch is master, the last push was on 2026-09-23, and the repository is not archived.

Version compatibility, and why it is genuinely awkward

The compatibility section of the readme is the most substantive part of the documentation, and it explains a problem that is specific to binding a fast-moving C++ API.

Starting with version 0.21.0, the z3 and z3-sys crates have a minimum supported Z3 version of 4.13.3. The readme then gives the two reasons for Z3 incompatibility.

The first is that Z3 sometimes adds APIs, which makes new C FFI targets, and causes linker errors if you naively attempt to link against a too-new symbol in an old Z3 version. The second is that Z3 sometimes shuffles existing enum values while adding new ones.

Those two causes have different consequences, and the readme is careful to separate them. The first issue means that using some z3 features imposes a minimum supported version. The second means that z3-sys has a separate range of compatibility based on enum changes, independent of what high-level Z3 versions are used.

That second point is the one that should shape your build decisions. A missing symbol is a loud failure at link time. A changed enum value is quiet: your code compiles, it links, and the solver returns an answer derived from the wrong meaning of a constant.

The current mitigation is automation. Starting with version 0.21.0, the crate attempts to auto-detect the linked Z3 version and automatically enables all compatible features, without requiring user-enabled features. If that version detection fails, it assumes the minimum supported version of 4.13.3 and warns.

The warning is what a mismatch looks like, and it is worth reading rather than scrolling past:

$ Z3_SYS_Z3_VERSION=4.16.0 cargo test --features gh-release
   Compiling z3-sys v0.13.0 (/repos/z3.rs/z3-sys)
warning: [email protected]: z3-sys: attempting to link against Z3 4.16.0 with `z3-sys` bindings for Z3 >= 5.0.0; enum numbering (e.g. Z3_decl_kind) may differ across these versions. Consider updating Z3 or else enabling the `bindgen` feature to ensure compatibility.

The tip attached to it says the crate will display a warning if you attempt to link against an incompatible Z3 version, and to use --features bindgen or update Z3 to fix this.

When to drop to the unsafe layer

The readme has a section on when z3-sys should be used instead of z3, and the answer is short and specific.

The first scenario where it makes sense to use z3-sys directly is when some Z3 feature is not wrapped into high-level bindings in the z3 crate yet. In that case the advice is to file an issue and discuss the implementation in the z3 crate, and in the meantime you can get at the raw underlying features through z3-sys.

The only other time to use z3-sys directly would be if you are writing your own custom high-level API for Z3, instead of using the z3 crate.

So there are exactly two reasons, and both of them are about the high-level layer being incomplete rather than about the low-level layer being better. That is the shape you want from a binding: the ergonomic crate is the default, and the raw crate is an escape hatch with a stated reason.

The bindgen feature is the other lever worth understanding, and it appears in the compatibility advice rather than in a feature list. It generates the bindings against the Z3 headers present on your machine instead of using the pre-generated ones, which is the answer when the enum numbering of your Z3 does not match what the crate expects.

That distinction, between generated-at-build-time bindings and pre-generated ones, is the crux of the whole compatibility story. Pre-generated bindings are fast and reproducible but assume a Z3 version. Bindings generated against your headers are always right but require the headers and a working bindgen at build time. The crate ships the pre-generated path as the default and offers bindgen for the cases where the assumption does not hold.

The gh-release feature, which appears in the example command, is a separate axis: it is about where the Z3 binaries come from rather than how the bindings are produced.

What the workspace contains, and what adopting it costs

The repository layout is small and reveals how the pieces fit together. There are the three crate directories, z3/, z3-sys/ and z3-src/, an xtask/ directory for the build automation, a .cargo/ directory for cargo configuration, a .gitmodules file, a release-plz.toml for release automation, and the workspace Cargo.toml.

The z3-src crate is the unusual one, and it is worth thinking about what it buys. A binding crate for a C++ library normally has a simple requirement: a system library must be installed. That is a fine assumption on a developer machine and a poor one in a container build or a CI pipeline, where the library has to be present at the right version before anything compiles.

By carrying the Z3 source distribution and the logic for vendored builds, this workspace can compile the solver as part of your build. That makes the build self-contained and reproducible, at the cost of a longer compile, because you are building a solver rather than linking a prebuilt one.

The version numbers tell you how the three crates relate. The high-level crate is at 0.21.1, the sys crate at 0.13.1, and the src crate at 501.0.1, where the major number tracks the upstream Z3 release the source corresponds to. So the source crate versions independently of the binding crates, which is the correct arrangement when the upstream project has its own release cadence.

The cost of adoption is therefore a build decision rather than an API decision. If your environment already has a Z3 of a known version, you can link against it and take the fast path. If it does not, the vendored path makes the question go away, at the price of a slower build.

The licence situation is less clear from what is available here. The repository licence field is not stated in the project metadata, and the readme does not summarise the terms, so the LICENSE file at the repository root is the place to look before you redistribute anything, and the upstream Z3 licence applies to the solver source carried in z3-src.

Editorial conclusion

z3.rs is a good fit for a Rust project that needs to discharge constraints, verify a property or generate a counterexample, because the high-level crate covers the common cases and keeps the FFI in a layer you do not have to touch. It is a poor fit if your build environment has no C toolchain, since the solver is a C library and the vendored path compiles it from source, and a poor fit if you need a Z3 feature the high-level crate has not wrapped yet, since that means dropping to the unsafe API. Before adopting, pin the Z3 version your build links against and let the crate detect it, because the failure mode is a linker error or, worse, silently different enum values rather than a compile error.

Frequently asked questions

Official sources

1. Issues
2. prove-rs/z3.rs on GitHub
3. README
4. Releases