Z3, also known as the Z3 Theorem Prover, is a cross-platform satisfiability modulo theories (SMT) solver by Microsoft.