z3 Documentation

C++ repository by @Z3Prover. AI agent rules & system prompts with 13k stars.

12,540 stars C++ C++ 1 file ยท ~10,456 tokens
RAW Doc

Docker & Self-Hosted Deployment Verified OCI

Deploy z3 on any server, homelab, or cloud container platform.

1-Click Terminal Command
bash (docker run) 
docker run -d --name z3 --restart always z3prover/z3:latest

File: README.md

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

Android Build Pyodide Wheel (PyPI) Nightly Build Cross Build F* Master Build
MSVC Static MSVC Clang-CL Build Z3 Cache Memory Safety Mark PRs Ready

Manual & Release Workflows

Documentation Release Build WASM Release

Specialized Workflows

Nightly Validation Copilot Setup Agentics Maintenance

Agentic Workflows

API Coherence Code Simplifier Release Notes Workflow Suggestion Academic Citation
Issue Backlog Memory Safety Report SMTLIB Benchmark Finder

Building Z3 on Windows using Visual Studio Command Prompt

For 32-bit builds, start with:

bash
python scripts/mk_make.py

or instead, for a 64-bit build:

bash
python scripts/mk_make.py -x

then run:

bash
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

Execute:

bash
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:

bash
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

bash
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:

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

To uninstall Z3, use

bash
sudo make uninstall

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:

bash
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

Z3 can be built using Bazel. This is known to work on
Ubuntu with Clang (but may work elsewhere with other compilers):

text
bazel build //...

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 the latest release from pypi using the command:

bash
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:

bash
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.

bash
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 for examples.

``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.

``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.

Smalltalk (``Pharo`` / ``Smalltalk/X``)

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

AIX

Build settings for AIX are described here.

System Overview

Interfaces

Power Tools

File: contrib/suppressions/sanitizers/README.md

Sanitizer suppression files

This directory contains files used to suppress
ASan/LSan/UBSan warnings/errors.

File: contrib/suppressions/README.md

Suppression files

This directory contains suppression files used by various
program analysis tools.

Suppression files tell a program analysis tool to suppress
various warnings/errors.

File: doc/design_recfuns.md

Design for handling recursive functions

Main source of inspiration is [Sutter, Kรถksal & Kuncak 2011],
as implemented in Leon, but the main
differences is that we should unroll function definitions directly from the
inside of Z3, in a backtracking way. Termination and fairness are ensured by
iterative-deepening on the maximum number of unrollings in a given branch.

Unfolding

The idea is that every function definition f(x1โ€ฆxn) := rhs[x1โ€ฆxn] is
compiled into:

  • a list of cases A_f_i[x1โ€ฆxn] => f(x1โ€ฆxn) = rhs_i[x1โ€ฆxn].
    When A_f_i[t1โ€ฆtn] becomes true in the model, f(t1โ€ฆtn) is said to be
    unfolded and the clause A_f_i[t1โ€ฆtn] => f(t1โ€ฆtn) = rhs_i[t1โ€ฆtn]
    is added as an auxiliary clause.
  • a list of constraints ฮ“_f_i[x1โ€ฆxn] <=> A_f_i[x1โ€ฆxn]
    that states when A_f_i[x1โ€ฆxn] should be true, depending on inputs x1โ€ฆxn.
    For every term f(t1โ€ฆtn) present in congruence closure, we
    immediately add all the ฮ“_f_i[t1โ€ฆtn] <=> A_f_i[t1โ€ฆtn] as auxiliary clauses
    (maybe during internalization of f(t1โ€ฆtn)?).

where each A_f_i[x1โ€ฆxn] is a special new predicate representing the
given case of f, and rhs_i does not contain any ite.
We assume pattern matching has been compiled to ite beforehand.

For example, fact(n) := if n<2 then 1 else n * fact(n-1) is compiled into:

  • A_fact_0[n] => fact(n) = 1
  • A_fact_1[n] => fact(n) = n * fact(n-1)
  • A_fact_0[n] <=> n < 2
  • A_fact_1[n] <=> ยฌ(n < 2)

