RecurIC3: Exploiting Structural Lemma Reuse to Accelerate IC3

IC3/PDR has become a widely adopted technique for safety model checking due to its high efficiency. Despite its success, the algorithm often suffers from redundant exploration due to the lack of a cross-level memory mechanism. This results in the repetitive discovery of highly similar CTIs (Counterexamples to Induction), forcing the solver to waste computational effort traversing overlapping blocking chains. We propose RecurIC3, a framework that alleviates this bottleneck via structural reuse. RecurIC3 maintains a Bad State Tree (G_bad) that persistently records CTIs together with their level-aligned predecessor–successor links along blocking chains, turning the blocking phase into a history-aware process. To reduce solver calls, RecurIC3 first retrieves and rechecks lightweight candidates from G_bad and falls back to solver queries only when reuse is exhausted. This approach can significantly reduce the search space, thereby enhancing the verification efficiency of IC3. We implemented RecurIC3 in the state-of-the-art model checker Kind2 and evaluated it on the official benchmark suite. On instances where reuse is triggered, RecurIC3 reduces the number of explored tree nodes by 27%, achieves a 1.42× cumulative speedup, and solves 16 additional instances (13 Safe and 3 Unsafe) within the same timeout. These results suggest that structural reuse can substantially accelerate IC3.