unsound: ultimate + cpachecker (undefined behavior)

[chkl]

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern int __VERIFIER_nondet_int(void);
int main()
{
    int k = __VERIFIER_nondet_int();
    int a[1048];
    if (k >= 0 && k < 1048)
    {
        if (a[0] == 23 && a[k] == 42)
        {
            int x = __VERIFIER_nondet_int();
            while (x >= 0)
            {
                __VERIFIER_assert(k != 31241045 && k != -1365206408 && k != 0 && k != 0);
                x = x - k;
            }
        }
    }
    return 0;
}

http://pfm2.mpi-sws.org/program/368588388658cc363a8b8ea1824b63e2faf05218