z3 is an open source theorem prover / SMT solver from Microsoft Research. (SMT stands for "satisfiability modulo theories".) This package contains the Python bindings for z3.