SMT solvers have nowadays become nearly ubiquitous in semantics based programming tools. They solve small logic puzzles or larger constraints useful for program analysis, verification and testing. When useful, but their internals opaque, they appear as magic wands with an air of mystery. This tutorial aims to unveil internals of Z3; establishing principles used for solving design, the art of programming solvers, and the empirics employed for integrating heuristics. The goal is to give participants an overview of the main ingredients useful for designing and implementing SMT solvers and at the same time serve as an entry guide to integrating new functionality within contemporary SMT solvers. Z3 is an SMT solver available from Microsoft Research.