Search code examples
installationocamlz3

Installing Z3 with OCaml bindings

I'm trying to install Z3 with OCaml bindings and getting the following error.

cp ../src/api/ml/z3.mli api/ml/z3.mli
ocamlc  -I api/ml -o api/ml/z3.cmi -c api/ml/z3.mli
File "api/ml/z3.mli", line 1159, characters 35-50:
Error: Unbound module Big_int
make: *** [api/ml/z3.cmo] Error 2

I firstly tried installing via

opam install z3

And then I tried cloning the Z3 repo and running

 python scripts/mk_make.py --ml
 cd build
 make

After which I get the same error.

Any help would be greatly appreciated. Thank you!

Solution

  • The Z3 installation is expecting an older OCaml environment. In recent OCaml releases, Big_int is in the Num module.

    $ opam install num

    For what it's worth, I don't believe there is an OPAM module for Z3. If you run the Z3 install, the OCaml/Z3 interface gets installed as if it was an OPAM module (in ~/.opam). But it's not really.

    I'm using Z3 every day, so I can verify that it works (both OCaml 4.03.0 and OCaml 4.06.0.)

    Update

    I just now verified that there is a Z3 package in OPAM these days, and I was able to install it under OCaml 4.06.0 on a previously clean system that I happen to have handy. The system is Ubuntu 14.04.

    I needed to do the following initial installations:

    sudo apt-get update
sudo apt-get install ocaml
sudo apt-get install m4
sudo apt-get install dev-libgmp
sudo apt-get install g++

    Then I installed OPAM:

    sudo add-apt-repository ppa:avsm/ppa
sudo apt-get update
sudo apt-get install opam

    Now running as myself:

    $ opam init
$ eval `opam config env`
$ opam update
$ opam switch 4.06.0
$ eval `opam config env`
$ opam install z3
$ ls ~/.opam/4.06.0/lib/z3
dllz3ml.so   z3.cmi       z3enums.cmx  z3ml.cmxa     z3native.cmx
libz3ml.a    z3.cmo       z3enums.mli  z3ml.cmxs     z3native.mli
libz3.so     z3.cmx       z3enums.o    z3.mli        z3native.o
META         z3enums.cmi  z3ml.a       z3native.cmi  z3native_stubs.o
opam.config  z3enums.cmo  z3ml.cma     z3native.cmo  z3.o

    This looks good to me. I'm not a Z3 wizard; it's mostly just a dependency of a project I'm working on. But these are the files I'm used to seeing.