Previously, we only detected fixed-sized loops when the loop comparison was between a variable and a constant. However, we already found the last assignment to the variable being changed in the loop body, and thus, we have a function for finding the last assigned value.

This PR adds the functionality also to detect fixed loops when the loop condition compares variables by finding the last assignment for the other compared variable.

This PR was inspired by the following loop from the SV-COMP task loops/invert_string-3.c, which we were lucky to solve based on the old heuristics but cannot solve anymore due to the new, more conservative heuristic.

unsigned int max = 5;
char str1[max], str2[max];
int i, j;

for (i=0; i<max; i++) {
    str1[i]=__VERIFIER_nondet_char();
}

This task has the case including a cast. I added another case that would handle similar conditions without a cast as a precaution.