Z3 for Java

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 unstable branch. 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

CodePlex requires git 1.7.10 or later to avoid HTTPS cloning errors. If we get a cloning error, we should use the instructions found here.

Next, we have to checkout the z3-java tag. This tag “points” to a fairly stable commit in the unstable branch.

cd z3
git checkout z3-java

Next, we generate the Z3 make file with the option --java.

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 examples/java/JavaExample.java using:

• 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)