Installing ocaml API for Z3 using opam

Question

I want to use Z3 in my OCaml program. Using opam, I did

$ opam install z3
$ eval $(opam env)

then tried compiling with

$ ocamlfind ocamlopt -o main -package z3 -linkpkg main.ml

What I get is a huge dump of thousands of In function foo undefined reference to bar, starting with

/home/andrepd/.opam/4.06.1+flambda/lib/z3/libz3-static.a(api_datatype.o): In function `mk_datatype_decl':
api_datatype.cpp:(.text+0x4bf): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x522): undefined reference to `__cxa_throw'
api_datatype.cpp:(.text+0x57b): undefined reference to `__cxa_free_exception'
api_datatype.cpp:(.text+0x58f): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x5f9): undefined reference to `__cxa_throw'
api_datatype.cpp:(.text+0x61f): undefined reference to `__cxa_allocate_exception'
api_datatype.cpp:(.text+0x68b): undefined reference to `__cxa_throw'
...

ending with

binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x1ab): undefined reference to `__cxa_allocate_exception'
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x205): undefined reference to `__cxa_throw'
binary_heap_upair_queue.cpp:(.text._ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_[_ZN2lp23binary_heap_upair_queueIjE7dequeueERjS2_]+0x226): undefined reference to `__cxa_free_exception'
/home/andrepd/.opam/4.06.1+flambda/lib/z3/libz3-static.a(binary_heap_upair_queue.o): In function `_GLOBAL__sub_I_binary_heap_upair_queue.cpp':
binary_heap_upair_queue.cpp:(.text.startup+0xc): undefined reference to `std::ios_base::Init::Init()'
binary_heap_upair_queue.cpp:(.text.startup+0x13): undefined reference to `std::ios_base::Init::~Init()'
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
Command exited with code 2.

What am I doing wrong? For the record, I was using ocamlbuild, with

$ ocamlbuild -use-ocamlfind -cflag '-linkpkg' main.native

and true: package(z3) in the _tags file. But calling plain ocamlfind like above gives the same output.

Versions: compiler: 4.06.1 w/ flambda, opam: 2.0.0, z3: 4.8.4.

Answer 1

TL;DR; The package is broken. The fix and a couple of workarounds are below, but in general, such questions should be posted to corresponding issue trackers. So consider opening an issue report or pull request with a fix.

Those linker errors indicate that the symbols from the C++ standard library are missing. Since OCaml is using the C linker to link the final product it is not passing the C++ standard library by default. Of course, a properly made package should do this for us¹, but we can still do it manually via the -cclib -lstdc++ (if you have libstdc++, otherwise use -lc++).

ocamlfind ocamlopt -linkpkg -cclib -lstdc++ -package z3 example.ml -o exe

With ocamlbuild you can use the cclib(x) parametrized tag, e.g.,

 <example.ml>: cclib(-lstdc++)

---

¹ the provided META file contains a bogus

linkopts = "-cclib -L/usr/lib"

which (a) doesn't make sense since -L is not a linker option, but the compiler one, and (b) is useless, as /usr/lib is usually in the search path anyway.

The correct option should be:

linkopts = "-cclib -lstdc++"

You might edit the file directly, it is located at $(ocamlfind query z3)/META.

Please, consider submitting a fix either to OPAM package or (ideally) to z3.