In SV-COMP no-overflow tasks there are cases similar to the following example:

int main() {
  int i = __VERIFIER_nondet_int();
  int j = __VERIFIER_nondet_int();
  
  if (!(i==0 && j==0)) return 0;
  while (i<100) {
    j+=2;
    i++;
  }
  __VERIFIER_assert(j==200);
  return 0;
}

where the loop has a fixed size of iterations from i == 0 to i == 99, which the autotuner is unable to detect because it only relies on finding the starting value through assignments.

As the CIL representation of the if-statement if (!(i==0 && j==0)) return 0; is too complicated to extract the value from there, I opted for assuming that if the variable is not assigned to a constant value before the loop, its' value is 0 (or 11, if the loop is decreasing).

Similarly, I propose assuming that the diff is 1 if it is not found, as loops are more often increasing the start value than decreasing.

This revealed another bug, which makes me wonder if the autotuner even was ever able to find any fixed-size loops previously, as it checked for the condition:

"The loop should modify the loop variable only once per iteration in its body and the difference needs to be constant. (This way the maximum number of steps can be estimated.)"

using the loop statement itself, not its body, making it always think that there is a nested loop present that is also modifying the loop variable.

Also, loops with size 100 were deemed too big to unroll if there were more than 0 instructions (function calls or assignments) in the loop.