[kaeso]

"Z3 integrates a modern DPLL-based SAT solver, a core theory solver that handles equalities and uninterpreted functions, satellite solvers (for arithmetic, arrays, etc.), and an E-matching abstract machine (for quantifiers)"

From http://research.microsoft.com/en-us/um/redmond/projects/z3/z...