smack: `while(nondet_bool)`

[chkl]

5b9d809dbbd123f4beb791107acaa33dea824607 (./c/loops/nec11_false-unreach-call_false-termination.i)

[chkl]

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

int main()
{
    int x = 0;
    while (1)
    {
        if (x == 4)
        {
            x = 0;
        }
        __VERIFIER_assert(x != 2);
        x++;
    }
    return 1;
}
~ 

Apparently, it's not connected to the nondet but to a potentially infinite loop.

[chkl]

can be solved by increasing the unroll bound --unroll=3 as zvonimir pointed out. Weirdly I cannot find that parameter in the SV-comp benchmark defintions. Probably, hard-coded in the sv-comp submission.

103