Python binding for Z3, a high-performance theorem prover developed
at Microsoft Research.