Z3 is a theorem prover from Microsoft Research with support for bitvectors,
booleans, arrays, floating point numbers, strings, and other data types.