Building with Visual Studio - Z3 Theorem Prover

Z3 can be built on Windows using Visual Studio’s command-line tools (nmake) or the Visual Studio IDE with CMake integration.

Prerequisites

Visual Studio 2019 or later (recommended for C++20 support)
Python (for build configuration with mk_make.py)
CMake 3.16+ (for CMake-based builds)

Z3 uses C++20, so Visual Studio 2019 or later is recommended for full language support.

Quick Start with Command Line

Open Developer Command Prompt

Launch the “Developer Command Prompt for Visual Studio” or “x64 Native Tools Command Prompt” from the Start menu.

Configure the build

For a 32-bit build:

python scripts/mk_make.py

For a 64-bit build:

python scripts/mk_make.py -x

Build with nmake

cd build
nmake

Using Visual Studio IDE with CMake

Visual Studio 2019+

Visual Studio 2019 and later have integrated CMake support:

Open the Z3 folder

In Visual Studio, select File → Open → Folder and navigate to the Z3 repository root directory.

Configure CMake

Visual Studio will automatically detect CMakeLists.txt and begin configuration. You can customize CMake options in CMakeSettings.json.

Select build configuration

Choose your build configuration (Debug, Release, etc.) from the dropdown in the toolbar.

Build the project

Select Build → Build All or press Ctrl+Shift+B.

Legacy Visual Studio Versions

For older Visual Studio versions, use CMake GUI:

Create build directory

Create an empty directory for build outputs.

Launch CMake GUI

Start the cmake-gui application.

Configure paths

Set “Where is the source code” to the Z3 repository root
Set “Where to build the binaries” to your empty build directory

Configure the project

Click Configure
Select your Visual Studio version as the generator
Choose platform (Win32 for 32-bit, x64 for 64-bit)
Click Finish

Adjust options

Modify any CMake options as needed. Click Configure again after changes.

Generate solution

Click Generate to create the Visual Studio solution file.

Build in Visual Studio

Open the generated Z3.sln file in the build directory
Select your build type (Debug/Release) in Visual Studio
Build the solution with Build → Build Solution

Security Features (MSVC)

When building with MSVC, Z3 enables several security features by default to protect against exploitation:

Control Flow Guard (CFG)

Enabled by default - Control Flow Guard protects against control flow hijacking attacks:

Compiler flag: /guard:cf
Linker flag: /GUARD:CF
Purpose: Validates indirect call targets at runtime to prevent attackers from redirecting control flow

With Python Build System

Disable if needed:

python scripts/mk_make.py --no-guardcf

With CMake

Disable if needed:

cmake -DZ3_ENABLE_CFG=OFF ../

Control Flow Guard is enabled by default on MSVC builds and provides important security hardening.

Address Space Layout Randomization (ASLR)

Automatically enabled with Control Flow Guard:

Linker flag: /DYNAMICBASE
Purpose: Randomizes memory addresses to make exploitation more difficult
Note: Required for Control Flow Guard to function

Incompatibilities

Control Flow Guard is incompatible with:

/ZI - Edit and Continue debug information format
/clr - Common Language Runtime compilation

When these options are detected, CFG is automatically disabled with a warning.

Control Flow Guard is incompatible with Edit and Continue (/ZI). Use /Zi for debug builds instead.

Build Configurations

With Python Script (nmake)

# 64-bit Release build
python scripts/mk_make.py -x
cd build
nmake

# 32-bit Debug build
python scripts/mk_make.py
cd build
nmake

# With Python bindings
python scripts/mk_make.py -x --python
cd build
nmake

With CMake and NMake

Ninja is recommended over NMake for significantly faster builds.

mkdir build
cd build
cmake -G "NMake Makefiles" -DCMAKE_BUILD_TYPE=Release ../
nmake

With CMake and Ninja

Ninja is much faster than NMake:

mkdir build
cd build
cmake -G "Ninja" -DCMAKE_BUILD_TYPE=Release ../
ninja

Language Bindings

.NET Bindings

Build with .NET support:

# Using Python script
python scripts/mk_make.py --dotnet
cd build
nmake

# Using CMake
cmake -DZ3_BUILD_DOTNET_BINDINGS=ON ../

Z3 also provides a NuGet package at nuget.org/packages/Microsoft.Z3.

Python Bindings

Build inside the Visual C++ native command prompt:

python scripts/mk_make.py -x --python
cd build
nmake

The build/python/z3 directory must be accessible from where Python runs, and libz3.dll must be in the PATH.

Java Bindings

# Using Python script
python scripts/mk_make.py --java
cd build
nmake

# Using CMake
cmake -DZ3_BUILD_JAVA_BINDINGS=ON ../

For IDE setup and troubleshooting, see the Java IDE Setup Guide.

Static vs Shared Library

Static Library (default)

cmake -DZ3_BUILD_LIBZ3_SHARED=OFF ../

Shared Library (DLL)

cmake -DZ3_BUILD_LIBZ3_SHARED=ON ../

Visual Studio Generator Selection

When using CMake GUI, select the appropriate generator:

