I guess that you can think of our algorithm as lazy SAT modulo quantified first order logic, with the crucial difference that first order logic is undecidable. But anyway in this case the "decision procedure for T" would just be checking whether any two complementary literals which are true in the model are unifiable, which is decidable.

Paper: http://www.cs.man.ac.uk/~korovink/my_pub/inst_gen_modular.pd...

Basically CDCL(T) uses the theory part (the "T") as a callback in the inner loop of the SAT solver (to validate partial models). iProver and similar refinement provers tend to have their own outer loops ("refinement loops" in other communities) that makes a succession of calls to the SAT solver, to completion, and use the model or unsat core to refine their own abstraction for the next iteration of the outer loop.