Z3 is a high-performance theorem prover being developed at Microsoft Research.
- Z3 has moved to github. You can access Z3 from
- This site will be retired and taken down as soon as we have moved all useful information.
git clone https://git01.codeplex.com/z3
is the stable and official branch. pure
is a stable branch containing Microsoft-only contributions. The branch
should be used to submit external contributions (see this
for more details). All other branches should be viewed as "work in progress", they may contain unstable and/or untested code.
The Z3 downloads on this site are available from github under the MIT license.
- Download pre-compiled binaries for Windows
- Supported platforms: Windows, OSX, Linux and FreeBSD
- Download nightly builds for
- Z3 source code can be compiled using Visual Studio, g++ and clang++
There are many ways to contribute to Z3.
- Review code checkins and send
- Submit bugs and help us verify fixes as they are checked in.
- Engage with other Z3 users and developers on
- Contribute tests and benchmarks at http://z3test.codeplex.com.
- Contribute code. We only accept pull requests in the branch contrib. See this
link for more details. We initially released the Z3 source code because it complements our research papers, and may help others to clarify misunderstandings, dispute claims made in our papers, experiment new ideas, reproduce our results, and advance the