We present a decision procedure for the problem of, given a set of regular expressions R1,..Rn, determining whether their intersection R = R1 ∩…∩ Rn is empty. While this problem is decidable, the implementation of pratical algorithms is still an open issue. Current solutions rely on the classical product algorithm for intersection of DFAs (Deterministic Finite Automata). Our solver, Revenant, finitely unrolls the automata from the regular expressions, encoding each as a set of propositional constraints. If a SAT solver determines satisfiability then R is non-empty. Otherwise our solver uses unbounded model checking techniques to extract an interpolant from the bounded proof. This interpolant serves as an overapproximation of R. If the solver reaches a fixed-point with the constraints remaining unsatisfiable, it has proven R to be empty. Otherwise, it increases the unrolling depth and repeats. We compare Revenant with other state-of-the-art string solvers. Evaluation suggests that it behaves better for constraints that express the intersection of sets of regular languages, a case of interest in the context of verification. This work will be presented at TACAS'13 and it is done together with Graeme Gange, Harald Sondergaard, Peter Schachte and Peter J. Stuckey from the University of Melbourne.