smack: `b[x] == 42 + x`

[chkl]

68069968d5f31e32ea53cfe836b4b84d4832e746 (./c/array-examples/standard_copyInitSum2_false-unreach-call_ground.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();
    }
}
int main()
{
    int a[100000];
    int b[100000];
    int i = 0;
    while (i < 100000)
    {
        a[i] = 42;
        i = i + 1;
    }
    for (i = 0; i < 100000; i++)
    {
        b[i] = a[i];
    }
    for (i = 0; i < 100000; i++)
    {
        a[i] = b[i] + i;
    }
    int x;
    for (x = 0; x < 100000; x++)
    {
        __VERIFIER_assert(b[x] == 42 + x != 0);
        __DUMMY_VERIFIER_assert(b[x] == 42 + x);
    }
    return 0;
}

There must be some bug, because smack has 23xSat and 88xUnsat.