The verification of complex systems is generally based on proving the validity, or, dually, the satisfiability of a logical formula. A standard practice consists in translating the behavior of the system to be verified into a logical formula, and proving that the negation of the formula is unsatisfiable. These formulæ may be domain-specific, so that it is only necessary to test the satisfiability of the formula modulo some background theory, whence the name Satisfiability Modulo Theories problems, or SMT problems. If the formula is actually satisfiable, this means the system is not error-free, and any model can be viewed as a trace that generates an error. The models of a satisfiable formula can therefore help the designers of the system guess the origin of the errors and deduce how they can be corrected; this is the main reason for example why state-of-the-art SMT solvers feature automated model building tools (see for instance Caferra, Leitsch, and Peltier, 2004).