The 2 first clauses are only added when A_fact_0[t] is true
(respectively A_fact_1[t] is true).
The 2 other clauses are added as soon as fact(t) is internalized.

Termination

To ensure termination, we define variables:

  • unfold_depth: int
  • current_max_unfold_depth: int
  • global_max_unfold_depth: int

and a special literal [max_depth=$n] for each n:int.
Solving is done under the local assumption
[max_depth=$current_max_unfold_depth] (this should be handled in some outer
loop, e.g. in a custom tactic).

Whenever A_f_i[t1โ€ฆtn] becomes true (for any f), we increment
unfold_depth. If unfold_depth > current_max_unfold_depth, then
the conflict clause [max_depth=$current_max_unfold_depth] => ฮ“ => false
where ฮ“ is the conjunction of all A_f_i[t1โ€ฆtn] true in the trail.

For non-recursive functions, we don't have to increment unfold_depth. Some other functions that are known

If the solver answers "SAT", we have a model.
Otherwise, if [max_depth=$current_max_unfold_depth] is part of the
unsat-core, then we increase current_max_unfold_depth.
If current_max_unfold_depth == global_max_unfold_depth then
we report "UNKNOWN" (reached global depth limit), otherwise we can
try to solve() again with the new assumption (higher depth limit).

Tactic

there should be a parametrized tactic funrec(t, n) where t is the tactic
used to solve (under assumption that depth is limited to current_max_unfold_depth)
and n is an integer that is assigned to global_max_unfold_depth.

This way, to try and find models for a problem with recursive functions + LIA,
one could use something like (funrec (then simplify dl smt) 100).

Expected benefits

This addition to Z3 would bring many benefits compared to current alternatives (Leon, quantifiers, โ€ฆ)

  • should be very fast and lightweight
    (compared to Leon or quantifiers).
    In particular, every function call is very lightweight even compared to Leon (no need for full model building, followed by unsat core extraction)
  • possibility of answering "SAT" for any QF_* fragment +
    recursive functions
  • makes define-funs-rec a first-class citizen of the language, usable to model user-defined theories or to analyze functional
    programs directly

Optimizations

  • maybe C_f_i literals should never be decided on
    (they can always be propagated).
    Even stronger: they should not be part of conflicts?
    (i.e. tune conflict resolution to always resolve
    these literals away, disregarding their level)

File: doc/JAVA_IDE_SETUP.md

Z3 Java Bindings: IDE Setup Guide

This guide explains how to set up and use Z3 Java bindings in popular Java IDEs (Eclipse, IntelliJ IDEA, and Visual Studio Code).

Prerequisites

Before setting up Z3 in your IDE, you need to obtain the Z3 binaries:

  1. Download the appropriate Z3 release for your platform from the Z3 Releases page

    • For Windows: z3-x.x.x-x64-win.zip
    • For Linux: z3-x.x.x-x64-glibc-x.x.zip
    • For macOS: z3-x.x.x-x64-osx-x.x.zip

  2. Extract the archive to a location on your system (e.g., C:\z3 on Windows or /opt/z3 on Linux/macOS)

  3. The extracted folder contains:

    • bin/com.microsoft.z3.jar - The Java API library
    • bin/libz3.dll (Windows) / bin/libz3.so (Linux) / bin/libz3.dylib (macOS) - The native Z3 library
    • bin/libz3java.dll (Windows) / bin/libz3java.so (Linux) / bin/libz3java.dylib (macOS) - The Java JNI bridge

Option 2: Build from Source

If you need to build Z3 from source with Java bindings enabled:

bash
python scripts/mk_make.py --java
cd build
make

The resulting files will be in the build directory.

Eclipse Setup

Step 1: Add Z3 JAR to Build Path

  1. Right-click on your Java project in the Package Explorer
  2. Select Build Path โ†’ Configure Build Path...
  3. In the Libraries tab, click Add External JARs...
  4. Navigate to the Z3 bin folder and select com.microsoft.z3.jar
  5. Click Apply and Close

