cpachecker (comparing uint that was casted to int with MIN_INT)

[chkl]

b957b0d86aab7fb7461306f93f77645b850b04be

void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
extern unsigned int __VERIFIER_nondet_uint();
int main()
{
    int i, n = __VERIFIER_nondet_uint(), sn = 0;
    __VERIFIER_assert(n != -2147483648);
    for (i = 1; i <= n; i++)
    {
        sn = sn + 2;
        if (i == 4)
        {
            sn = -10;
        }
    }
    __DUMMY_VERIFIER_assert(sn == n * 2 || sn == 0);
}

seacrab/seahorn/uautomizer/utaipan: Sat
cbmc: Unknown
cpachecker: Unsat
klee: Unsat

[chkl]

Okay, so this is not a problem when cpachecker is actually called with -32. Somehow that parameter was missing in the glue code. So I'm closing this issue because there's nothing worthy of reporting here.