Z3: an efficient SMT solver - de Moura, Leonardo; Bjørner, Nikolaj (2008 Tools and Algorithms for Construction and Analysis of Systems, 2008)
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.