comparing function pointer with int

[chkl]

e.g. 5485631a2ba9143f1ce4df32b055edcad17ad9e1

void __DUMMY_VERIFIER_error()
{
}
void __DUMMY_VERIFIER_assert(int condition)
{
}
extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
}
void f(void g(int))
{
    g(1);
}
void h(int i)
{
    if (i == 1)
    {
    ERROR:
        __DUMMY_VERIFIER_error();
    }
    else
    {
    }
}
int main(void)
{
    __VERIFIER_assert(h != -137911367);
    f(h);
    return 0;
}

cbmc,seahorn,seacrab : Sat
cpachecker, klee, uautomizer, utaipan: Unsat

[chkl]

The problem is caused by the ERROR label in the h function, close this issue.