Interpolation sits between bounded search and full induction: it uses a bounded run, but instead of reporting bounded to N it extracts an over-approximation of the reachable states from the solver's own reasoning. When that approximation is closed under steps and excludes the bad states, the property is proven without any hand-written helper. Knowing the two conditions it must satisfy, and what the loop does when an approximation is too coarse, tells you why it sometimes finishes with a proof where k-induction stalls, and why it sometimes needs a longer bound.
Split the unrolled design into a prefix A, the first step from the current start set R, and a suffix B, the next m steps toward a violation. If the bounded run from R is unsatisfiable, the solver's refutation yields an interpolant I: a formula over the shared middle state that is implied by A and inconsistent with B. In state terms, I contains the image of R and excludes every state that can reach bad within m steps. Those are the two conditions, and they hold by construction, so an interpolant never swallows a bad-reaching state. The engine then grows the start set to R union I and repeats; if I adds nothing new, R is closed under steps and excludes bad, and the property is proven.
What can go wrong is the next bounded run. The grown start set R is an over-approximation, and it can reach bad in more than m steps even though the real design cannot, so the bounded run from R is now satisfiable. If R is still the real start set the trace is a true counterexample; otherwise it is spurious, and the engine must lengthen the suffix, restart from the real start set and try again. That is the failure mode of a coarse approximation: it costs bound, not soundness.
The script runs that loop on the counter with enable free, reset state 0 and bad state 15, taking at each round the weakest interpolant, every state that cannot reach 15 within m steps. At m equal to 1 the interpolant is 0 to 13: the grown start set contains 13, which reaches 15 in two steps, so the next bounded run is satisfiable and spurious. The same happens at m equal to 2, 3 and 4, each time with a start set one state smaller. At m equal to 5 the interpolant is 0 to 9, which is closed under steps: the property is proven, with the bound at 5. The unsafe variant, 9 declared bad, lengthens until the bounded run from the real reset state itself finds the path, and reports a counterexample at m equal to 8. The first check runs the two conditions on single candidates: the image of reset within 3 steps fits inside the candidate 0 to 4, which excludes every state that can reach 15 within 5 steps, and the over-wide candidate that includes 10 and 11 is not an interpolant. The set 0 to 4 satisfies both conditions and is still not closed under steps, because it steps to 5, which is why the loop has to grow it.
N = 16
ALL = set(range(N))
def succ(s):
return {s, 0 if s == 9 else (s + 1) % N}
def image(S):
return {t for s in S for t in succ(s)}
def pre(S):
return {s for s in ALL if succ(s) & S}
def reach_within(S, steps):
cur = set(S)
for _ in range(steps):
cur |= image(cur)
return cur
def bad_within(bad, m):
out = set(bad)
for _ in range(m):
out |= pre(out)
return out
def is_interpolant(A_image, I, B):
# condition 1: implied by the prefix (contains its image); condition 2: inconsistent with the suffix
return A_image <= I and not (I & B)
# the two conditions on single candidates (reset within 3 steps, bad-reaching within 5 steps)
image3 = reach_within({0}, 3)
B5 = bad_within({15}, 5)
assert image3 == {0, 1, 2, 3} and B5 == {10, 11, 12, 13, 14, 15}
assert is_interpolant(image3, {0, 1, 2, 3, 4}, B5)
assert not is_interpolant(image3, image3 | {10, 11}, B5) # over-wide candidate swallows bad-reaching states
assert image({0, 1, 2, 3, 4}) - {0, 1, 2, 3, 4} == {5} # a valid interpolant need not be closed under steps
def itp_loop(init, bad, mmax=12):
log, m, R = [], 1, set(init)
while m <= mmax:
if reach_within(R, m + 1) & bad: # bounded run from R: one step plus m more
if R == set(init):
return "counterexample", m, log
log.append(("spurious", m)) # the grown set reaches bad: lengthen and restart
R, m = set(init), m + 1
continue
I = ALL - bad_within(bad, m) # weakest interpolant
assert is_interpolant(image(R), I, bad_within(bad, m))
if I <= R:
return "proved", m, log, R
R |= I
return "unknown", m, log
status, m, log, R = itp_loop({0}, {15})
assert status == "proved" and m == 5, (status, m)
assert R == set(range(10)) and image(R) <= R and not (R & {15})
assert [x for x in log if x[0] == "spurious"] == [("spurious", 1), ("spurious", 2), ("spurious", 3), ("spurious", 4)]
ustatus, um, _ = itp_loop({0}, {9})
assert ustatus == "counterexample" and um == 8, (ustatus, um)
assert itp_loop({0}, {9})[0] != "proved" # injected: a false proof claim about the unsafe system
print("PASS: interpolant loop proves 0..9 at bound 5 after 4 spurious restarts; unsafe variant refuted at bound 8")Interpolation verdicts quote the bound they used: an interpolant is relative to its split.
A run that finishes with a proof names the invariant, which is reviewed like any helper.
Stalled runs are diagnosed by bound and split before they are given more time.
Recheck a stalled interpolation run by varying the split: a short prefix with a long suffix behaves differently from the reverse, and the log shows which side grows. Count the spurious restarts: a run that keeps lengthening its bound is telling you the approximations are coarse, which on wide arithmetic is a sign of the interpolants bloating exactly where a solver struggles, and abstraction helps interpolation for the same reason it helps bounded search.
No: over-approximation is allowed to contain extra states, as long as none of them can reach bad within the suffix and the final set closes under steps. Extra unreachable states threaten the bound the loop needs, never soundness.