Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

Z3Prover/z3

The Z3 Theorem Prover
Source code at GitHub null
Z3Prover/z3.json
{
  "createdAt": "2015-03-26T18:16:07Z",
  "defaultBranch": "master",
  "description": "The Z3 Theorem Prover",
  "fullName": "Z3Prover/z3",
  "homepage": null,
  "language": "C++",
  "name": "z3",
  "pushedAt": "2025-11-26T02:08:17Z",
  "stargazersCount": 11572,
  "topics": [],
  "updatedAt": "2025-11-26T02:08:24Z",
  "url": "https://github.com/Z3Prover/z3"
}

Z3

Section titled “Z3”

Z3 is a theorem prover from Microsoft Research. It is licensed under the [MIT license]!(LICENSE.txt). 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]!(RELEASE_NOTES.md) for notes on various stable releases of Z3.

![Try the online Z3 Guide]!(z3guide.jpeg)

Build status

Section titled “Build status”
Azure PipelinesOpen BugsAndroid BuildWASM BuildWindows BuildPyodide BuildOCaml Build
Build StatusOpen IssuesAndroid BuildWASM BuildWindowsPyodide BuildOCaml Build

[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

Section titled “Building Z3 on Windows using Visual Studio Command Prompt”

For 32-bit builds, start with:

Terminal window
python scripts/mk_make.py

or instead, for a 64-bit build:

Terminal window
python scripts/mk_make.py -x

then run:

Terminal window
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
  • These can be disabled using python scripts/mk_make.py --no-guardcf (Python build) or cmake -DZ3_ENABLE_CFG=OFF (CMake build) if needed

Building Z3 using make and GCC/Clang

Section titled “Building Z3 using make and GCC/Clang”

Execute:

Terminal window
python scripts/mk_make.py
cd build
make
sudo make install

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:

Terminal window
CXX=clang++ CC=clang python scripts/mk_make.py

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

Terminal window
CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

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:

Terminal window
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

To uninstall Z3, use

Terminal window
sudo make uninstall

To clean Z3, you can delete the build directory and run the mk_make.py script again.

Building Z3 using CMake

Section titled “Building Z3 using CMake”

Z3 has a build system using CMake. Read the [README-CMake.md]!(README-CMake.md) file for details. It is recommended for most build tasks, except for building OCaml bindings.

Building Z3 using vcpkg

Section titled “Building Z3 using vcpkg”

vcpkg is a full platform package manager. To install Z3 with vcpkg, execute:

Terminal window
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

Section titled “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):

bazel build //...

Dependencies

Section titled “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

Section titled “Z3 bindings”

Z3 has bindings for various programming languages.

.NET

Section titled “.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]!(examples/dotnet) for examples.

C

Section titled “C”

These are always enabled.

See [examples/c]!(examples/c) for examples.

C++

Section titled “C++”

These are always enabled.

See [examples/c++]!(examples/c++) for examples.

Java

Section titled “Java”

Use the --java command line flag with mk_make.py to enable building these.

See [examples/java]!(examples/java) for examples.

OCaml

Section titled “OCaml”

Use the --ml command line flag with mk_make.py to enable building these.

See [examples/ml]!(examples/ml) for examples.

Python

Section titled “Python”

You can install the Python wrapper for Z3 for the latest release from pypi using the command:

Terminal window
   pip install z3-solver

Use the --python command line flag with mk_make.py to enable building these.

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 --pypkgdir option to change the Python package directory used for installation. For example:

Terminal window
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

If you do need to install to a non-standard prefix, a better approach is to use a Python virtual environment and install Z3 there. Python packages also work for Python3. 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.

Terminal window
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# 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]!(examples/python) for examples.

Julia

Section titled “Julia”

The Julia package 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]!(src/api/julia).

WebAssembly / TypeScript / JavaScript

Section titled “WebAssembly / TypeScript / JavaScript”

A WebAssembly build with associated TypeScript typings is published on npm as z3-solver. Information about building these bindings can be found in [src/api/js]!(src/api/js).

Smalltalk (Pharo / Smalltalk/X)

Section titled “Smalltalk (Pharo / Smalltalk/X)”

Project MachineArithmetic provides a Smalltalk interface to Z3’s C API. For more information, see MachineArithmetic/README.md.

System Overview

Section titled “System Overview”

System Diagram

Interfaces

Section titled “Interfaces”

Power Tools

Section titled “Power Tools”