smack: `i != 1` in small loop

[chkl]

81b1bd637f45be4cc680ccb90d8473331ce60b3a (./c/reducercommutativity/sum40_true-unreach-call.i)

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
extern int __VERIFIER_nondet_int();
int sum(int x[40])
{
    int i;
    long long ret;
    ret = 0;
    for (i = 0; i < 40; i++)
    {
        ret = ret + x[i];
    }
    return ret;
}
int main()
{
    int x[40];
    int temp;
    int ret;
    int ret2;
    int ret5;
    for (int i = 0; i < 40; i++)
    {
        x[i] = __VERIFIER_nondet_int();
    }
    ret = sum(x);
    temp = x[0];
    x[0] = x[1];
    x[1] = temp;
    ret2 = sum(x);
    temp = x[0];
    for (int i = 0; i < 40 - 1; i++)
    {
        __VERIFIER_assert(i != 1);
        x[i] = x[i + 1];
    }
    x[40 - 1] = temp;
    ret5 = sum(x);
    if (ret != ret2 || ret != ret5)
    {
        __DUMMY_VERIFIER_error();
    }
    return 1;
}

cbmc/klee : Sat
smack : Unsat
rest : Unknown

[chkl]

This boils down to something like this:

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
extern int __VERIFIER_nondet_int();

int main()
{

    for (int i = 0; i < 7; i++)
    {
        __VERIFIER_assert(i != 1);
    }
    return 1;
}

Seriously?

[chkl]

Also related to a default unroll bound of 1 (#103 )