Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Windows binary distributions include C++ runtime redistributables

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available here.

Z3 can be built using Visual Studio, a Makefile, using CMake, using vcpkg, or using Bazel. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Build status

Pull Request & Push Workflows

| WASM Build | Windows Build | CI | OCaml Binding | | ------------|---------------|----|-----------| | | | | |

Scheduled Workflows

| Open Bugs | Android Build | Pyodide Build | Nightly Build | Cross Build | | -----------|---------------|---------------|---------------|-------------| | | | | | |

| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Code Coverage | Memory Safety | Mark PRs Ready | |-------------|---------------|----------------|---------------|---------------|----------------| | | | | | | |

Manual & Release Workflows

| Documentation | Release Build | WASM Release | NuGet Build | |---------------|---------------|--------------|-------------| | | | | |

Specialized Workflows

| Nightly Validation | Copilot Setup | Agentics Maintenance | |--------------------|---------------|----------------------| | | | |

Agentic Workflows

| A3 Python | API Coherence | Code Simplifier | Release Notes | Workflow Suggestion | | ----------|---------------|-----------------|---------------|---------------------| | | | | | |

| Academic Citation | Build Warning Fixer | Code Conventions | CSA Report | Issue Backlog | | ------------------|---------------------|------------------|------------|---------------| | | | | | |

| Memory Safety Report | Ostrich Benchmark | QF-S Benchmark | Tactic-to-Simplifier | ZIPT Code Reviewer | | ---------------------|-------------------|----------------|----------------------|--------------------| | | | | | |

Building Z3 on Windows using Visual Studio Command Prompt

For 32-bit builds, start with:

python scripts/mk_make.py

or instead, for a 64-bit build:

python scripts/mk_make.py -x

then run:

cd build
nmake

Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later.

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
• Thes