The manual inspection of not enabling vs enabling loopUnrolling showed that the stats for the current unrolling are (broadly) the following:

• The maximum of loop unrolling is 25
• The average of loop unrolling is 6
• The median of loop unrolling is 4

Looking into the semantics of the tasks where unrolling helped us verify (Unknown -> True), however, revealed that

• The maximum bound of (other than nondet) is 1000000
• The average bound is 37074
• The median bound is 10

Regardless of the semantics of the program, I also tried to find the minimum amount of unrollings necessary for solving the task. This showed that:

• The average minimum unrollings needed to solve the task is 2
• The median minimum is 10

For all loops with a nondet bound that I found by inspection, the sufficient (minimum) times of unrollings needed for solving the task is at max 2.

As revealed by some intermediate runs, unrolling fixed loops with the bound up to 100 makes us timeout in many of the instances (including on some of the regression tests; see #1516 (comment)). For the maximum bound of loop unrolling, which was 25 previously, the actual semantics were that the loop has to be unrolled by a minimum of 19 times (the syntax can determine that) for us to solve the task. Thus, I have changed the heuristic of if totalLoops < 17 && AutoTune0.isActivated "forceLoopUnrollForFewLoops" then 10 else 0 in to | Some i when i <= 20 -> i, i.e., if a fixed loop iteration of 20 or less is found, we will unroll the loop the found amount of times.
(The next old unroll maximum would be 16, where the semantics is nondet, and 1 unroll is sufficient, and further from that, the new max is 12, which cases semantics I have not looked into too thoroughly yet.)

Otherwise, if the found loop iterations are 20+, we will default to the median of the previous unrolling (4), which, in many cases, is the sufficient amount of unrolling needed to solve a task - so, we would default to unrolling 4 times instead of the complicated heuristic of calculating some (weird) bound based on the number of statements in the loop: max unroll_min (targetInstructions / loopStats.instructions). According to a run with these settings, we do not lose too many tasks but gain a bit in performance (e.g. instead of the "random" unrolling of 12 times in many cases, where 2 times would be sufficient, we now only unroll 4 times).

We made a run with these new defaults, and I investigated some of the tasks (edge cases) where we could not solve the task because the iterations found by the new heuristics were too small. Some PRs will follow this PR to again handle these lost cases in addition to some new tasks that we can further solve due to some (new) improvements to the unrolling.