sea* assert(false) in loop

[chkl]

165972c7791e89699d38688cedaf52576d6aeb3d (./array-examples/standard_find_ground_false-def-behavior.i)

void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
extern int __VERIFIER_nondet_int();
int main()
{
    int a[100000];
    int e = __VERIFIER_nondet_int();
    int i = 0;
    while (i < 100000 && a[i] != e)
    {
        __VERIFIER_assert(0);
        i = i + 1;
    }
    int x;
    for (x = 0; x < i; x++)
    {
        __DUMMY_VERIFIER_assert(a[x] != e);
    }
    return 0;
}

cbmc: unknown cpachecker/klee/smack/uautomizer/utaipan : sat sea* : unsat

[chkl]

• similar cases with other assertions in the loop.

[chkl]

simplified version with same outcome:

void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
extern int __VERIFIER_nondet_int();
int main()
{
    int a[3];
    int e = __VERIFIER_nondet_int();
    int i = 0;
    while (i < 3 && a[i] != e)
    {
        __VERIFIER_assert(0);
        i = i + 1;
    }
    return 0;
}

It seems to depend on a being an array.

[chkl]

https://github.com/seahorn/seahorn/issues/152