Introduction

Z3 is a Satisfiability Modulo Theories (SMT) solver. That is, it is an automated satisfiability checker for many sorted (i.e., typed) first-order logic with built-in theories, including support for quantifiers. The currently supported theories are:

• equality over free (aka uninterpreted) function and predicate symbols,
• real and integer arithmetic (with limited support for non-linear arithmetic),
• bit-vectors,
• arrays,
• tuple/records/enumeration types and algebraic (recursive) data-types.

Z3 checks whether a set of formulas is satisfiable in the built-in theories. When, the set of formulas is existential (i.e., it does not contain universal quantifiers), then Z3 is in fact a decision procedure: it is always guaranteed (modulo bugs and memory limits) to return a correct answer. When a set of formulas F is satisfiable, Z3 can produce a model for F. Models are particularly useful in software verification, because they can be easily translated into execution traces. If a set of formulas contains universal quantifiers, then the model produced by Z3 should be viewed as a potential model, since Z3 is incomplete in this case.

Z3 can be used as a command-line executable, or a library. In the current version, we provide APIs for: C, .NET, and OCaml.