goblint
Success messages with bounds from termination analysis
Our race analysis can output "proofs" as success messages with allglobs enabled. This is useful for inspecting why Goblint believes the program to be correct.
We could do something similar for termination analysis: when we manage to prove a loop to be bounded and thus terminate, optionally output a success message with the bound (at least non-relationally, if not relationally). @karoliineh looked at some SV-COMP termination program where termination wasn't obvious because the loop could both increment (by 2) or decrement (by 1) the counter based on some condition.
The SV-COMP task termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c can be used as a test case when addressing this issue.
I think we had such a message at some point but then removed it to be less verbose. One can probably go dig through https://github.com/goblint/analyzer/pull/1093 to find the commit where it was removed.
