unsound: sea*/crab-llvm (overflow)

[chkl]

0a64a21f3c6bdad86e8d0fac4317e19dd7900f9f (c/bitvector-regression/recHanoi03_false-unreach-call_true-termination.c)

minimized:

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

int main()
{
    int n = __VERIFIER_nondet_int();
    if (n < 1)
    {
        return 0;
    }
    unsigned result = hanoi(n);
    __VERIFIER_assert(1 << n != 0 );

}

ultimate,cbmc,cpachecker,smack: sat
crab-llvm, seahorn, seacrab,  klee: unsat

I am pretty certain, that the error location is reachable. In fact any number of n greater than 32 should suffice to let 1 << n become zero.

Is that noteworthy? Because for obvious reasons we don't report overflow unsoundness (because nobody checks that).

[wuestholz]

@chkl Yeah, that seems to be caused by overflow or at least some sort of (unsound) modeling of bitwise operations using arithmetic operations.