Skip to main content
The Z3 Go bindings provide a comprehensive interface to Z3’s C API using CGO. The bindings are included in the Z3 source repository and must be built from source.

​
Requirements

Go

  • Go 1.20 or later
  • CGO enabled (default)

Build Tools

  • C/C++ compiler (gcc, clang, or MSVC)
  • CMake 3.4+ or Python 3.x
  • Git

​
Build Z3 with Go Bindings

The Go bindings must be built as part of the Z3 library.
1

Clone Z3 Repository

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

Configure with CMake

mkdir build && cd build
cmake -DBUILD_GO_BINDINGS=ON ..
Add -DCMAKE_BUILD_TYPE=Release for optimized builds.
3

Build Z3

make -j$(nproc)
4

Verify Build

The build creates:
  • libz3.so / libz3.dylib / z3.dll - Z3 shared library
  • Go bindings in src/api/go/
ls -la build/libz3.*
ls -la src/api/go/

​
Method 2: Python Build System

1

Clone and Configure

git clone https://github.com/Z3Prover/z3.git
cd z3
python scripts/mk_make.py --go
2

Build

cd build
make -j$(nproc)

​
Set Up Go Environment

After building Z3, configure your Go environment to use the bindings.

​
Linux / macOS

export LD_LIBRARY_PATH=/path/to/z3/build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I/path/to/z3/src/api"
export CGO_LDFLAGS="-L/path/to/z3/build -lz3"
Add to ~/.bashrc or ~/.zshrc for permanent configuration:
~/.bashrc
# Z3 Go bindings
export Z3_ROOT="$HOME/z3"
export LD_LIBRARY_PATH="$Z3_ROOT/build:$LD_LIBRARY_PATH"
export CGO_CFLAGS="-I$Z3_ROOT/src/api"
export CGO_LDFLAGS="-L$Z3_ROOT/build -lz3"

​
macOS Specific

On macOS, use DYLD_LIBRARY_PATH instead: 
export DYLD_LIBRARY_PATH=/path/to/z3/build:$DYLD_LIBRARY_PATH
export CGO_CFLAGS="-I/path/to/z3/src/api"
export CGO_LDFLAGS="-L/path/to/z3/build -lz3"

​
Windows

set PATH=C:\path\to\z3\build\Release;%PATH%
set CGO_CFLAGS=-IC:\path\to\z3\src\api
set CGO_LDFLAGS=-LC:\path\to\z3\build\Release -lz3
For PowerShell: 
$env:Path = "C:\path\to\z3\build\Release;" + $env:Path
$env:CGO_CFLAGS = "-IC:\path\to\z3\src\api"
$env:CGO_LDFLAGS = "-LC:\path\to\z3\build\Release -lz3"

​
Using Go Modules

The Z3 Go bindings use Go modules. Your project should reference the Z3 repository:

​
go.mod

go.mod
module myproject

go 1.20

require github.com/Z3Prover/z3/src/api/go v0.0.0

replace github.com/Z3Prover/z3/src/api/go => /path/to/z3/src/api/go
The replace directive points to your local Z3 build since the Go bindings are not published to a Go module registry.

​
Using in Your Code

main.go
package main

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

func main() {
    ctx := z3.NewContext()
    x := ctx.MkIntConst("x")
    fmt.Println("Created Z3 context and variable:", x.String())
}

​
Verification

Test your installation:
test.go
package main

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

func main() {
    // Create context
    ctx := z3.NewContext()
    fmt.Println("Z3 Go bindings installed successfully!")
    
    // Simple test
    x := ctx.MkIntConst("x")
    zero := ctx.MkInt(0, ctx.MkIntSort())
    constraint := ctx.MkGt(x, zero)
    
    solver := ctx.NewSolver()
    solver.Assert(constraint)
    
    if solver.Check() == z3.Satisfiable {
        fmt.Println("✓ Solver working correctly")
        model := solver.Model()
        if val, ok := model.Eval(x, true); ok {
            fmt.Println("✓ Model evaluation working:", val.String())
        }
    }
}
Run it: 
go run test.go
Expected output: 
Z3 Go bindings installed successfully!
✓ Solver working correctly
✓ Model evaluation working: 1

​
Installation Options

​
System-Wide Installation

To install Z3 system-wide: 
sudo make install
# Usually installs to /usr/local/lib
sudo ldconfig
After system installation, you may not need LD_LIBRARY_PATH: 
export CGO_CFLAGS="-I/usr/local/include"
export CGO_LDFLAGS="-lz3"

​
Static Linking

For static linking, build Z3 as a static library: 
cmake -DBUILD_GO_BINDINGS=ON -DBUILD_LIBZ3_SHARED=OFF ..
make
Then link statically: 
export CGO_LDFLAGS="-L/path/to/z3/build -lz3 -lstdc++ -lpthread -lm"

​
Troubleshooting

Problem: Linker can’t find Z3 library.Solution:
  • Verify CGO_LDFLAGS includes -L/path/to/build -lz3
  • Check that libz3.so exists in the build directory
  • On Linux: Run sudo ldconfig after system install
  • On Windows: Ensure z3.dll is in PATH
Problem: Compiler can’t find Z3 headers.Solution:
  • Verify CGO_CFLAGS includes -I/path/to/z3/src/api
  • Check that z3.h exists in src/api/z3.h
Problem: Go can’t find the Z3 package.Solution:
  • Check your go.mod has the correct replace directive
  • Verify the path points to z3/src/api/go (not just z3)
  • Run go mod tidy
Problem: error while loading shared libraries: libz3.soSolution:
  • Set LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS)
  • Or install Z3 system-wide and run ldconfig
  • On Windows: Ensure directory with z3.dll is in PATH
Problem: CGO is disabled.Solution:
export CGO_ENABLED=1
go env -w CGO_ENABLED=1
Problem: XCode command line tools or compiler missing.Solution:
xcode-select --install
brew install cmake

​
Docker Setup

Use Docker for isolated development:
Dockerfile
FROM golang:1.21

# Install build dependencies
RUN apt-get update && apt-get install -y \
    build-essential \
    cmake \
    git

# Build Z3
RUN git clone https://github.com/Z3Prover/z3.git /z3 && \
    cd /z3 && \
    mkdir build && \
    cd build && \
    cmake -DBUILD_GO_BINDINGS=ON .. && \
    make -j$(nproc)

# Set environment
ENV LD_LIBRARY_PATH=/z3/build:$LD_LIBRARY_PATH
ENV CGO_CFLAGS="-I/z3/src/api"
ENV CGO_LDFLAGS="-L/z3/build -lz3"

WORKDIR /app

​
Platform-Specific Notes

Most Linux distributions work out of the box with gcc/g++.Install dependencies:
# Ubuntu/Debian
sudo apt-get install build-essential cmake git

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

# Arch
sudo pacman -S base-devel cmake git

​
Next Steps

Getting Started

Learn the basics with examples

API Reference

Complete API documentation

Examples

Example programs on GitHub

Build Guide

Detailed build instructions