Lazy algorithms for <I>Satisfiability Modulo Theories</I> (SMT) combine a
generic DPLL-based SAT <I>engine</I> with a <I>theory solver</I> for the given
theory <I>T</I> that can decide the <I>T</I>-consistency of conjunctions of
ground literals.  For many theories of interest, theory solvers need to reason
by performing internal case splits.  Here we argue that it is more convenient
to delegate these case splits to the DPLL engine instead.  The delegation can
be done on demand for solvers that can encode their internal case splits into
one or more clauses, possibly including new constants and literals. This
results in drastically simpler theory solvers.  We present this idea in an
improved version of DPLL(<I>T</I>), a general SMT architecture for the lazy
approach, and formalize and prove it correct in an extension of <I>Abstract
DPLL Modulo Theories</I>, a framework for modeling and reasoning about lazy
algorithms for SMT.  A remarkable additional feature of the architecture, also
discussed in the paper, is that it naturally includes an efficient
Nelson-Oppen-like combination of multiple theories and their solvers.