Interpolant-Based Unbounded Model Checking