smack: reach uneven number

[chkl]

7a9ab5cae91070e39be23efe64bf3acb093e7948 (./c/bitvector/jain_2_false-no-overflow.i)

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
extern int __VERIFIER_nondet_int(void);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int main()
{
    int x, y;
    x = 1;
    y = 1;
    while (1)
    {
        __VERIFIER_assert(x != 152129);
        x = x + 2 * __VERIFIER_nondet_int();
        y = y + 2 * __VERIFIER_nondet_int();
        __DUMMY_VERIFIER_assert(x + y != 1);
    }
    return 0;
}

cpachecker/sea* : Sat
smack: Unsat
rest : Unknown

[chkl]

minimal working example:

extern void __VERIFIER_error() __attribute__((__noreturn__));
extern int __VERIFIER_nondet_int(void);
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
int main()
{
    int x;
    x = 1;
    while (1)
    {
        __VERIFIER_assert(x != 9);
        x = x + 2 * __VERIFIER_nondet_int();
    }
    return 0;
}

[chkl]

https://github.com/smackers/smack/issues/324

[chkl]

This is probably due to the same "bug" as #98