Skip to content

configuringZ3

Neil Walkinshaw edited this page Jul 10, 2018 · 2 revisions

Configuring Z3

A couple of functions within Mint involve the use of constraint solvers. For this work we use the Z3 constraint solver. Since most constraint solvers use native libraries, it can be a bit messy to set up.

Please follow the the instructions here to install it for your system:

http://leodemoura.github.io/blog/2012/12/10/z3-for-java.html

Important note - Since Z3 has moved from CodePlex to Github, you need to replace the git command in these instructions as follows:

git clone https://github.com/Z3Prover/z3.git -b unstable

Having followed the rest of the instructions, you ought to have a dynamic linked library (.so in *nix, .dll in Windows, .dylib in MacOS). You need to add this to the Java runtime path for native libraries.

Now you should be able to run the executable jar file.

Clone this wiki locally