Integrating SAT solvers with domain-specific reasoners