unsoundness: crab-llvm (recursive function)

[chkl]

extern int __VERIFIER_nondet_int();
extern void __VERIFIER_error();
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
int fibo(int n)
{
    __VERIFIER_assert(n != 0);
    if (n < 1)
    {
        return 0;
    }
    else if (n == 1)
    {
        return 1;
    }
    else
    {
        return fibo(n - 1) + fibo(n - 2);
    }
}
int main(void)
{
    int x = 10;
    int result = fibo(x);

    return 0;
}

crab-llvm says "unsat".

[chkl]

https://github.com/seahorn/crab-llvm/issues/20