# 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.

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.

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

Now, we build Z3 and the example applications.

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)