# When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?

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?

If the formula is satisfiable you cannot construct an interpolant. If the formula is unsatisfiable, you know that the final states are not reachable in at most $k$ steps. You do not know about reachability of final states in $k+1$ or more steps.
If the formula you suggest is unsatisfiable, you can replace the sub-formula $I$ of $A$ with the interpolant and check for satisfiability. If this new formula is unsatisfiable, you know that the error state is not reachable in $k+1$ steps. Something significant just happened. We were able to determine that the final states are not reachable in $k+1$ steps using only $k$ unwindings.