Z3 is a state-of-the art theorem prover from microsoft research. it can be used to check the satisfiability of logical formulas over one or more theories. z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories.

this package can be used to invoke z3 via its c++ api.