Step 2: Configure Native Library Path

Eclipse needs to know where to find the native Z3 libraries (.dll, .so, or .dylib files).

Method 1: Using Eclipse Native Library Location (Recommended)

  1. In the Package Explorer, expand the Referenced Libraries section
  2. Find and expand com.microsoft.z3.jar
  3. Right-click on Native Library Location and select Edit...
  4. Click External Folder... and select the Z3 bin folder (where the native libraries are located)
  5. Click OK

Method 2: Using VM Arguments

  1. Right-click on your project โ†’ Run As โ†’ Run Configurations...
  2. Select your Java application configuration (or create a new one)
  3. Go to the Arguments tab
  4. In the VM arguments field, add:
    text
    -Djava.library.path=C:\path\to\z3\bin
    (Replace with your actual Z3 bin directory path)
  5. Click Apply and Run

Method 3: Using System PATH (Windows)

  1. Add the Z3 bin directory to your system PATH environment variable:
    • Open System Properties โ†’ Advanced โ†’ Environment Variables
    • Under System Variables, find and edit the Path variable
    • Add the full path to your Z3 bin directory (e.g., C:\z3\bin)
    • Click OK and restart Eclipse

Step 3: Verify Setup

Create a test Java file with the following code:

java
import com.microsoft.z3.*;

public class Z3Test {
    public static void main(String[] args) {
        System.out.println("Creating Z3 context...");
        Context ctx = new Context();
        System.out.println("Z3 version: " + Version.getFullVersion());
        
        // Simple example: x > 0
        IntExpr x = ctx.mkIntConst("x");
        Solver solver = ctx.mkSolver();
        solver.add(ctx.mkGt(x, ctx.mkInt(0)));
        
        if (solver.check() == Status.SATISFIABLE) {
            System.out.println("SAT");
            System.out.println("Model: " + solver.getModel());
        }
        
        ctx.close();
        System.out.println("Success!");
    }
}

Run the program. If you see the Z3 version and "Success!" printed, your setup is working correctly.

IntelliJ IDEA Setup

Step 1: Add Z3 JAR to Project

  1. Open your project in IntelliJ IDEA
  2. Go to File โ†’ Project Structure (or press Ctrl+Alt+Shift+S)
  3. Select Modules โ†’ Dependencies
  4. Click the + button and select JARs or directories...
  5. Navigate to the Z3 bin folder and select com.microsoft.z3.jar
  6. Click OK and Apply

Step 2: Configure Native Library Path

Method 1: Using Run Configuration (Recommended)

  1. Go to Run โ†’ Edit Configurations...
  2. Select your application configuration (or create a new one)
  3. In the VM options field, add:
    text
    -Djava.library.path=/path/to/z3/bin
    (Replace with your actual Z3 bin directory path)
  4. Click OK

Method 2: Using Environment Variable (Windows)

Add the Z3 bin directory to your system PATH as described in the Eclipse section above, then restart IntelliJ IDEA.

Step 3: Verify Setup

Use the same test code from the Eclipse section to verify your setup.

Visual Studio Code Setup

Step 1: Install Java Extension Pack

  1. Open Visual Studio Code
  2. Install the Extension Pack for Java from the Extensions marketplace

Step 2: Add Z3 JAR to Classpath

Create or edit .vscode/settings.json in your project root:

json
{
    "java.project.referencedLibraries": [
        "path/to/z3/bin/com.microsoft.z3.jar"
    ]
}

Step 3: Configure Native Library Path

Create or edit .vscode/launch.json in your project root:

json
{
    "version": "0.2.0",
    "configurations": [
        {
            "type": "java",
            "name": "Launch with Z3",
            "request": "launch",
            "mainClass": "YourMainClass",
            "vmArgs": "-Djava.library.path=/path/to/z3/bin"
        }
    ]
}

Replace YourMainClass with your actual main class name and adjust the path to your Z3 bin directory.

