Installation

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.

Method 1: CMake (Recommended)

Clone Z3 Repository

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

Configure with CMake

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

Add -DCMAKE_BUILD_TYPE=Release for optimized builds.

Build Z3

make -j$(nproc)

cmake --build . --config Release

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

Clone and Configure

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

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

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

sudo make install
# Usually installs to /usr/local/lib

cmake --build . --target install
# Installs to C:\Program Files\z3

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

undefined reference to Z3_* errors

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

z3.h: No such file or directory

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

cannot find package

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

shared library error at runtime

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

CGO not enabled

Problem: CGO is disabled.Solution:

export CGO_ENABLED=1
go env -w CGO_ENABLED=1

Build fails on macOS

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

Linux
macOS
Windows

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

Requires XCode command line tools:

xcode-select --install
brew install cmake

Apple Silicon (M1/M2) works but ensure you’re using native Go:

go env GOARCH  # Should show arm64

Requires Visual Studio or MinGW:Visual Studio (Recommended):

Install Visual Studio 2019 or later
Include “Desktop development with C++”
Use “x64 Native Tools Command Prompt”

MinGW:

# Install via MSYS2
pacman -S mingw-w64-x86_64-gcc cmake

Next Steps

Getting Started

Learn the basics with examples

API Reference

Complete API documentation

Examples

Example programs on GitHub

Build Guide

Detailed build instructions

Python

C++

C

Java

.NET

JavaScript/TypeScript

Go

OCaml

Requirements

Go

Build Tools

Build Z3 with Go Bindings

Method 1: CMake (Recommended)

Method 2: Python Build System

Set Up Go Environment

Linux / macOS

macOS Specific

Windows

Using Go Modules

go.mod

Using in Your Code

Verification

Installation Options

System-Wide Installation

Static Linking

Troubleshooting

Docker Setup

Platform-Specific Notes

Next Steps

Getting Started

API Reference

Examples

Build Guide

​Requirements

Go

Build Tools

​Build Z3 with Go Bindings

​Method 1: CMake (Recommended)

​Method 2: Python Build System

​Set Up Go Environment

​Linux / macOS

​macOS Specific

​Windows

​Using Go Modules

​go.mod

​Using in Your Code

​Verification

​Installation Options

​System-Wide Installation

​Static Linking

​Troubleshooting

​Docker Setup

​Platform-Specific Notes

​Next Steps

Getting Started

API Reference

Examples

Build Guide

Requirements

Build Z3 with Go Bindings

Method 1: CMake (Recommended)

Method 2: Python Build System

Set Up Go Environment

Linux / macOS

macOS Specific

Windows

Using Go Modules

go.mod

Using in Your Code

Verification

Installation Options

System-Wide Installation

Static Linking

Troubleshooting

Docker Setup

Platform-Specific Notes

Next Steps