Prototype loop transition invariant generation

[sim642]

YAML witness 2.1 has loop_transition_invariants for describing proofs of termination. I think it will be a demo in SV-COMP 2026 but I was still wondering if we could generate something like that. These invariants basically relate values from a previous iteration with values from the current iteration.

The idea, which might already be wrong, is the following:

1. Duplicate the local relational state with primed previous iteration variables.
2. Put those together into one relational state with the original local state.
3. Assert that the instrumented loop counter has strictly increased (or increased exactly by one?).
4. Project out the loop counters.

For example, for 78-termination/01-simple-loop-terminating this can output

(long long )\at(i, AnyPrev) >= 1LL && (long long )i >= (long long )\at(i, AnyPrev) + 1LL

or

(long long )\at(i, LastPrev) + 1LL == (long long )i && (long long )i >= 2LL

These express a strict increase in program variables. The only thing missing here is an upper bound for i, which in this regression test actually comes from non-Apron intervals, but should be easily added as i <= 11. Together, these constitute some kind of proof of termination.

TODO

• [ ] Convince ourselves that this method is correct.
• [ ] Clean up the implementation.