Bug: Ultimate's termination analysis infers wrong ranking function

[debugfe]

Basic Info

• Version: 00d4337 from SV-Comp 26
• Java Version: openjdk 21.0.10 2026-01-20
• Commands: ~/UAutomizer-linux/Ultimate.py --spec termination.prp --file test.c --full-output --architecture 64bit

Description

I believe Ultimate infers a wrong ranking function (as printed in the log) for the following code:

int main() {
  int n = 3;
  int v1 = n, decrement = 1;
  while (v1 > 0) {
    if (decrement == 1) {
      v1--;
      decrement = 0;
    } else {
      decrement = 1;
    }
  }
  return 0;
}

The summary in the log says

...
    Your program was decomposed into 2 terminating modules (1 trivial, 1 deterministic, 0 nondeterministic). One deterministic module has affine ranking function v1 and consists of 4 locations. 1 modules have a trivial ranking function, the largest among these consists of 3 locations.

However, here v1 cannot be a ranking function, it does not decrease in every iteration.
LassoRanker on the other hand did find the correct ranking function (long) 2 * v1 + (long) -1 * decrement, see also the web interface .
Is this a bug (in the translation to LassoRanker)?

[schuessf]

At least to my understaning, this is expected.
LassoRanker is only able to analyze lasso programs (which is done here with block encoding to collapse the whole loop into a single "statement"), but it provides a ranking function for the whole program.
BüchiAutomizer on the other hand can analyze arbitrary programs (not relying on block encoding) by decomposing the program into modules (i.e., smaller lasso programs), but it only provides a termination proof (often via a ranking function) for each of the modules separately, which you can also see here:

• The module with the ranking function v1 covers only the then-branch of the program.
• The other module with a trivial ranking function covers only the else-branch of the program (which is infeasible, as it cannot be taken twice in a row).
• Apparently, these two modules are sufficient to cover the whole program.

I don't know all of the details, maybe @Heizmann has some further insights to our approach in BüchiAutomizer?

[debugfe]

Okay, I also thought this might not be intended because the inferred ranking functions change when just renaming variable decrement to b:
Your program was decomposed into 5 terminating modules (2 trivial, 3 deterministic, 0 nondeterministic). One deterministic module has affine ranking function b and consists of 3 locations. One deterministic module has affine ranking function b and consists of 3 locations. One deterministic module has affine ranking function v1 and consists of 4 locations. 2 modules have a trivial ranking function, the largest among these consists of 6 locations.