This talk gives an overview of a general approach to reason with quantified formulas in Satisfiability Modulo Theories. The approach maintains a set S of ground instances of the input formulas which is incrementally expanded with instances of quantified input formulas where the instances are selected based on counter-models of S. In first-order theories that admit quantifier elimination and have a decidable ground satiisfiability problem, this approach leads to pratically efficient decision procedures for the full theory.