Note By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license.
Z3 is an SMT solver that combines several theory solvers into a combined framework. It can be used to prove theorems and find counter-examples for non-theorems.