cpachecker: `nd() * 2 != 0`

[chkl]

58353850a096427990395ddbb7d984acc4e1c48f (./c/loops/sum01_true-unreach-call_true-termination.i)

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
extern void __VERIFIER_assume(int cond);
extern void __VERIFIER_assert(int cond);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
extern int __VERIFIER_nondet_int();
int main()
{
    int i, n = __VERIFIER_nondet_int(), sn = 0;
    if (!(n < 1000 && n >= -1000))
    {
        return 0;
    }
    for (i = 1; i <= n; i++)
    {
        sn = sn + 2;
    }
    __VERIFIER_assert(n * 2 != 0);
    __DUMMY_VERIFIER_assert(sn == n * 2 || sn == 0);
}

Seriously cpachecker?

[chkl]

https://groups.google.com/forum/#!topic/cpachecker-users/3JCOeNuoleA

[chkl]

Dear Christian,

thank you for the bug report. The bug is fixed in revision 28476.

Best, Matthias