Why a property can be true of every reachable state and still fail k-induction. Diagnose an inductive-step failure and find the invariant that closes the proof.
Part of Hardware Formal Verification on formal.org.