ApronAnalysis doesnt work on certain loops

[Nimmseasy]

With the following loop implementation apron wasn't able to provide meaningful analysis for loop1, loop2 or res

int main()
{
    int rows = 3;
    int columns = 4;
    int i = 1;
    int loop1;
    int loop2;
    int res; 

    loop1 = 0;
    while (1)
    {
        loop1 = loop1 + 1;
        res = loop1;
        if (i > rows) break;
        int j = 1;

        loop2 = 0;
        while (1)
        {
            loop2 = loop2 + 1;
            res = loop2;
            if (j > columns) break;
            printf("(%d, %d) ", i, j);
            j++;
        }

        printf("\n");
        i++;
    }

    return 0;
}

This is the result of apron after res=loop1;, with the following options --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --enable warn.debug

if we implement the loop as the typical while (i<=columns) or place the break condition before everything else apron gives a meaningful analysis

[sim642]

This might not be the fault of apron analysis per se because this example involves nested loops, which are known to produce more difficult examples for solvers (by demanding local restarting). Another fault might be polyhedra widenings which aren't very precise (without thresholds) and the lack of polyhedra narrowings.

[sim642]

I guess by meaningful analysis you mean Apron should find loop1 == i (or offset by one, depending on the node). With --set sem.int.signed_overflow assume_none it also does, so the problem is that loop1 has no upper bound after widening, so loop1++ loses the constraint.