Step 4: Verify Setup

Use the same test code to verify your setup.

Command-Line Build and Run

If you prefer to build and run from the command line:

Compiling

bash
# Windows
javac -cp "C:\path\to\z3\bin\com.microsoft.z3.jar;." YourProgram.java

# Linux/macOS
javac -cp "/path/to/z3/bin/com.microsoft.z3.jar:." YourProgram.java

Running

bash
# Windows
java -cp "C:\path\to\z3\bin\com.microsoft.z3.jar;." -Djava.library.path=C:\path\to\z3\bin YourProgram

# Linux
LD_LIBRARY_PATH=/path/to/z3/bin java -cp "/path/to/z3/bin/com.microsoft.z3.jar:." YourProgram

# macOS
DYLD_LIBRARY_PATH=/path/to/z3/bin java -cp "/path/to/z3/bin/com.microsoft.z3.jar:." YourProgram

Troubleshooting

ClassNotFoundException: com.microsoft.z3.Context

Problem: Java cannot find the Z3 classes.

Solution:

  • Verify that com.microsoft.z3.jar is in your project's classpath
  • In Eclipse: Check Project Properties โ†’ Java Build Path โ†’ Libraries
  • In IntelliJ: Check File โ†’ Project Structure โ†’ Modules โ†’ Dependencies
  • Ensure you're not just copying the JAR to your project's bin folder - it must be explicitly added to the classpath

UnsatisfiedLinkError: no z3java in java.library.path

Problem: Java can find the Z3 classes but cannot load the native libraries.

Solution:

  • Verify that libz3.dll/libz3.so/libz3.dylib and libz3java.dll/libz3java.so/libz3java.dylib are in a directory accessible to Java
  • Add the Z3 bin directory to:
    • The java.library.path VM argument, or
    • The system PATH environment variable (Windows), or
    • The LD_LIBRARY_PATH (Linux) / DYLD_LIBRARY_PATH (macOS) environment variable

ExceptionInInitializerError or Z3Exception

Problem: Z3 fails to initialize properly.

Solution:

  • Ensure all Z3 files (JAR and native libraries) are from the same version
  • Check that you're using a compatible Java version (Java 8 or later)
  • Verify that the native libraries match your system architecture (32-bit vs 64-bit)

Running on Different Platforms

Windows:

  • Use semicolons (;) as classpath separators
  • Native libraries: libz3.dll and libz3java.dll
  • Set PATH or use -Djava.library.path

Linux:

  • Use colons (:) as classpath separators
  • Native libraries: libz3.so and libz3java.so
  • Set LD_LIBRARY_PATH or use -Djava.library.path

macOS:

  • Use colons (:) as classpath separators
  • Native libraries: libz3.dylib and libz3java.dylib
  • Set DYLD_LIBRARY_PATH or use -Djava.library.path

Maven/Gradle Setup

For Maven or Gradle projects, you can use system-scoped dependencies:

Maven

xml
<dependency>
    <groupId>com.microsoft</groupId>
    <artifactId>z3</artifactId>
    <version>x.x.x</version> 
    <scope>system</scope>
    <systemPath>${project.basedir}/lib/com.microsoft.z3.jar</systemPath>
</dependency>

Place the Z3 JAR in your project's lib directory and configure the native library path as described above.

Gradle

gradle
dependencies {
    implementation files('lib/com.microsoft.z3.jar')
}

Additional Resources

Building Z3 with Java Support

If you need to build Z3 from source with Java bindings:

bash
# Clone the repository
git clone https://github.com/Z3Prover/z3.git
cd z3

# Configure with Java support
python scripts/mk_make.py --java

# Build
cd build
make

# The Java bindings will be in the build directory
# - com.microsoft.z3.jar
# - libz3java.so / libz3java.dll / libz3java.dylib
# - libz3.so / libz3.dll / libz3.dylib

For more details on building Z3, see the main README.md.

File: examples/go/README.md

Z3 Go Examples

