z3.rs

The z3.rs project is split into three main crates depending on your needs:

• z3: The high-level, idiomatic Rust bindings. This is the recommended crate for almost all users (99% of use cases).
• z3-sys: Low-level, unsafe FFI bindings that expose the raw C API of the Z3 solver. Use this only if you need a Z3 feature not yet wrapped by the z3 crate, or if you are building your own high-level API.
• z3-src: Contains the Z3 source distribution and the logic required to handle vendored builds.

The compatibility between the Rust crates and the upstream Z3 solver depends on the version of the crates you are using.

For z3 ≥ 0.20.0 (and z3-sys ≥ 0.11.0)

• Minimum Upstream Z3: 4.8.17 is required. This is due to API requirements (e.g., Regexp methods) and DeclKind enum correctness.
• Special Feature: Optimize::translate and Optimize::clone require upstream Z3 ≥ 4.16.0. These are gated behind the z3_4_16 feature flag.

For z3 ≤ 0.19.x (and z3-sys ≤ 0.10.x)

• Upstream Z3: Supports versions ≥ 4.8.12.

The version of the z3-src crate encodes the specific Z3 release it bundles using the following format:

{Z3_major}{Z3_minor:02}.{Z3_patch}.{packaging_revision}

For example, version 416.0.0 bundles Z3 release 4.16.0.

By default, the crate looks for Z3 in your system paths. If you are using Homebrew on macOS and the headers are not found, you must set the Z3_SYS_Z3_HEADER environment variable. You may also need to set Z3_LIBRARY_PATH_OVERRIDE for the linker.

To make these settings permanent for your project, add them to .cargo/config.toml.

# Via environment variables
Z3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h cargo build

# Or via .cargo/config.toml
[env]
Z3_LIBRARY_PATH_OVERRIDE = "/opt/homebrew/lib"
Z3_SYS_Z3_HEADER = "/opt/homebrew/include/z3.h"

Enabling the vendored feature uses cmake to build Z3 locally.

If you want to use your own Z3 source tree instead of the one provided by z3-src, set the Z3_SRC_SOURCE_DIR environment variable to the absolute path of your Z3 source.

Note: A z3 directory within your project or workspace is not automatically detected; you must point to it explicitly.

To use a path relative to your project root, use the relative = true key in .cargo/config.toml.

# Using an absolute path
Z3_SRC_SOURCE_DIR=/absolute/path/to/z3 cargo build

# Using a relative path in .cargo/config.toml
[env]
Z3_SRC_SOURCE_DIR = { value = "path/to/z3", relative = true }

If you are maintaining your own Z3 FFI bindings and want to compile Z3 from source instead of linking against a system-installed copy, add z3-src as a build-dependency in your Cargo.toml.

In your build.rs, call z3_src::build() to compile the source. The returned artifacts object provides access to the include directory and library directory, and includes a helper method print_cargo_metadata() which emits the necessary cargo:rustc-link-search and cargo:rustc-link-lib directives for Cargo to link the static library correctly.

// Cargo.toml
[build-dependencies]
z3-src = "416"

// build.rs
fn main() {
    let artifacts = z3_src::build();
    artifacts.print_cargo_metadata();
    // artifacts.include_dir() — path containing z3.h
    // artifacts.lib_dir()     — path containing the static library
}

The z3 crate provides high-level Rust bindings to the Z3 SMT solver. You can add it to your project using Cargo.

$ cargo add z3

To successfully build z3-src, ensure the following are available on your system:

1. CMake: Must be available on your PATH during the build process.
2. C++ compiler: A compiler supported by Z3's CMake build system (e.g., GCC, Clang, or MSVC).

Note on build time: Compilation is resource-intensive and typically takes approximately 5 minutes on modern hardware. Incremental rebuilds are cached by Cargo in the OUT_DIR directory.

Add z3-sys to your Rust project using Cargo. This crate provides low-level Rust bindings to the Z3 SMT solver.

$ cargo add z3-sys

If you are using z3 version 0.20 or higher and require Optimize::translate or Optimize::clone, you must ensure your upstream Z3 version is at least 4.16.0 and enable the z3_4_16 feature flag in your Cargo.toml.

[dependencies]
z3 = { version = "0.20", features = ["z3_4_16"] }

The z3 crate requires the Z3 library to be present on your system. You can control how the crate finds Z3 using specific feature flags in your Cargo.toml:

• Default (No flags): Searches for a system-installed copy of Z3 (e.g., via apt, brew, etc.).
• vendored: Builds and statically links Z3 from source using cmake. The source is provided by the z3-src crate. (Note: bundled is a deprecated alias for vendored).
• vcpkg: Uses a copy of Z3 installed via the vcpkg package manager.
• gh-release: Downloads a pre-compiled copy of Z3 from GitHub releases for your platform.

# Example using gh-release
[dependencies]
z3 = {version="0", features = ["gh-release"]}

# Example using vcpkg
[dependencies]
z3 = {version="0", features = ["vcpkg"]}