Z3 is installed on system but get error "Failure("Z3 not installed")"

[Shawdox]

What I ran:

sudo apt install z3
z3
# Z3 [version 4.8.7 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.
# Usage: z3 [options] [-file:]file
owi conc test.wat

What I got:

owi: internal error, uncaught exception:
     Failure("Z3 not installed")

I'm a beginner in OCaml, is there something I'm getting wrong?

[filipeom]

I believe the version of Z3 available through apt is not compiled with OCaml bindings. Therefore, you should install Z3 through the opam package manager. For example:

opam install z3

[Shawdox]

Hi, thanks for the help. I tried to use this opam install z3 and recompiled the whole project, but still got the samle problem.

opam install z3
opam install . --deps-only
dune clean
dune build -p owi @install
dune install

[zapashcanon]

You should rebuild and reinstall smtml after installing Z3. (We changed a lot of things recently in smtml so things are a little bit unstable, sorry!)

[filipeom]

You should rebuild and reinstall smtml after installing Z3. (We changed a lot of things recently in smtml so things are a little bit unstable, sorry!)

You can try to do this:

opam install z3 # skip if you already have done this 
opam update && opam install smtml.0.2.0
dune build -p owi @install
dune install

If you get issues saying the version of smtml is not available consider updating opam repository to the git version:

opam repository remove default --all-switches
opam repository add default https://github.com/ocaml/opam-repository.git --all-switches --set-default
opam update && opam install smtml.0.2.0

[Shawdox]

Thanks! I tried to run all these commands but the issue is still unchanged. It's so weird. Do you have any suggestion how to identity the root cause?

[filipeom]

Thanks! I tried to run all these commands but the issue is still unchanged. It's so weird. Do you have any suggestion how to identity the root cause?

Maybe you're opam switch is out of sync? Could you post the outputs of opam switch? And maybe even opam list just to see if the packages are correctly installed in your switch?

[Shawdox]

Thanks! I tried to run all these commands but the issue is still unchanged. It's so weird. Do you have any suggestion how to identity the root cause?

Maybe you're opam switch is out of sync? Could you post the outputs of opam switch? And maybe even opam list just to see if the packages are correctly installed in your switch?

That is the point. I just repull the repo and recomplie it, and the problem is solved.

[zapashcanon]

I'm reopening because we should give some advice in the README about installing at least one solver (Z3 or Bitwuzla currently) if the user is interested in symbolic execution.

[krtab]

We should wait for https://github.com/formalsec/smtml/pull/165 to be merged and released to opam to check that everything works smoothly.