Home

Information

• Z3 is an SMT solver and supports the SMTLIB format.
• Try Z3 in your browser.
• Browse Z3 Q&A at Stack Overflow
• Read our FAQ
• Tutorials and Documentation

On the web

• Checking Firewalls by Andrew Helwer.
• Z3 in Dynamics Product Configurator by Dennis Conrad.
• Quick Introduction to SAT/SMT solvers and symbolic execution An excellent source of well-worked through and motivating examples of using Z3's python interface.
• Ransomware and Z3 by 0xec.
• IDE for Z3 based on ACIDE
• Leo de Moura's Blog
• Python symbolic exploration using Z3

Background

• Programming Z3, a tutorial.
• Z3 internals, a tutorial.
• Diagnosing Z3 proof failures.
• Browse our Slides, read our Papers
• Papers citing Z3 at Google Scholar

Source Code

• Is here on github.

REMARK: master is the official branch and all new contributions including bugfixes are added to master directly. pure and unstable are branches that are kept only as backups and should not be used. All other branches should be viewed as "work in progress", they may contain unstable and/or untested code.

Platforms

• Supported platforms: Windows, OSX, Linux (Ubuntu, Debian), and FreeBSD
• Download source & binary releases (or here)
• Download automatically compiled nightly binaries (may be unstable)
• Z3 source code can be compiled using Visual Studio, g++ and clang++

External bindings

Contact the creator of the package for any support issues.

• guile-z3
• NuGet
• OCaml
• Python/Pip
• Rust
• Vcpkg
• Ruby

Power Tools

• The Axiom Profiler currently developed by ETH Zurich

License

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

Contribute

There are many ways to contribute to Z3.

• Engage with other Z3 users and developers on Stack Overflow.
• Contribute tests and benchmarks to z3test.
• Contribute code.
• For more information see contribution guidelines.

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.