Install Z3 in Windows

Question

I did download the file Z3 4.3.0 for Windows (64 bits) that is on site: http://z3.codeplex.com/releases.

When I try to run the file z3.exe which is in the bin folder. Prompt appears and disappears immediately. I needed to know how to run a file written in z3 through z3.exe file.

How can I do this? Or what is the best option to run z3 through Java?

Answer 1

z3.exe is a command line tool. To execute a SMT-LIB 2.0 file called file.smt2, you should execute the following command in the Command Prompt.

 z3 file.smt2

If the directory containing z3.exe is not in your PATH environment variable, you will have to include the directory in the command above.

BTW, Z3 has not graphical user interface or environment. It is essentially a library for automated reasoning. z3.exe is a simple executable built using this library that allows us execute commands stored in a file.

You can also play with Z3 using the web interface available at rise4fun. At rise4fun, we have a SMT-LIB front-end, and a Python based one. Both of them have interactive tutorials.

Here are some useful resources to learn about SMT:

• Z3 tutorial
• Tutorial on SMT-LIB
• Article describing SMT applications
• SMT-Lib benchmarks
• Stackoverflow: you can search Z3 related question by including [z3] in the search box.

Z3 has APIs for several programming languages: C, C++, .Net, Python and OCaml. In the next release, we will also provide support for Java. You can already play with the Java by using one of the nightly builds. Go here for more information about Z3 nightly builds. The nightly builds contain a Java example application using the Z3 API.