nevermind

[chkl]

Either I am getting something wrong here or I found a really interesting case:

extern void __VERIFIER_error() __attribute__((__noreturn__));
extern void __VERIFIER_assume(int);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
extern short __VERIFIER_nondet_int(void);
int SIZE;
int main()
{
    SIZE = __VERIFIER_nondet_int();
    if (SIZE > 1)
    {
        long long i = __VERIFIER_nondet_int();
        long long a[SIZE];
        for (i = 0; i < SIZE; i++)
        {
        }
        __VERIFIER_assert(i < SIZE != 1);

    }
    return 1;
}

This is a variation of http://pfm2.mpi-sws.org/program/6dc735f9a438739dfd3a0cb62ccebaaf7eb830c6

At first I thought it is due to undefined behavior, but even when I initialize i with __VERIFIER_nondet_int(), I see the same problem. As the program is above then verdicts are:

unsat: cpachecker, crab-llvm, seahorn, uautomizer
sat: smack
unknown: cbmc, klee

As soon as I rename the local variable in the for loop from i to j the verdicts change to:

unsat: crab-llvm
sat: smack
unknown: cbmc, cpachecker,klee,seacrab,seahorn