[unsoundness/undefined-behavior] crab-llvm, uninitialized variable

[chkl]

extern void __VERIFIER_error() __attribute__((__noreturn__));
extern void __VERIFIER_assume(int);
void __VERIFIER_assert(int cond)
{
    if (!cond)    {
    ERROR:
        __VERIFIER_error();
    }
}
extern int __VERIFIER_nondet_int(void);

int main()
{
    int x  = __VERIFIER_nondet_int();
    if (x > 1) {
        int i;
        __VERIFIER_assert(i >= x);
    }
    return 1;
}

crab-llvm says "unsat", whereas all other verifiers say "sat".

There are a lot of those cases.

[chkl]

It's undefined behavior nonetheless it is curious that crab-llvm disagrees with seahorn. Question asked here: https://github.com/seahorn/crab-llvm/issues/20