How to run Z3 under Mac OS X?

Z3 3.2.1 has been made available for Mac OS X. The remainder of this page is kept for historical reasons.

This is a method to use the SMT solver Z3 under Mac OS X. It has been tested on Mac OS X (version 10.5). For additions, corrections or suggestions, please contact me.

1. Install Wine

Download Wine for Mac OS X from http://winebottler.kronenberg.org/ and install it.

2. Install Z3

Download the Z3 installer from http://research.microsoft.com/projects/Z3/ and install Z3 by clicking on the downloaded application.

3. Run Z3

To conveniently run Z3, use this shell script for Mac OS X. Note that the script may need some modification; especially compare the path to Z3 as given in the script file with the location Z3 was installed to. To make the script executable, run the following command in the directory of the shell script:

chmod a+x z3

To test that the setup works, run the following command in the directory of the shell script:

./z3 -version

4. Use Z3 within Isabelle

To use Z3 within Isabelle, download this tarball and unpack it into Isabelle's contrib directory. Replace the file z3 in the subdirectory z3/x86-darwin with the one modified in step 3. Additionally, add a line to Isabelle's user-defined components lists (e.g., in $ISABELLE_HOME_USER/etc/components) reading as follows:

ISABELLE_HOME/contrib/z3

where ISABELLE_HOME should be replaced by the path stored in the shell variable $ISABELLE_HOME. This path can be obtained via the following command:

isabelle getenv ISABELLE_HOME

Finally, to enable Z3 with Isabelle and to confirm non-commercial usage of Z3, add a line to Isabelle's user-defined settings (e.g., in $ISABELLE_HOME_USER/etc/settings) reading as follows:

Z3_NON_COMMERCIAL=yes