Generator	Architecture	Visual Studio Version
Visual Studio 17 2022	x64	VS 2022 (64-bit)
Visual Studio 17 2022	Win32	VS 2022 (32-bit)
Visual Studio 16 2019	x64	VS 2019 (64-bit)
Visual Studio 16 2019	Win32	VS 2019 (32-bit)
Visual Studio 15 2017 Win64	x64	VS 2017 (64-bit)
Visual Studio 15 2017	Win32	VS 2017 (32-bit)

Generators with “Win64” in the name indicate 64-bit builds. Without it, they’re 32-bit builds.

CMake Configuration Options

Common options for Visual Studio builds:

# Release build with Python bindings
cmake -DCMAKE_BUILD_TYPE=Release \
      -DZ3_BUILD_PYTHON_BINDINGS=ON \
      -DZ3_BUILD_LIBZ3_SHARED=ON ../

# Debug build without Control Flow Guard
cmake -DCMAKE_BUILD_TYPE=Debug \
      -DZ3_ENABLE_CFG=OFF ../

# Link-time optimization enabled
cmake -DCMAKE_BUILD_TYPE=Release \
      -DZ3_LINK_TIME_OPTIMIZATION=ON ../

See the CMake build guide for a complete list of options.

Multi-Configuration Builds

Visual Studio is a multi-configuration generator - you don’t set the build type when running CMake:

# Configure once
cmake -G "Visual Studio 17 2022" -A x64 ../

# Then select Debug or Release in Visual Studio IDE

With command-line tools:

# Build Debug configuration
cmake --build . --config Debug

# Build Release configuration
cmake --build . --config Release

Installation

Install to a specific location:

cmake -DCMAKE_INSTALL_PREFIX="C:/Program Files/Z3" ../
cmake --build . --config Release
cmake --install . --config Release

Troubleshooting

C++20 Errors

Ensure you’re using Visual Studio 2019 or later:

# Check Visual Studio version
where cl
cl /?

Python Not Found

Add Python to your PATH or specify the full path:

C:\Python39\python.exe scripts/mk_make.py

Missing DLL at Runtime

Ensure libz3.dll is in your PATH or in the same directory as the executable:

set PATH=%PATH%;C:\path\to\z3\build

Control Flow Guard Warnings

If you see CFG incompatibility warnings, either:

Disable Edit and Continue (use /Zi instead of /ZI)
Disable Control Flow Guard: -DZ3_ENABLE_CFG=OFF

CMake Can’t Find Visual Studio

Run CMake from the Developer Command Prompt, or specify the generator explicitly:

cmake -G "Visual Studio 17 2022" ../

Build Performance

Parallel Builds

With nmake (single-threaded), consider using Ninja instead:

cmake -G "Ninja" ../
ninja -j8  # Use 8 parallel jobs

With MSBuild (Visual Studio):

cmake --build . --config Release -- /m:8

Incremental Builds

Ninja provides much faster incremental builds than NMake:

# Install Ninja via Chocolatey
choco install ninja

# Use Ninja generator
cmake -G "Ninja" ../
ninja

Next Steps

Learn about CMake builds for cross-platform development
See Make builds for Unix-like systems
Explore Bazel builds for advanced scenarios

​Prerequisites

​Quick Start with Command Line

​Using Visual Studio IDE with CMake

​Visual Studio 2019+

​Legacy Visual Studio Versions

​Security Features (MSVC)

​Control Flow Guard (CFG)

​With Python Build System

​With CMake

​Address Space Layout Randomization (ASLR)

​Incompatibilities

​Build Configurations

​With Python Script (nmake)

​With CMake and NMake

​With CMake and Ninja

​Language Bindings

​.NET Bindings

​Python Bindings

​Java Bindings

​Static vs Shared Library

​Static Library (default)

​Shared Library (DLL)

​Visual Studio Generator Selection

​CMake Configuration Options

​Multi-Configuration Builds

​Installation

​Troubleshooting

​C++20 Errors

​Python Not Found

​Missing DLL at Runtime

​Control Flow Guard Warnings

​CMake Can’t Find Visual Studio

​Build Performance

​Parallel Builds

​Incremental Builds

​Next Steps

Prerequisites

Quick Start with Command Line

Using Visual Studio IDE with CMake

Visual Studio 2019+

Legacy Visual Studio Versions

Security Features (MSVC)

Control Flow Guard (CFG)

With Python Build System

With CMake

Address Space Layout Randomization (ASLR)

Incompatibilities

Build Configurations

With Python Script (nmake)

With CMake and NMake

With CMake and Ninja

Language Bindings

.NET Bindings

Python Bindings

Java Bindings

Static vs Shared Library

Static Library (default)

Shared Library (DLL)

Visual Studio Generator Selection

CMake Configuration Options

Multi-Configuration Builds

Installation

Troubleshooting

C++20 Errors

Python Not Found

Missing DLL at Runtime

Control Flow Guard Warnings

CMake Can’t Find Visual Studio

Build Performance

Parallel Builds

Incremental Builds

Next Steps