Installation

The Z3 OCaml bindings provide access to Z3’s SMT solving capabilities from OCaml. The bindings support both static and dynamic linking and work with all OCaml linkers.

Requirements

OCaml

OCaml 4.09.0 or later
ocamlfind (findlib)
opam (recommended)

Build Tools

C/C++ compiler
Python 3.x or CMake
Git

Installation Methods

Method 1: Build from Source (Recommended)

Build Z3 with OCaml bindings from source.

Clone Z3 Repository

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

Build with Python

python scripts/mk_make.py --ml --staticlib
cd build
make -j$(nproc)

The --staticlib flag creates a static library, making binaries self-contained.

Install with ocamlfind

ocamlfind install z3 build/api/ml/* build/libz3-static.a

This installs:

OCaml modules: z3.cmi, z3.cmo, z3.cmx, etc.
Static library: libz3-static.a
Libraries: z3ml.{a,cma,cmxa,cmxs}

Method 2: OPAM (When Available)

The Z3 OCaml package availability in OPAM may vary. Check the opam repository for the latest version.

opam install z3

If the package is not available or outdated, use Method 1.

Build Artifacts

The build process creates several files:

OCaml Modules

files

Core Z3 module with type definitions and main API

files

Z3 enumeration types

files

Native bindings to Z3 C API

Libraries

library

Native code static library for ocamlopt

library

Bytecode library for ocamlc

library

Standalone shared library for dynamic loading with Dynlink

library

C stubs archive

library

Shared object for OCaml runtime (bytecode)

library

Z3 library itself (when using --staticlib)

Compiling OCaml Programs

Using ocamlfind (Recommended)

The easiest way to compile programs using Z3:

ocamlfind ocamlc -thread -package z3 -linkpkg program.ml -o program

ocamlfind ocamlopt -thread -package z3 -linkpkg program.ml -o program

The -thread flag is required for the Z3 bindings.

Static Linking

With --staticlib, native binaries have no Z3 dependency:

ocamlfind ocamlopt -thread -package z3 -linkpkg program.ml -o program
ldd ./program
# Shows only system libraries, no libz3.so

Custom Bytecode (Self-Contained)

Create a portable bytecode executable:

ocamlfind ocamlc -custom -thread -package z3 -linkpkg program.ml -o program

The resulting binary is self-contained (no DLL dependencies).

Manual Compilation

Without ocamlfind:

ocamlc -thread -I +threads -I $(ocamlfind query z3) \
  unix.cma threads.cma z3ml.cma program.ml -o program

ocamlopt -thread -I +threads -I $(ocamlfind query z3) \
  unix.cmxa threads.cmxa z3ml.cmxa program.ml -o program

Using in OCaml Toplevel

Load Z3 in the OCaml REPL:

$ ocaml
        OCaml version 4.14.0

# #use "topfind";;
# #require "z3";;
# open Z3;;
# let ctx = Z3.mk_context [];;  
val ctx : Z3.context = <abstr>

OCaml Scripts

Create executable OCaml scripts:

script.ml

#!/usr/bin/env ocaml
#use "topfind";;
#require "z3";;

open Z3

let () =
  let ctx = mk_context [] in
  (* Your Z3 code here *)
  Printf.printf "Z3 version: %s\n" Version.to_string

Make it executable:

chmod +x script.ml
./script.ml

Dynamic Loading with Dynlink

The z3ml.cmxs file can be dynamically loaded:

Dynlink.loadfile "z3ml.cmxs";;
open Z3;;

This is useful for plugins and dynamic code loading.

Verification

Test your installation:

test.ml

open Z3
open Z3.Arithmetic
open Z3.Boolean
open Z3.Solver

let () =
  Printf.printf "Z3 OCaml Bindings Test\n";
  Printf.printf "Z3 Version: %s\n\n" Version.to_string;
  
  let ctx = mk_context [] in
  let x = Integer.mk_const_s ctx "x" in
  let zero = Integer.mk_numeral_i ctx 0 in
  let constraint_ = mk_gt ctx x zero in
  
  let solver = mk_solver ctx None in
  Solver.add solver [constraint_];
  
  match check solver [] with
  | SATISFIABLE ->
      Printf.printf "Installation successful!\n";
      (match get_model solver with
       | Some model -> 
           Printf.printf "Model: %s\n" (Model.to_string model)
       | None -> ())
  | _ -> Printf.printf "Unexpected result\n"

Compile and run:

ocamlfind ocamlopt -thread -package z3 -linkpkg test.ml -o test
./test

Expected output:

Z3 OCaml Bindings Test
Z3 Version: 4.x.x

Installation successful!
Model: x -> 1

Platform-Specific Notes

Linux
macOS
Windows

Most distributions work out of the box:

# Ubuntu/Debian
sudo apt-get install ocaml ocaml-findlib opam

# Fedora
sudo dnf install ocaml ocaml-findlib opam

# Arch
sudo pacman -S ocaml ocaml-findlib opam

If using dynamic linking, ensure library path is set:

export LD_LIBRARY_PATH=/path/to/z3/build:$LD_LIBRARY_PATH

Install via Homebrew:

brew install ocaml opam
opam init
eval $(opam env)

Use DYLD_LIBRARY_PATH for dynamic linking:

export DYLD_LIBRARY_PATH=/path/to/z3/build:$DYLD_LIBRARY_PATH

Z3 OCaml bindings assume the win32 or win64 OCaml port (using MSVC), not Cygwin or MinGW.Install OCaml for Windows:

Download from OCaml for Windows
Or use DkML

The build uses cl (MSVC) as the C compiler.

Troubleshooting

Cannot find package z3

Problem: ocamlfind can’t locate Z3.Solution:

Verify installation: ocamlfind query z3
Reinstall: ocamlfind remove z3 then reinstall
Check OPAM switch: opam switch

Linking errors

Problem: Undefined references to Z3 symbols.Solution:

Ensure -thread flag is used
With dynamic linking, set LD_LIBRARY_PATH
Use --staticlib when building for self-contained binaries

DLL not found (bytecode)

Problem: dllz3ml.so not found when running bytecode.Solution:

Install properly with ocamlfind (it handles stublibs)
Or use -custom flag for self-contained bytecode
Check: ocamlfind query -format '%d/stublibs' z3

Version mismatch

Problem: OCaml module compiled with different Z3 version.Solution:

Rebuild Z3 from source
Clean build directory: make clean before rebuilding
Reinstall with ocamlfind

Advanced: Manual Installation Paths

If not using ocamlfind:

# Install to custom location
INSTALL_DIR="/opt/z3-ml"
mkdir -p $INSTALL_DIR
cp build/api/ml/*.{cmi,cmo,cmx,o,mli} $INSTALL_DIR/
cp build/api/ml/*.{a,cma,cmxa,cmxs} $INSTALL_DIR/
cp build/api/ml/*.so $INSTALL_DIR/
cp build/libz3-static.a $INSTALL_DIR/

# Compile with custom path
ocamlopt -thread -I +threads -I $INSTALL_DIR \
  unix.cmxa threads.cmxa z3ml.cmxa program.ml -o program

Docker Setup

Use Docker for isolated environment:

Dockerfile

FROM ocaml/opam:ubuntu-22.04-ocaml-4.14

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

# Build Z3
RUN git clone https://github.com/Z3Prover/z3.git /home/opam/z3 && \
    cd /home/opam/z3 && \
    python3 scripts/mk_make.py --ml --staticlib && \
    cd build && \
    make -j$(nproc)

# Install OCaml bindings
RUN cd /home/opam/z3 && \
    ocamlfind install z3 build/api/ml/* build/libz3-static.a

WORKDIR /home/opam/app

Next Steps

Getting Started

Learn the basics with examples

Examples

Example programs on GitHub

API Documentation

OCaml API reference

Build Instructions

Detailed build guide

Python

C++

C

Java

.NET

JavaScript/TypeScript

Go

OCaml

Requirements

OCaml

Build Tools

Installation Methods

Method 1: Build from Source (Recommended)

Method 2: OPAM (When Available)

Build Artifacts

OCaml Modules

Libraries

Compiling OCaml Programs

Using ocamlfind (Recommended)

Static Linking

Custom Bytecode (Self-Contained)

Manual Compilation

Using in OCaml Toplevel

OCaml Scripts

Dynamic Loading with Dynlink

Verification

Platform-Specific Notes

Troubleshooting

Advanced: Manual Installation Paths

Docker Setup

Next Steps

Getting Started

Examples

API Documentation

Build Instructions

​Requirements

OCaml

Build Tools

​Installation Methods

​Method 1: Build from Source (Recommended)

​Method 2: OPAM (When Available)

​Build Artifacts

​OCaml Modules

​Libraries

​Compiling OCaml Programs

​Using ocamlfind (Recommended)

​Static Linking

​Custom Bytecode (Self-Contained)

​Manual Compilation

​Using in OCaml Toplevel

​OCaml Scripts

​Dynamic Loading with Dynlink

​Verification

​Platform-Specific Notes

​Troubleshooting

​Advanced: Manual Installation Paths

​Docker Setup

​Next Steps

Getting Started

Examples

API Documentation

Build Instructions

Requirements

Installation Methods

Method 1: Build from Source (Recommended)

Method 2: OPAM (When Available)

Build Artifacts

OCaml Modules

Libraries

Compiling OCaml Programs

Using ocamlfind (Recommended)

Static Linking

Custom Bytecode (Self-Contained)

Manual Compilation

Using in OCaml Toplevel

OCaml Scripts

Dynamic Loading with Dynlink

Verification

Platform-Specific Notes

Troubleshooting

Advanced: Manual Installation Paths

Docker Setup

Next Steps