Repository files navigation

Z3 is a theorem prover from Microsoft Research.It is licensed under theMIT license. Windows binary distributions includeC++ runtime redistributables

If you are not familiar with Z3, you can starthere.

Pre-built binaries for stable and nightly releases are availablehere.

Z3 can be built usingVisual Studio, aMakefile or usingCMake. It providesbindings for several programming languages.

See therelease notes for notes on various stable releases of Z3.

Azure Pipelines	Open Bugs	Android Build	WASM Build	Windows Build	Pyodide Build

Docker image.

For 32-bit builds, start with:

python scripts/mk_make.py

or instead, for a 64-bit build:

python scripts/mk_make.py -x

then run:

cd buildnmake

Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later.

Execute:

python scripts/mk_make.pycd buildmakesudo make install

Note by defaultg++ is used as C++ compiler if it is available. If youprefer to use Clang, change themk_make.py invocation to:

CXX=clang++ CC=clang python scripts/mk_make.py

Note that Clang < 3.7 does not support OpenMP.

You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler.In that case, 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.py

A 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 executables atPREFIX/bin, libraries atPREFIX/lib, and include files atPREFIX/include, where thePREFIXinstallation prefix is inferred by themk_make.py script. It is usually/usr for most Linux distros, and/usr/local for FreeBSD and macOS. Usethe--prefix= command-line option to change the install prefix. For example:

python scripts/mk_make.py --prefix=/home/leocd buildmakemake install

To uninstall Z3, use

sudo make uninstall

To clean Z3, you can delete the build directory and run themk_make.py script again.

Z3 has a build system using CMake. Read theREADME-CMake.mdfile for details. It is recommended for most build tasks,except for building OCaml bindings.

vcpkg is a full platform package manager. To install Z3 with vcpkg, execute:

git clone https://github.com/microsoft/vcpkg.git./bootstrap-vcpkg.bat# For powershell./bootstrap-vcpkg.sh# For bash./vcpkg install z3

Z3 itself has only few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-containedmulti-precision functionality. Python is required to build Z3. Building Java, .NET, OCaml andJulia APIs requires installing relevant toolchains.

Z3 has bindings for various programming languages.

You can install a NuGet package for the latest release Z3 fromnuget.org.

Use the--dotnet command line flag withmk_make.py to enable building these.

Seeexamples/dotnet for examples.

These are always enabled.

Seeexamples/c for examples.

These are always enabled.

Seeexamples/c++ for examples.

Use the--java command line flag withmk_make.py to enable building these.

Seeexamples/java for examples.

Use the--ml command line flag withmk_make.py to enable building these.

Seeexamples/ml for examples.

You can install the Python wrapper for Z3 for the latest release from pypi using the command:

   pip install z3-solver

Use the--python command line flag withmk_make.py to enable building these.

Note that it is required on certain platforms that the Python package directory(site-packages on most distributions anddist-packages on Debian-baseddistributions) live under the install prefix. If you use a non-standard prefixyou can use the--pypkgdir option to change the Python package directoryused for installation. For example:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

If you do need to install to a non-standard prefix, a better approach is to useaPython virtual environmentand install Z3 there. Python packages also work for Python3.Under Windows, recall to build inside the Visual C++ native command build environment.Note that thebuild/python/z3 directory should be accessible from where Python is used with Z3and it requireslibz3.dll to be in the path.

virtualenv venvsource venv/bin/activatepython scripts/mk_make.py --pythoncd buildmakemake install# You will find Z3 and the Python bindings installed in the virtual environmentvenv/bin/z3 -h...python -c'import z3; print(z3.get_version_string())'...

Seeexamples/python for examples.

The Julia packageZ3.jl wraps the C API of Z3. A previous version of it wrapped the C++ API: Information about updating and building the Julia bindings can be found insrc/api/julia.

A WebAssembly build with associated TypeScript typings is published on npm asz3-solver. Information about building these bindings can be found insrc/api/js.

ProjectMachineArithmetic provides a Smalltalk interfaceto Z3's C API. For more information, seeMachineArithmetic/README.md.

• Default input format isSMTLIB2

• Other native foreign function interfaces:

• C++ API

• .NET API

• Java API

• Python API (also available inpydoc format)

• Rust

• C

• OCaml

• Julia

• Smalltalk (supports Pharo and Smalltalk/X)

• TheAxiom Profiler currently developed by ETH Zurich