SMT (Satisfiability Modulo Theories) solvers are decision procedures for large logic formulas in expressive languages built on top of propositional logic. They are used successfully for an increasing number of applications, and most notably in the context of formal verification. We will present the SMT architecture and how it interacts with the embedded SAT solver. In particular, we will study how a SAT solver can be lifted to more expressive languages, and how to build combinations of decision procedures for unions of decidable languages. In conclusion, we will consider a couple of important research challenges for the near future of SMT: arithmetics and proofs.