Installation

Z3 can be installed using package managers for various programming languages, or built from source for custom configurations. Choose the method that best fits your needs.

Pre-built packages

The easiest way to install Z3 is through language-specific package managers. These include both the Z3 library and language bindings.

Python

Install via pip (recommended):

pip install z3-solver

This installs the Z3 library with Python bindings for Python 3.x. The package includes pre-compiled binaries for Windows, Linux, and macOS.

Use a virtual environment to isolate Z3 from other Python packages:

python -m venv z3env
source z3env/bin/activate  # On Windows: z3env\Scripts\activate
pip install z3-solver

JavaScript/TypeScript

Install via npm:

npm install z3-solver

Or with Yarn:

yarn add z3-solver

The package provides TypeScript typings and a WebAssembly build of Z3.

.NET

Install the NuGet package:

dotnet add package Microsoft.Z3

Or add it to your .csproj file:

<PackageReference Include="Microsoft.Z3" Version="*" />

Java

Add to your Maven pom.xml:

<dependency>
  <groupId>tools.aqua</groupId>
  <artifactId>z3-turnkey</artifactId>
  <version>4.12.2.1</version>
</dependency>

For Gradle:

implementation 'tools.aqua:z3-turnkey:4.12.2.1'

For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code), see the Java IDE Setup Guide.

Pre-built binaries

Download pre-built binaries for stable and nightly releases from the GitHub Releases page. These releases include:

The z3 command-line executable
Static and shared libraries
Header files
Language bindings

Linux
macOS
Windows

Download the appropriate release for your architecture (x64, ARM, etc.)
Extract the archive:
```
tar -xzf z3-*.tar.gz
```

Add to your PATH:

export PATH=$PATH:/path/to/z3/bin
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/path/to/z3/bin

Download the macOS release
Extract the archive:
```
tar -xzf z3-*.tar.gz
```

Add to your PATH:

export PATH=$PATH:/path/to/z3/bin
export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/path/to/z3/bin

Download the Windows release (x64 or x86)
Extract the ZIP file
Add the bin directory to your PATH:
- Right-click “This PC” → Properties → Advanced system settings
- Click “Environment Variables”
- Edit the Path variable and add C:\path\to\z3\bin

Building from source

Building from source gives you the latest features and allows customization. Z3 requires Python 3.x and C++20 support.

Using CMake (recommended)

CMake is the recommended build system for most platforms.

Clone the repository

git clone https://github.com/Z3Prover/z3.git
cd z3

Create build directory

mkdir build
cd build

Configure with CMake

Linux/macOS
Windows (Visual Studio)

cmake -DCMAKE_BUILD_TYPE=Release ..

For a debug build:

cmake -DCMAKE_BUILD_TYPE=Debug ..

cmake -G "Visual Studio 17 2022" ..

For 32-bit builds:

cmake -G "Visual Studio 17 2022" -A Win32 ..

Build

cmake --build . --config Release

Or use parallel builds for faster compilation:

cmake --build . --config Release -j 8

Install (optional)

sudo cmake --install .

To install to a custom location:

cmake --install . --prefix /usr/local

For detailed CMake options and configuration, see README-CMake.md in the Z3 repository.

Using Make

For Linux and macOS systems, you can use the traditional Make-based build:

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

Build options

Specify compiler:

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

Custom install prefix:

python scripts/mk_make.py --prefix=/home/user/local

64-bit build (Windows):

python scripts/mk_make.py -x

Enable Python bindings:

python scripts/mk_make.py --python

Using Visual Studio

For Windows developers using Visual Studio:

Open Visual Studio Command Prompt

Launch the “Developer Command Prompt” for your Visual Studio version.

Generate build files

For 32-bit:

python scripts/mk_make.py

For 64-bit:

python scripts/mk_make.py -x

Build

cd build
nmake

Z3 uses C++20, so Visual Studio 2019 or later is recommended.

Security features: By default, MSVC builds enable Control Flow Guard (/guard:cf) and Address Space Layout Randomization (/DYNAMICBASE). To disable:

python scripts/mk_make.py --no-guardcf

Or with CMake:

cmake -DZ3_ENABLE_CFG=OFF ..

Using Bazel

Z3 can be built with Bazel on Ubuntu and other platforms:

bazel build //...

Using vcpkg

vcpkg is a cross-platform package manager:

git clone https://github.com/microsoft/vcpkg.git
cd vcpkg
./bootstrap-vcpkg.sh  # On Windows: .\bootstrap-vcpkg.bat
./vcpkg install z3

Building language bindings

When building from source, you can enable specific language bindings.

Python bindings

CMake
Make

cmake -DZ3_BUILD_PYTHON_BINDINGS=ON \
      -DZ3_BUILD_LIBZ3_SHARED=ON \
      ..
make
make install

python scripts/mk_make.py --python
cd build
make
make install

Java bindings

cmake -DZ3_BUILD_JAVA_BINDINGS=ON ..
make

