Remove restriction that no loop unrolling is done when breaks are in the loop

[karoliineh]

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

int counter = 0;
int main() {
    int  X = __VERIFIER_nondet_int();
    long long x = 0;

    while (counter++<10) {
        ...
        if (!(x <= X))
            break;
        ...
    }
    ...

Where we do not detect loops with fixed iterations due to the restriction:

There is one single break in an if statement where the condition compares a local variable v to a constant e.

This PR removes this restriction, as reaching these breaks should make the loop iterations smaller anyway.

However, all these tasks also have the increment counter++ in the loop condition, which we do not handle and which is very difficult to handle using only the syntax, as these statements are picked into pieces by CIL:

int counter = 0;
int main() {
    int  X = __VERIFIER_nondet_int();
    long long x = 0;

    tmp = counter;
    counter = counter + 1;
    while (tmp<10) {
        ...
        if (!(x <= X))
            break;
        ...
        tmp = counter;
        counter = counter + 1;
    }
    ...

Thus, I opted for another assumption that when we find a fixed loop and its start but cannot detect the increment within the loop, we assume the increment is 1.

This solved the tasks with the bounds being 5 and 10, but for bounds 20 and 50, I also had to apply the hack introduced in #1516 to just use the fixed loop size that was found by the heuristics if there are less than 10 loops in the program (the only stat I could find/access to estimate the size of the program (being small)).

[sim642]

checkNoBreakVisitor itself is also unused now.

[sim642]

Looking at this visitor now, I understand why it didn't want multiple breaks. It's main goal is to actually find the comparison for the loop, which will be an if with a break inside.
By only allowing one such break it guaranteed that the result is unambiguous: there couldn't be multiple such comparisons found.

Now, if there are multiple matching ifs with breaks inside, this will still find the first one because compOption is only assigned when it's None, so that can happen at most once.
Is the loop condition always in the first matching one though? If so, then why did the old version have a problem at all? Or maybe there are loops where the condition isn't actually the first one?