Z3 now provides support for Java.
The new Java bindings are based on the .Net bindings developed by Christoph Wintersteiger.
They will be included in the next official release. In the meantime, we can already try them using the
Please try the new Java bindings and submit problems and bugs.
Here are the instructions to build the Z3 Java bindings.
First, we have to clone the
unstable branch from codeplex.
git clone https://git01.codeplex.com/z3 -b unstable
Next, we have to checkout the
z3-java tag. This tag "points" to a fairly stable commit in the
cd z3 git checkout z3-java
Next, we generate the Z3 make file with the option
python scripts/mk_make.py --java
Now, we build Z3 and the example applications.
cd build make all examples
That is it. Now, we can execute the example located at
java -cp com.microsoft.z3.jar;. JavaExample (on Windows)
LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample (on Linux and FreeBSD)
java -cp com.microsoft.z3.jar:. JavaExample (on OSX)