 (Ganzinger et al. 2004) discusses an approach to SMT called DPLL(T) consisting of a general DPLL(X) engine that works in conjunction with a solver SolverT for background theory T. Bofill et al. (2008) present the approach in the setting of the theory of arrays, where the DPLL engine is responsible for enumerating propositional models for the given formula whereas SolverT checks whether these models are consistent with the theory of arrays. Their approach is sound and complete, and can be smoothly extended to multidimensional arrays.