Crash when running example.ml (Ocaml)

[bleepbloopsify]

I currently have z3.4.8.11 installed, and when running the example, I get this error:

libc++abi: terminating with uncaught exception of type is_non_propositional_predicate::found

We are building with dune:

(executable
 (name example)
 (libraries z3))

and running using

dune exec ./example.exe

the directory looks like this:

dune
example.ml

where example.ml is this file: https://github.com/Z3Prover/z3/blob/master/examples/ml/ml_example.ml

Note:
I am on macOS Big Sur (11.5.2)

[NikolajBjorner]

I can't address bugs in downstream versions of z3

[k4rtik]

Hi @NikolajBjorner

I tried the OCaml example using the latest Z3 and get the same error:

$ ocamlfind ocamlopt -o example -thread -package Z3 -linkpkg example.ml
ld: warning: directory not found for option '-L/opt/local/lib'
$ ./example
libc++abi: terminating with uncaught exception of type is_non_propositional_predicate::found
Abort trap: 6
$ z3 --version
Z3 version 4.8.13 - 64 bit

Do you think the ld warning is worth investigating?

[k4rtik]

For reference, I built z3 this way, following the build and install instructions in the opam file for 4.8.11 by @c-cube:

$ python scripts/mk_make.py --ml --staticlib
$ cd build; make -j8
$ ocamlfind install  z3 api/ml/* libz3-static.a
[...]
ocamlfind: [WARNING] You have installed DLLs but the directory /Users/kartik/.opam/4.12.0/lib/stublibs is not mentioned in ld.conf
[...]
$ cp z3 /Users/kartik/.opam/4.12.0/bin/

There was an issue earlier with libstdc++.so which @ivg had resolved, so I am cc'ing him in this conversation.

[ivg]

Do you think the ld warning is worth investigating?

To my opinion it is irrelevant. It is just saying that there was no such folder. The package is linked statically, and there are no extra dependencies, and it loads without any linker errors, so it looks good to me.

And the message is likely coming from the C++ to C boundary from an escaping exception. Have you tried this example on a Linux machine?

[ivg]

For your information, I tried this on a Linux machine and an old version of z3 (4.8.9) and the example works perfectly fine.

[k4rtik]

I will try on Linux later today, but this is certainly an issue on Mac as reported by OP and confirmed with my report.

[k4rtik]

So I may be doing something really stupid, but I can't seem to get ocamlfind to recognize that z3 is installed (using 'opam install') on Linux:

$ ocamlfind ocamlopt -o ml_example -thread -package Z3 -linkpkg ml_example.ml
ocamlfind: Package `Z3' not found

opam list says:

[...]
z3                    4.8.11      Z3 solver
[...]

[aytey]

Z3 vs. z3?

[k4rtik]

Wow, indeed that fixed it on Linux, but the official example at https://github.com/Z3Prover/z3/blob/master/examples/ml/README does have what I wrote above. While both -package Z3 and -package z3 works fine on macOS (except for the crash reported above).

Perhaps, the example doc needs to be fixed.

@ivg answered it here: https://stackoverflow.com/a/50004273/1167061