A few papers I've been reading have algorithms on using interpolants for the following clauses (bounded model checking):
$$ \begin{align*} A &= I \wedge T_1 \\ B &= T_2 \wedge T_3 \wedge \ldots \wedge T_k \wedge (F_1 \vee F_2 \vee \ldots \vee F_k) \\ \end{align*} $$
This interpolant is then used to compute an over approximation of reachable states and then we can check for inconsistency with less computation.
BUT, the interpolant itself is derived from a proof of unsatisfiability. So before you get the interpolant, wouldn't you already know if the final states are reachable?