Detect fixed loops with autotuner even if there is no assignment of const value to the loop variable before loop

[karoliineh]

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.

[sim642]

On entire sv-benchmarks runs with 60s, this doesn't really make any difference to our score (after the second fixes). Some tasks (loop-lit/hh2012-ex1b) go from <1s to 60s TIMEOUT, embarrassingly many are from goblint-regression. Some tasks (list-simple/dll2n_remove_all) go from true to unknown, which is particularly odd.
With the 60s time limit, we gain only 6 new true results.

While this PR makes the fixed loop unrolling work for the first time ever, the lack of positive impact suggests we need to rethink our loop unrolling because there are dubious things going on.