This directory contains examples demonstrating how to use the Z3 Go bindings.

Examples

basic_example.go

Demonstrates fundamental Z3 operations:

  • Creating contexts and solvers
  • Defining integer and boolean variables
  • Adding constraints
  • Checking satisfiability
  • Extracting models

Building and Running

Prerequisites

  1. Build Z3 with Go bindings enabled
  2. Ensure Z3 library is in your library path
  3. Go 1.20 or later

Linux/macOS

bash
# Build Z3 first
cd ../..
mkdir build && cd build
cmake ..
make -j$(nproc)

# Set up environment
cd ../examples/go
export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I../../src/api"
export CGO_LDFLAGS="-L../../build -lz3"

# Run examples
go run basic_example.go

Windows

cmd
REM Build Z3 first
cd ..\..
mkdir build
cd build
cmake ..
cmake --build . --config Release

REM Set up environment
cd ..\examples\go
set PATH=..\..\build\Release;%PATH%
set CGO_CFLAGS=-I..\..\src\api
set CGO_LDFLAGS=-L..\..\build\Release -lz3

REM Run examples
go run basic_example.go

Expected Output

When you run basic_example.go, you should see output similar to:

text
Z3 Go Bindings - Basic Example
================================

Example 1: Solving x > 0
Satisfiable!
Model: ...
x = 1

Example 2: Solving x + y = 10 โˆง x - y = 2
Satisfiable!
x = 6
y = 4

Example 3: Boolean satisfiability
Satisfiable!
p = false
q = true

Example 4: Checking unsatisfiability
Status: unsat
The constraints are unsatisfiable (as expected)

All examples completed successfully!

Creating Your Own Examples

  1. Import the Z3 package:

    go
    import "github.com/Z3Prover/z3/src/api/go"

  2. Create a context:

    go
    ctx := z3.NewContext()

  3. Create variables and constraints:

    go
    x := ctx.MkIntConst("x")
constraint := ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort()))

  4. Solve:

    go
    solver := ctx.NewSolver()
solver.Assert(constraint)
if solver.Check() == z3.Satisfiable {
    model := solver.Model()
    // Use model...
}

Troubleshooting

"undefined reference to Z3_*" errors

Make sure:

  • Z3 is built and the library is in your library path
  • CGO_LDFLAGS includes the correct library path
  • On Windows, the DLL is in your PATH

"cannot find package" errors

Make sure:

  • CGO_CFLAGS includes the Z3 API header directory
  • The go.mod file exists in src/api/go

CGO compilation errors

Ensure:

  • CGO is enabled (set CGO_ENABLED=1 if needed)
  • You have a C compiler installed (gcc, clang, or MSVC)
  • The Z3 headers are accessible

More Information

See the README.md in src/api/go for complete API documentation.

File: examples/python/tutorial/jupyter/README.md

Jupyter version of the Z3 Python Tutorial.

Thanks to Peter Gragert, the Z3 tutorial guide is now available in the Jupyter notebook format.

An online tutorial is available from https://github.com/philzook58/z3_tutorial

File: src/api/dotnet/README.md

Z3 Nuget Package

For more information see the Z3 github page

File: src/api/go/README.md

Z3 Go Bindings

This directory contains Go language bindings for the Z3 theorem prover.

Overview

The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support:

  • Core Z3 Types: Context, Config, Symbol, AST, Sort, Expr, FuncDecl
  • Solver Operations: Creating solvers, asserting constraints, checking satisfiability
  • Model Manipulation: Extracting and evaluating models
  • Boolean Logic: And, Or, Not, Implies, Iff, Xor
  • Arithmetic: Add, Sub, Mul, Div, Mod, comparison operators
  • Bit-vectors: Full bit-vector arithmetic, bitwise operations, shifts, comparisons
  • Floating Point: IEEE 754 floating-point arithmetic with rounding modes
  • Arrays: Select, Store, constant arrays
  • Sequences/Strings: String operations, concatenation, contains, indexing
  • Regular Expressions: Pattern matching, Kleene star/plus, regex operations
  • Quantifiers: Forall, Exists
  • Functions: Function declarations and applications
  • Tactics & Goals: Goal-based solving and tactic combinators
  • Probes: Goal property checking
  • Datatypes: Algebraic datatypes, tuples, enumerations, lists
  • Parameters: Solver and tactic configuration
  • Optimize: Optimization problems with maximize/minimize objectives

