Bug: Ultimate provides wrong termination result

[pwnchaser]

Hi, I found that the version from SV-Comp classifies this program as non-terminating (printing RESULT: Ultimate proved your program to be incorrect!):

extern int __VERIFIER_assume(int cond);
extern int __VERIFIER_nondet_int(void);

int main() {
  int n = __VERIFIER_nondet_int();
  __VERIFIER_assume(n >= 1);
  long nlng = (long) n;
  int nint = (int) nlng;
  while(nint <= 0) {
  } 
  return 0;
}

However if we encode the loop condition with __ULTIMATE_assert(!(nint <= 0)); and use --spec unreach-call.prp Ultimate sees that the loop condition is always false, so I'd expect to see that the program below is terminating.
I am using the setup from SV-Comp, specifically Ultimate 0.3.0-dev-d790fec and used the following command for the termination analysis:

"/usr/bin/java" "-Dosgi.configuration.area=/home/UAutomizer-linux/data/config" "-Xmx15G" "-Xms4m" "-jar" "/home/UAutomizer-linux/plugins/org.eclipse.equinox.launcher_1.6.800.v20240513-1750.jar" "-data" "@noDefault" "-ultimatedata" "/home/UAutomizer-linux/data" "-tc" "/home/UAutomizer-linux/config/AutomizerTermination.xml" "-s" "/home/UAutomizer-linux/config/svcomp-Termination-64bit-Automizer_Default.epf" "--cacsl2boogietranslator.entry.function" "main" "--witnessprinter.witness.directory" "/home/UAutomizer-linux" "--witnessprinter.witness.filename" "witness" "--witnessprinter.write.witness.besides.input.file" "false" "--witnessprinter.graph.data.specification" "CHECK( init(main()), LTL(F end) )" "--witnessprinter.graph.data.producer" "Automizer" "--witnessprinter.graph.data.architecture" "64bit" "--witnessprinter.graph.data.programhash" "2c49b87410271d55416f5a5bc7d2a9ffd85bb848b87c5b0387334a9de7ab45eb" "-i" test.c

Additionally, I wanted to ask if Ultimate is able to emit inferred ranking functions (apart from the incomplete info the log)?

Thanks in advance!

[Heizmann]

Thanks for the report. @schuessf found out that we accidentally use the wrong settings for termination. We will fix that.

The tool implements the approach that is published in the following two papers.
https://link.springer.com/chapter/10.1007/978-3-319-08867-9_53
https://dl.acm.org/doi/10.1145/3192366.3192405
In the log you see the ranking functions that were computed for each module. If this helps you, I can implement that we write out these ranking functions also as a result. However, we cannot yet compute a ranking function for the whole program in general. (For your program, we decompose the program only in one module and hence we also have a ranking function for the program)

[pwnchaser]

Wow, thanks for the fast fix!
I noticed however that this changed the termination of other programs in an unexpected way:
E.g. this program now became "terminating"

extern int __VERIFIER_nondet_int(void);

int main(){
  int x = __VERIFIER_nondet_int();
  int y = 0;
  while (x > 0) {
    x = __VERIFIER_nondet_int();
    x = x + x + y;
    y = y - 1;
  }
}

while dropping line 7 (x = __VERIFIER_nondet_int();) results in a program that is found non-terminating as expected.

[Heizmann]

I think the problem is that there can be a signed integer overflow in the line x = x + x + y;.
Our analysis for detecting overflows confirms this.
Our termination analysis is only supposed to be sound for programs without undefined behavior.

[pwnchaser]

Oh I see the assignment here adds undefined behavior.
Concerning the ranking functions, yes writing out the ranking function separately would be great. Specifically, it would be nice if one could also see which ranking function corresponds to which program loop (ideally LOC of the input program) in case that information is not lost during Ultimate's analysis.
Cheers :)