Z3Prover / z3

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][1], a [Makefile][2], using [CMake][3], using [vcpkg][4], or using [Bazel][5]. It provides [bindings for several programming languages][6]. 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 | | ---------------------|-------------------|----------------|----------------------|--------------------| | | | | | | [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang [3]: #building-z3-using-cmake [4]: #building-z3-using-vcpkg [5]: #building-z3-using-bazel [6]: #z3-bindings Building Z3 on Windows using Visual Studio Command Prompt For 32-bit builds, start with: or instead, for a 64-bit build: then run: 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 ( ) - 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 ( ) - enabled by default for memory layout randomization, required by the linker option • These can be disabled using (Python build) or (CMake build) if needed Building Z3 using make and GCC/Clang Execute: Note by default g++ is used as C++ compiler if it is available. If you prefer to use Clang, change the mk_make.py invocation to: Note that Clang < 3.7 does not support OpenMP. You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. In that case, make sure to use Cygwin's own Python and not some Windows installation of Python. For a 64-bit build (from Cygwin64), configure Z3's sources with A 32-bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32. By default, it will install z3 executables at PREFIX/bin , libraries at PREFIX/lib , and include files at PREFIX/include , where the PREFIX installation prefix is inferred by the mk_make.py script. It is usually /usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use the --prefix= command-line option to change the install prefix. For example: To uninstall Z3, use To clean Z3, you can delete the build directory and run the mk_make.py script again. Building Z3 using CMake Z3 has a build system using CMake. Read the README-CMake.md file for details. It is recommended for most build tasks, except for building OCaml bindings. Building Z3 using vcpkg vcpkg is a full platform package manager. To install Z3 with vcpkg, execute: Building Z3 using Bazel Z3 can be built using Bazel. This is known to work on Ubuntu with Clang (but may work elsewhere with other compilers): 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. Use the --dotnet command line flag with mk_make.py to enable building these. See examples/dotnet for examples. C These are always enabled. See examples/c for examples. C++ These are always enabled. See examples/c++ for examples. Java Use the --java command line flag with mk_make.py to enable building these. For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and troubleshooting, see the Java IDE Setup Guide. See examples/java for examples. Go Use the --go command line flag with mk_make.py to enable building these. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build. With CMake, use the -DZ3_BUILD_GO_BINDINGS=ON option. See examples/go for examples and src/api/go/README.md for complete API documentation. OCaml Use the --ml command line flag with mk_make.py to enable building these. See examples/ml for examples. Python You can install the Python wrapper for Z3 for th…