Building

Prerequisites

  • Go 1.20 or later
  • Z3 library built and installed
  • CGO enabled

With CMake

bash
mkdir build && cd build
cmake -DBUILD_GO_BINDINGS=ON ..
make

With Python Build System

bash
python scripts/mk_make.py --go
cd build
make

Usage

Basic Example

go
package main

import (
    "fmt"
    "github.com/Z3Prover/z3/src/api/go"
)

func main() {
    // Create a context
    ctx := z3.NewContext()
    
    // Create variables
    x := ctx.MkIntConst("x")
    y := ctx.MkIntConst("y")
    
    // Create constraints: x + y == 10 && x > y
    ten := ctx.MkInt(10, ctx.MkIntSort())
    eq := ctx.MkEq(ctx.MkAdd(x, y), ten)
    gt := ctx.MkGt(x, y)
    
    // Create solver and check
    solver := ctx.NewSolver()
    solver.Assert(eq)
    solver.Assert(gt)
    
    if solver.Check() == z3.Satisfiable {
        model := solver.Model()
        if xVal, ok := model.Eval(x, true); ok {
            fmt.Println("x =", xVal.String())
        }
        if yVal, ok := model.Eval(y, true); ok {
            fmt.Println("y =", yVal.String())
        }
    }
}

Running Examples

bash
cd examples/go

# Set library path (Linux/Mac)
export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I../../src/api"
export CGO_LDFLAGS="-L../../build -lz3"

# Set library path (Windows)
set PATH=..\..\build;%PATH%
set CGO_CFLAGS=-I../../src/api
set CGO_LDFLAGS=-L../../build -lz3

# Run example
go run basic_example.go

API Reference

Context

  • NewContext() - Create a new Z3 context
  • NewContextWithConfig(cfg *Config) - Create context with configuration
  • SetParam(key, value string) - Set context parameters

Creating Expressions

  • MkBoolConst(name string) - Create Boolean variable
  • MkIntConst(name string) - Create integer variable
  • MkRealConst(name string) - Create real variable
  • MkInt(value int, sort *Sort) - Create integer constant
  • MkReal(num, den int) - Create rational constant

Boolean Operations

  • MkAnd(exprs ...*Expr) - Conjunction
  • MkOr(exprs ...*Expr) - Disjunction
  • MkNot(expr *Expr) - Negation
  • MkImplies(lhs, rhs *Expr) - Implication
  • MkIff(lhs, rhs *Expr) - If-and-only-if
  • MkXor(lhs, rhs *Expr) - Exclusive or

Arithmetic Operations

  • MkAdd(exprs ...*Expr) - Addition
  • MkSub(exprs ...*Expr) - Subtraction
  • MkMul(exprs ...*Expr) - Multiplication
  • MkDiv(lhs, rhs *Expr) - Division
  • MkMod(lhs, rhs *Expr) - Modulo
  • MkRem(lhs, rhs *Expr) - Remainder

Comparison Operations

  • MkEq(lhs, rhs *Expr) - Equality
  • MkDistinct(exprs ...*Expr) - Distinct
  • MkLt(lhs, rhs *Expr) - Less than
  • MkLe(lhs, rhs *Expr) - Less than or equal
  • MkGt(lhs, rhs *Expr) - Greater than
  • MkGe(lhs, rhs *Expr) - Greater than or equal

Solver Operations

  • NewSolver() - Create a new solver
  • Assert(constraint *Expr) - Add constraint
  • Check() - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown)
  • Model() - Get model (if satisfiable)
  • Push() - Create backtracking point
  • Pop(n uint) - Remove backtracking points
  • Reset() - Remove all assertions

