Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.
If you are not familiar with Z3, you can start here.
Pre-built binaries for releases are available from here, and nightly builds from here.
Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.
See the release notes for notes on various stable releases of Z3.
| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | macOS | TravisCI |
|---|---|---|---|---|---|---|
 |
32-bit builds, start with:
python scripts/mk_make.pyor instead, for a 64-bit build:
python scripts/mk_make.py -xthen:
cd build
nmakeExecute:
python scripts/mk_make.py
cd build
make
sudo make installNote by default g++ is used as the C++ compiler if it is available. If you
would prefer to use Clang change the mk_make.py invocation to:
CXX=clang++ CC=clang python scripts/mk_make.pyNote that Clang < 3.7 does not support OpenMP.
You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python.
For a 64 bit build (from Cygwin64), configure Z3's sources with
CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.pyA 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.
By default, it will install z3 executable at PREFIX/bin, libraries at
PREFIX/lib, and include files at PREFIX/include, where PREFIX
installation prefix if inferred by the mk_make.py script. It is usually
/usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use
the --prefix= command line option to change the install prefix. For example:
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make installTo uninstall Z3, use
sudo make uninstallTo clean Z3 you can delete the build directory and run the mk_make.py script again.
Z3 has an unofficial build system using CMake. Read the README-CMake.md file for details.
Z3 has bindings for various programming languages.
Use the --dotnet command line flag with mk_make.py to enable building these.
On non-windows platforms mono is required. On these platforms the location of the C# compiler and gac utility need to be known. You can set these as follows if they aren't detected automatically. For example:
CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py --dotnetNote for very old versions of Mono (e.g. 2.10) you may need to set CSC
to /usr/bin/dmcs.
Note that when make install is executed on non-windows platforms the GAC
utility is used to install Microsoft.Z3.dll into the
GAC as the
Microsoft.Z3.Sharp package. During install a
pkg-config file
(Microsoft.Z3.Sharp.pc) is also installed which allows the
MonoDevelop IDE to find the bindings. Running
make uninstall will remove the dll from the GAC and the pkg-config file.
See examples/dotnet for examples.
These are always enabled.
See examples/c for examples.
These are always enabled.
See examples/c++ for examples.
Use the --java command line flag with mk_make.py to enable building these.
See examples/java for examples.
Use the --ml command line flag with mk_make.py to enable building these.
See examples/ml for examples.
Use the --python command line flag with mk_make.py to enable building these.
Note that is required on certain platforms that the Python package directory
(site-packages on most distributions and dist-packages on Debian based
distributions) live under the install prefix. If you use a non standard prefix
you can use the --pypkgdir option to change the Python package directory
used for installation. For example:
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packagesIf you do need to install to a non standard prefix a better approach is to use
a Python virtual environment
and install Z3 there. Python packages also work for Python3.
Under Windows, recall to build inside the Visual C++ native command build environment.
Note that the build/python/z3 directory should be accessible from where python is used with Z3
and it depends on libz3.dll to be in the path.
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...See examples/python for examples.
WebAssembly bindings are provided by Clément Pit-Claudel.