Investigate soundness of boundedness check for termination

[sim642]

Originally posted by @sim642 in #1580 (comment)

---

Although this doesn't really explain the case from #1577:

./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/termination.prp ../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c --html --enable dbg.termination-bounds

outputs (among other things)

[Success][Termination] Loop terminates: bounded by 0 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 1 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 2 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 3 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 4 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 5 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 6 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 7 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 8 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 9 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by (Not {0, 1}([0,32]),[10,2147483896],not {0} ([0,32]),ℤ) iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)

The maximum bound 2147483896 is one lower, but that's just because we activate congruence analysis we can rule out 2147483897 (which is is excluded because it is odd).
And we don't go to top because we assume no overflows, so 2147483896 + 2 doesn't overflow to top. But if it were to be a loop incrementing by one, this could go up to 2147483897 and we consider it unbounded. So I'm a bit confused by the termination checking logic with this.

---

We discussed this in GobCon 2024-10-29. Unrolling the loop once might be of importance here: all subsequent iterations have even x and our congruence domain also knows that. However, the termination check is on the instrumented loop counter variable, not x, and that's still incremented by 1 each iteration.

There's something about relationality in this case as well:

1. Even having interval for x and a relational equality a la 2 * term = x doesn't help us because we cannot refine intervals via such equalities right now.
2. Polyhedra domain (which should be activated automatically for termination but somehow isn't) does infer a constraint with multiplier 2.
3. Octagon domain also proves this terminating although it cannot represent such constraints. So something else must be going on.

The big question is: is boundedness checking by being top really sound?