Z3 is a high-performance theorem prover being developed at Microsoft Research.
git clone https://git01.codeplex.com/z3
is the stable and official branch. pure
is a stable branch containing Microsoft-only contributions. The branch contrib
should be used to submit external contributions (see this link
for more details). All other branches should be viewed as "work in progress", they may contain unstable and/or untested code.
- Download pre-compiled binaries for Windows
- Supported platforms: Windows, OSX, Linux and FreeBSD
- 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 feedback.
- Submit bugs and help us verify fixes as they are checked in.
- Engage with other Z3 users and developers on StackOverflow.
- 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 state-of-the-art.