Z3 is a high-performance theorem prover being developed at Microsoft Research.

Background

Source Code

git clone https://git01.codeplex.com/z3

REMARK: master 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.

Platforms

  • 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++

Contribute

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.

Last edited Jan 6, 2013 at 2:54 AM by leodemoura, version 56