Z3 is a satisfiability modulo theories (SMT) solver; given a set of
constraints with variables, it reports a set of values for those variables
that would meet the constraints. The Z3 input format is an extension of the
one defined by the SMT-LIB 2.0 standard. Z3 supports arithmetic, fixed-size
bit-vectors, extensional arrays, datatypes, uninterpreted functions, and
quantifiers.
