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. If the package is not available or outdated, use Method 1.
Build Artifacts The build process creates several files:
OCaml Modules Core Z3 module with type definitions and main API
z3enums.{cmi,cmo,cmx,o,mli}
Z3 enumeration types
z3native.{cmi,cmo,cmx,o,mli}
Native bindings to Z3 C API
Libraries Native code static library for ocamlopt
Bytecode library for ocamlc
Standalone shared library for dynamic loading with Dynlink
Shared object for OCaml runtime (bytecode)
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
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
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:
#!/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:
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
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: The build uses cl (MSVC) as the C compiler. Troubleshooting
Problem : ocamlfind can’t locate Z3.Solution :
Verify installation: ocamlfind query z3
Reinstall: ocamlfind remove z3 then reinstall
Check OPAM switch: opam switch
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
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
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:
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
