Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types. This is a fork of the original Z3. Unfortunately it conflicts with the math/z3 package as a result.