z3prover/z3High-performance SMT solver for automated theorem proving, constraint solving, and program verification. Supports multiple theories and language bindings for formal analysis.
# Z3 Z3 is a theorem prover from Microsoft Research. It is licensed under the [MIT license](https://github.com/z3prover/z3/blob/master/LICENSE.txt). Windows binary distributions include [C++ runtime redistributables](https://visualstudio.microsoft.com/license-terms/vs2022-cruntime/) If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background). Pre-built binaries for stable and nightly releases are available [here](https://github.com/Z3Prover/z3/releases). Z3 can be built using [CMake][3], [vcpkg][4], or [Bazel][5]. It provides [bindings for several programming languages][6]. See the [release notes](https://github.com/z3prover/z3/blob/master/RELEASE_NOTES.md) for notes on various stable releases of Z3. [](https://microsoft.github.io/z3guide/) ## Build status ### Pull Request & Push Workflows | WASM Build | Windows Build | CI | Finite-Field Regressions | | ------------|---------------|----------------------|-------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/ci.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/finite-field.yml) | | Determinism Linter | Solver Determinism | Pulse Native Checker Build | |---------------------|---------------------|----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/ast-order-warning-report.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/determinism.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pulse-checker-build.yml) | ### Scheduled Workflows | Android Build | Nightly Build | Cross Build | F* Master Build | | ---------------|---------------|-------------|------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nightly.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/cross-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-master-build.yml) | | MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready | |-------------|---------------|----------------|---------------|----------------| | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/msvc-static-build-clang-cl.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/build-z3-cache.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/mark-prs-ready-for-review.yml) | | Clang-Tidy Warning Report | |----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/clang-tidy-warning-report.yml) | ### Manual & Release Workflows | Documentation | Release Build | WASM Release | Pyodide Wheel (PyPI) | |---------------|---------------|--------------|---------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/docs.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/wasm-release.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pyodide-pypi.yml) | ### Specialized Workflows | Nightly Validation | Copilot Setup | Agentics Maintenance | Dispatch NFV Formal Audit | |--------------------|---------------|----------------------|----------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/nightly-validation.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/copilot-setup-steps.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/agentics-maintenance.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/nfv-formal-audit-dispatcher.yml) | ### Follow-up / Comment Workflows | Determinism Linter PR Comment | Solver Determinism PR Comment | Pulse Checker Regressions | |--------------------------------|---------------------------------|--------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/ast-order-warning-comment.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/determinism-comment.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pulse-checker-regressions.yml) | ### Agentic Workflows | API Coherence | Code Simplifier | Release Notes | Workflow Suggestion | Academic Citation | | -------------|-----------------|---------------|---------------------|-------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/api-coherence-checker.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-simplifier.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/release-notes-updater.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/workflow-suggestion-agent.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/academic-citation-tracker.lock.yml) | | Issue Backlog | Memory Safety Report | SMTLIB Benchmark Finder | F* NFV PR Audit | | --------------|----------------------|-------------------------|-----------------| | [](https://github.com/Z3Prover/z3/actions/workflows/issue-backlog-processor.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/memory-safety-report.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/smtlib-benchmark-finder.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/fstar-nfv-audit.lock.yml) | | A3 Python Analysis | Code Conventions | Compare Stats Anomaly Reporter | CSA Analysis | Tactic-to-Simplifier | |----------------------|-------------------|----------------------------------|----------------|------------------------| | [](https://github.com/Z3Prover/z3/actions/workflows/a3-python.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/code-conventions-analyzer.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/compare-stats-anomaly-reporter.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/csa-analysis.lock.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/tactic-to-simplifier.lock.yml) | [3]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-cmake [4]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-vcpkg [5]: https://raw.githubusercontent.com/z3prover/z3/master/#building-z3-using-bazel [6]: https://raw.githubusercontent.com/z3prover/z3/master/#z3-bindings ## Building Z3 using CMake CMake is the preferred and most fully featured build system for Z3. A basic release build is: ```bash cmake -S . -B build -DCMAKE_BUILD_TYPE=Release cmake --build build --parallel $(nproc) ``` See [README-CMake.md](https://github.com/z3prover/z3/blob/master/README-CMake.md) for build options, language bindings, installation, and instructions for consuming Z3 from another CMake project. Z3 uses C++20. On Windows, the recommended version of Visual Studio is therefore VS2019 or later; CMake with the Ninja or Visual Studio generator builds Z3 from the Visual Studio Command Prompt. **Security Features (MSVC)**: When building with Visual Studio/MSVC, a couple of security features are enabled by default for Z3: - Control Flow Guard (`/guard:cf`) - enabled by default to detect attempts to compromise your code by preventing calls to locations other than function entry points, making it more difficult for attackers to execute arbitrary code through control flow redirection - Address Space Layout Randomization (`/DYNAMICBASE`) - enabled by default for memory layout randomization, required by the `/GUARD:CF` linker option - These can be disabled using `cmake -S . -B build -DZ3_ENABLE_CFG=OFF` if needed Use `sudo cmake --install build` to install to the system prefix (or set `-DCMAKE_INSTALL_PREFIX=` at configure time for a custom prefix). To uninstall, consult your platform's package manager, or, since CMake tracks installed files in `build/install_manifest.txt`, remove those files directly. ## Building Z3 using vcpkg vcpkg is a full platform package manager. To install Z3 with vcpkg, execute: ```bash git clone https://github.com/microsoft/vcpkg.git ./bootstrap-vcpkg.bat # For powershell ./bootstrap-vcpkg.sh # For bash ./vcpkg install z3 ``` ## Building Z3 using Bazel Z3 can be built using [Bazel](https://bazel.build/). This is known to work on Ubuntu with Clang (but may work elsewhere with other compilers): ``` bazel build //... ``` ## Dependencies Z3 itself has only few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading. It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained multi-precision functionality. Python is required to build Z3. Building Java, .NET, OCaml and Julia APIs requires installing relevant toolchains. ## Z3 bindings Z3 has bindings for various programming languages. ### ``.NET`` You can install a NuGet package for the latest release Z3 from [nuget.org](https://www.nuget.org/packages/Microsoft.Z3/). With CMake, use the ``-DZ3_BUILD_DOTNET_BINDINGS=ON`` option. See [``examples/dotnet``](https://github.com/z3prover/z3/blob/master/examples/dotnet) for examples. ### ``C`` These are always enabled. See [``examples/c``](https://github.com/z3prover/z3/blob/master/examples/c) for examples. ### ``C++`` These are always enabled. See [``examples/c++``](https://github.com/z3prover/z3/blob/master/examples/c%2B%2B) for examples. ### ``Java`` With CMake, use the ``-DZ3_BUILD_JAVA_BINDINGS=ON`` option. For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and troubleshooting, see the [Java IDE Setup Guide](https://github.com/z3prover/z3/blob/master/doc/JAVA_IDE_SETUP.md). See [``examples/java``](https://github.com/z3prover/z3/blob/master/examples/java) for examples. ### ``Go`` With CMake, use the ``-DZ3_BUILD_GO_BINDINGS=ON`` option. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build. See [``examples/go``](https://github.com/z3prover/z3/blob/master/examples/go) for examples and [``src/api/go/README.md``](https://github.com/z3prover/z3/blob/master/src/api/go/README.md) for complete API documentation. ### ``OCaml`` With CMake, use the ``-DZ3_BUILD_OCAML_BINDINGS=ON`` option. See [``examples/ml``](https://github.com/z3prover/z3/blob/master/examples/ml) for examples. ### ``Python`` You can install the Python wrapper for Z3 for the latest release from pypi using the command: ```bash pip install z3-solver ``` With CMake, use the ``-DZ3_BUILD_PYTHON_BINDINGS=ON`` option. Note that it is required on certain platforms that the Python package directory (``site-packages`` on most distributions and ``dist-packages`` on Debian-based distributions) live under the install prefix. If you use a non-standard prefix you can use the ``-DCMAKE_INSTALL_PYTHON_PKG_DIR=`` option to change the Python package directory used for installation. For example: ```bash cmake -S . -B build -DCMAKE_INSTALL_PREFIX=/home/leo -DZ3_BUILD_PYTHON_BINDINGS=ON -DCMAKE_INSTALL_PYTHON_PKG_DIR=/home/leo/lib/python3.x/site-packages ``` If you do need to install to a non-standard prefix, a better approach is to use a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/) and install Z3 there. Under Windows, recall to build inside the Visual C++ native command build environment. Note that the ``build/python/z3`` directory should be accessible from where Python is used with Z3 and it requires ``libz3.dll`` to be in the path. ```bash virtualenv venv source venv/bin/activate cmake -S . -B build -DCMAKE_INSTALL_PREFIX=$VIRTUAL_ENV -DZ3_BUILD_PYTHON_BINDINGS=ON cmake --build build --parallel $(nproc) cmake --install build # You will find Z3 and the Python bindings installed in the virtual environment venv/bin/z3 -h ... python -c 'import z3; print(z3.get_version_string())' ... ``` See [``examples/python``](https://github.com/z3prover/z3/blob/master/examples/python) for examples. ### ``Julia`` The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C API of Z3. A previous version of it wrapped the C++ API: Information about updating and building the Julia bindings can be found in [src/api/julia](https://github.com/z3prover/z3/blob/master/src/api/julia). ### ``WebAssembly`` / ``TypeScript`` / ``JavaScript`` A WebAssembly build with associated TypeScript typings is published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). Information about building these bindings can be found in [src/api/js](https://github.com/z3prover/z3/blob/master/src/api/js). ### Smalltalk (``Pharo`` / ``Smalltalk/X``) Project [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) provides a Smalltalk interface to Z3's C API. For more information, see [MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md). ### AIX [Build settings for AIX are described here.](https://github.com/Z3Prover/z3/pull/8113) ## System Overview  ## Interfaces * Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu) * Other native foreign function interfaces: * [C++ API](https://z3prover.github.io/api/html/namespacez3.html) * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html) * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html) * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html)) * [Rust](https://github.com/prove-rs/z3.rs) * C * OCaml * [Julia](https://github.com/ahumenberger/Z3.jl) * [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (supports Pharo and Smalltalk/X) ## Power Tools * The [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) currently developed by ETH Zurich # Policy for filing fuzz bugs Z3 is a popular target for fuzzers. Many (best) papers have been published on finding bugs in z3 and SMT solvers and without doubt the bug file/fix ratio plays an important role establishing evidence in the publications for the value of fuzz tools. Unfortunately, addressing fuzz bugs doesn't necessarily advance uses of z3 where it matters most to users, and efforts to address them takes time away from such activities. With rapidly increasing quality of coding agents for diagnostics and fixes it is now a reasonable ask that fuzz bug reports make a solid effort on diagnostics and fix. To help focus efforts on what matters, fuzz bugs without further analysis than a repro may be closed without further consideration.
