Handle loop statement comparison between two variables in loop unrolling

[karoliineh]

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.

[sim642]

Theoretically it would be possible to lift this from the option monad to the list monad for non-determinism and return both here. Then the following checks getsPointedAt, constBefore, etc would filter it down to the one that meets all the conditions (although I guess both could still pass all of them).
It would automatically achieve backtracking instead of what currently happens: if the first one doesn't pass getPointedAt, we don't retry everything with the second variable.

I don't know if it would be worth the trouble though.