A tutorial on Z3. Z3 is a SAT solver. It is used as the underlying deduction engine in many applications that need a theorem prover.