Model Operations

  • Eval(expr *Expr, modelCompletion bool) - Evaluate expression in model
  • NumConsts() - Number of constants in model
  • NumFuncs() - Number of functions in model
  • String() - Get string representation

Bit-vector Operations

  • MkBvSort(sz uint) - Create bit-vector sort
  • MkBVConst(name string, size uint) - Create bit-vector variable
  • MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr) - Arithmetic operations
  • MkBVAnd/Or/Xor/Not(...) - Bitwise operations
  • MkBVShl/LShr/AShr(lhs, rhs *Expr) - Shift operations
  • MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...) - Comparisons
  • MkConcat(lhs, rhs *Expr) - Bit-vector concatenation
  • MkExtract(high, low uint, expr *Expr) - Extract bits
  • MkSignExt/ZeroExt(i uint, expr *Expr) - Extend bit-vectors

Floating-Point Operations

  • MkFPSort(ebits, sbits uint) - Create floating-point sort
  • MkFPSort16/32/64/128() - Standard IEEE 754 sorts
  • MkFPInf/NaN/Zero(sort *Sort, ...) - Special values
  • MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr) - Arithmetic with rounding
  • MkFPNeg/Abs/Sqrt(...) - Unary operations
  • MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr) - Comparisons
  • MkFPIsNaN/IsInf/IsZero(expr *Expr) - Predicates

Sequence/String Operations

  • MkStringSort() - Create string sort
  • MkSeqSort(elemSort *Sort) - Create sequence sort
  • MkString(value string) - Create string constant
  • MkSeqConcat(exprs ...*Expr) - Concatenation
  • MkSeqLength(seq *Expr) - Length
  • MkSeqPrefix/Suffix/Contains(...) - Predicates
  • MkSeqAt(seq, index *Expr) - Element access
  • MkSeqExtract(seq, offset, length *Expr) - Substring
  • MkStrToInt/IntToStr(...) - Conversions

Regular Expression Operations

  • MkReSort(seqSort *Sort) - Create regex sort
  • MkToRe(seq *Expr) - Convert string to regex
  • MkInRe(seq, re *Expr) - String matches regex predicate
  • MkReStar(re *Expr) - Kleene star (zero or more)
  • MkRePlus(re *Expr) - Kleene plus (one or more)
  • MkReOption(re *Expr) - Optional (zero or one)
  • MkRePower(re *Expr, n uint) - Exactly n repetitions
  • MkReLoop(re *Expr, lo, hi uint) - Bounded repetition
  • MkReConcat(regexes ...*Expr) - Concatenation
  • MkReUnion(regexes ...*Expr) - Alternation (OR)
  • MkReIntersect(regexes ...*Expr) - Intersection
  • MkReComplement(re *Expr) - Complement
  • MkReDiff(a, b *Expr) - Difference
  • MkReEmpty/Full/Allchar(sort *Sort) - Special regexes
  • MkReRange(lo, hi *Expr) - Character range
  • MkSeqReplaceRe/ReAll(seq, re, replacement *Expr) - Regex replace

Datatype Operations

  • MkConstructor(name, recognizer string, ...) - Create constructor
  • MkDatatypeSort(name string, constructors []*Constructor) - Create datatype
  • MkDatatypeSorts(names []string, ...) - Mutually recursive datatypes
  • MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort) - Tuples
  • MkEnumSort(name string, enumNames []string) - Enumerations
  • MkListSort(name string, elemSort *Sort) - Lists

Tactic Operations

  • MkTactic(name string) - Create tactic by name
  • MkGoal(models, unsatCores, proofs bool) - Create goal
  • Apply(g *Goal) - Apply tactic to goal
  • AndThen(t2 *Tactic) - Sequential composition
  • OrElse(t2 *Tactic) - Try first, fallback to second
  • Repeat(max uint) - Repeat tactic
  • TacticWhen/Cond(...) - Conditional tactics

