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

News

  • Z3 has moved to github. You can access Z3 from Z3Prover
  • This site will be retired and taken down as soon as we have moved all useful information.

Information

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.

License

The Z3 downloads on this site are available from github under the MIT license.

Platforms

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 Thu at 8:40 PM by NBjorner, version 72