Many approaches for Satisfiability Modulo Theory (SMT(T)) rely on the
  integration between a SAT solver and a decision procedure for sets
  of literals in the background theory T (T-solver).  When T is the
  combination of two or more simpler theories, the approach is
  typically handled by means of Nelson-Oppen's  combination
  procedure (NO), in which two specific T-solvers deduce and exchange
  (disjunctions of) interface equalities.

  In recent papers we have proposed a new approach to SMT($\bigcup_i T_i$),
  called \emph{Delayed Theory Combination} (DTC). Here part or all
  the (possibly very expensive) task of deducing interface equalities
  is played by the SAT solver itself.

  In this talk I present and discuss the main features of DTC, and present a 
  comparison with N.O. combination procedure.