problem: cannot find z3
kumori123 opened this issue · 2 comments
Hi，thank you for your great Kind2.
I met a problem. although I install z3-solver through opam, however kind2 executable files cannot find z3-solver.
Thank you for your suggestion!
Hi, what version of the z3 opam package did you install? You can run opam list -i z3 to check it out.
I just installed the latest version available (4.11.2). As expected, the binary was installed in ~/.opam/4.14.0/bin/z3 where 4.14.0 is the version of my OCaml compiler. If you allowed opam init to modify your ~/.profile, the binary should be available in your PATH and Kind 2 should be able to find it. Otherwise, you need to run eval $(opam env). After the first setup with opam init, I recommend to close your session, and login again so that any new shell you open uses the configuration in ~/.profile.
Alternatively, you can tell Kind 2 where to find a z3 binary by passing the option --z3_bin /path/to/z3
The problem is resolved.
Thank you for your suggestions!