Probe Operations

  • MkProbe(name string) - Create probe by name
  • Apply(g *Goal) - Evaluate probe on goal
  • Lt/Gt/Le/Ge/Eq(p2 *Probe) - Probe comparisons
  • And/Or/Not(...) - Probe combinators

Parameter Operations

  • MkParams() - Create parameter set
  • SetBool/Uint/Double/Symbol(key string, value ...) - Set parameters

Optimize Operations

  • NewOptimize() - Create optimization context
  • Assert(constraint *Expr) - Add constraint
  • AssertSoft(constraint *Expr, weight, group string) - Add soft constraint
  • Maximize(expr *Expr) - Add maximization objective
  • Minimize(expr *Expr) - Add minimization objective
  • Check(assumptions ...*Expr) - Check and optimize
  • Model() - Get optimal model
  • GetLower/Upper(index uint) - Get objective bounds
  • Push/Pop() - Backtracking
  • Assertions/Objectives() - Get assertions and objectives
  • UnsatCore() - Get unsat core

Fixedpoint Operations (Datalog/CHC)

  • NewFixedpoint() - Create fixedpoint solver
  • RegisterRelation(funcDecl *FuncDecl) - Register predicate
  • AddRule(rule *Expr, name *Symbol) - Add Horn clause
  • AddFact(pred *FuncDecl, args []int) - Add table fact
  • Query(query *Expr) - Query constraints
  • QueryRelations(relations []*FuncDecl) - Query relations
  • GetAnswer() - Get satisfying instance or proof
  • Push/Pop() - Backtracking

Quantifier Operations

  • MkQuantifier(isForall bool, weight int, sorts, names, body, patterns) - Create quantifier
  • MkQuantifierConst(isForall bool, weight int, bound, body, patterns) - Create with bound vars
  • IsUniversal/IsExistential() - Check quantifier type
  • GetNumBound() - Number of bound variables
  • GetBoundName/Sort(idx int) - Get bound variable info
  • GetBody() - Get quantifier body
  • GetNumPatterns() - Number of patterns
  • GetPattern(idx int) - Get pattern

Lambda Operations

  • MkLambda(sorts, names, body) - Create lambda expression
  • MkLambdaConst(bound, body) - Create lambda with bound variables
  • GetNumBound() - Number of bound variables
  • GetBoundName/Sort(idx int) - Get bound variable info
  • GetBody() - Get lambda body

Type Variables

  • MkTypeVariable(name *Symbol) - Create polymorphic type variable sort

Logging

  • OpenLog(filename string) - Open interaction log
  • CloseLog() - Close log
  • AppendLog(s string) - Append to log
  • IsLogOpen() - Check if log is open

Memory Management

The Go bindings use runtime.SetFinalizer to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately. The bindings enable Z3_enable_concurrent_dec_ref when creating contexts so finalizer-driven decref operations are safe with concurrent GC.

Thread Safety

Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context.

License

Z3 is licensed under the MIT License. See LICENSE.txt in the repository root.

Contributing

Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository.

References

File: src/api/js/README.md

TypeScript Bindings

This directory contains JavaScript code to automatically derive TypeScript bindings for the C API, which are published on npm as z3-solver.

The readme for the bindings themselves is located in PUBLISHED_README.md.

Building

You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with emsdk. Newer versions of emscripten may break the build; you can find the version used in CI in this file.

Then run npm i to install dependencies, npm run build:ts to build the TypeScript wrapper, and npm run build:wasm to build the wasm artifact.

Build on your own

Consult the file build-wasm.ts for configurations used for building wasm.

Tests

Run npm test after building to run tests.

Explore Related Technologies & Topics

View All 9,111+ Repositories โ†’

Discover similar high-velocity repositories, agent skills, and OpenAPI specifications across the ecosystem.

โšก MCP Servers Model Context Protocol โ†’ ๐Ÿง  Agent Skills Prompt & rule files โ†’ ๐Ÿ”Œ OpenAPI Specs REST & Swagger schemas โ†’