Set JAVA_HOME if CMake can’t find your Java installation:

JAVA_HOME=/usr/lib/jvm/default cmake -DZ3_BUILD_JAVA_BINDINGS=ON ..

.NET bindings

cmake -DZ3_BUILD_DOTNET_BINDINGS=ON ..
make

Go bindings

Go bindings require Go 1.20+ and shared library:

cmake -DZ3_BUILD_GO_BINDINGS=ON \
      -DZ3_BUILD_LIBZ3_SHARED=ON \
      ..
make

To use the Go bindings:

export CGO_CFLAGS="-I/path/to/z3/include"
export CGO_LDFLAGS="-L/path/to/z3/lib -lz3"
export LD_LIBRARY_PATH="/path/to/z3/lib:$LD_LIBRARY_PATH"

OCaml bindings

python scripts/mk_make.py --ml
cd build
make

The CMake build system is not recommended for OCaml bindings. Use the Make-based build instead.

Dependencies

Z3 has minimal dependencies:

Required: C++ runtime libraries, pthreads (for multi-threading)
Optional: GMP (GNU Multiple Precision library) for faster arithmetic
Build-time: Python 3.x

To use GMP:

cmake -DZ3_USE_LIB_GMP=ON ..

Platform-specific notes

Linux

Most Linux distributions can build Z3 with the default GCC or Clang compiler.Install build dependencies:

# Debian/Ubuntu
sudo apt-get install build-essential cmake python3

# Fedora/RHEL
sudo dnf install gcc-c++ cmake python3

macOS

Install Xcode command-line tools:

xcode-select --install

Or install via Homebrew:

brew install z3

Windows

Use Visual Studio 2019 or later for C++20 support
Alternatively, use Clang or MinGW with CMake
For Cygwin builds, use Cygwin’s Python and the Mingw-w64 cross-compiler

AIX

See AIX build settings for platform-specific configuration.

Verifying installation

After installation, verify Z3 is working:

Command line
Python
Java

z3 --version

Should output something like:

Z3 version 4.12.2 - 64 bit

import z3
print(z3.get_version_string())

Should output:

4.12.2

import com.microsoft.z3.*;

public class Test {
    public static void main(String[] args) {
        System.out.println(Version.getFullVersion());
    }
}

Troubleshooting

Python import error

If you get ImportError: No module named z3:

Ensure Z3 is installed: pip list | grep z3
Check you’re using the right Python environment
Verify PYTHONPATH includes the Z3 installation directory

Library not found (Linux/macOS)

If you see error while loading shared libraries: libz3.so:

# Linux
export LD_LIBRARY_PATH=/path/to/z3/lib:$LD_LIBRARY_PATH

# macOS
export DYLD_LIBRARY_PATH=/path/to/z3/lib:$DYLD_LIBRARY_PATH

Add these to your .bashrc or .zshrc for persistence.

CMake can't find compiler

Set the compiler explicitly:

CC=gcc CXX=g++ cmake ..
# or
CC=clang CXX=clang++ cmake ..

Build fails with C++ errors

Z3 requires C++20. Ensure your compiler is recent enough:

GCC 10 or later
Clang 10 or later
Visual Studio 2019 or later

Next steps

Quickstart tutorial

Solve your first problem with Z3

Python bindings

Learn the Python API in depth

Building Z3

Advanced build configuration and options

Examples

Explore code examples and tutorials

Getting Started

Core Concepts

Building Z3

Guides

Pre-built packages

Python

JavaScript/TypeScript

.NET

Java

Pre-built binaries

Building from source

Using CMake (recommended)

Using Make

Using Visual Studio

Using Bazel

Using vcpkg

Building language bindings

Python bindings

Java bindings

.NET bindings

Go bindings

OCaml bindings

Dependencies

Platform-specific notes

Verifying installation

Troubleshooting

Next steps

Quickstart tutorial

Python bindings

Building Z3

Examples

Build docs developers (and LLMs) love

Getting Started

Core Concepts

Building Z3

Guides

​Pre-built packages

​Python

​JavaScript/TypeScript

​.NET

​Java

​Pre-built binaries

​Building from source

​Using CMake (recommended)

​Using Make

​Using Visual Studio

​Using Bazel

​Using vcpkg

​Building language bindings

​Python bindings

​Java bindings

​.NET bindings

​Go bindings

​OCaml bindings

​Dependencies

​Platform-specific notes

​Verifying installation

​Troubleshooting

​Next steps

Quickstart tutorial

Python bindings

Building Z3

Examples

Build docs developers (and LLMs) love

Pre-built packages

Python

JavaScript/TypeScript

.NET

Java

Pre-built binaries

Building from source

Using CMake (recommended)

Using Make

Using Visual Studio

Using Bazel

Using vcpkg

Building language bindings

Python bindings

Java bindings

.NET bindings

Go bindings

OCaml bindings

Dependencies

Platform-specific notes

Verifying installation

Troubleshooting

Next steps