How to run Z3 under Linux or Mac OS X?

This is a method to use the SMT solver Z3 in a non-Windows environment (Linux, Mac OS X, ...). It has been tested on Ubuntu (version 8.04) and Mac OS X (version 10.5). For additions, corrections or suggestions, please contact me.

1. Install Wine

Wine (version 1.0 or higher) may already be included in your distribution. Otherwise, there are the following locations to obtain Wine from:

Wine for major Linux/BSD distributions: http://www.winehq.org/site/download
Wine on Mac OS X: http://www.kronenberg.org/darwine/ (note that you might need to install TRiX which is shipped with Darwine), comprehensive overview: http://wiki.winehq.org/MacOSX

2. Install Z3

Download the Z3 installer from http://research.microsoft.com/projects/Z3/ (version 2.3 has been tested to work).

On Mac OS X, install Z3 by just clicking on the downloaded application. In other systems run the following command in a shell (where "Z3.msi" has to be substituted with the name of the downloaded installer):

wine msiexec /i Z3.msi

Afterwards, download "winetricks" from http://code.google.com/p/winezeug/ and run:

winetricks vcrun2008

3. Run Z3

To conveniently run Z3, use this shell script for Linux or 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

Please note that Z3 cannot check files given with absolute paths, because Z3's options already start with a forward slash.

Last updated: 1.12.2009