Comment by greatgib

If anyone wondering, because it took me a few hops to find out:

Z3 is a high-performance theorem prover being developed at Microsoft Research.