Satisfiability Modulo Theories (SMT) solvers are increasingly used in verification as back-ends to check the satisfiability of formulas in presence of interpreted symbols.  After a brief overview of their architecture, we will review the current methods used in those solvers to handle quantifiers.  An early technique, E-matching or trigger-based instantiation, generates instances when some patterns of terms are present in the formula.  Although it is experimentally quite successful, it might generate many useless instances. Model-based quantifier instantiation is a more recent semantic instantiation technique: instances are built to fix a tentative model that does not agree with the quantified formulas.  An even more recent method to which we have contributed is conflict-based instantiation; it can be seen as a weaker and more efficient form of model-based instantiation, that generates only the instances that contradict the partial model in the ground solver.  Finally, we will also report on our results on revisiting enumerative instantiation.