#48

[MCFuzzer]

int _br_1 = 0;
void
test (const char *in)
{
  while (1)
    {
      if (*in == 'a')
	{ _br_1++;
	  const char *p = in + 1;
	  if (*p == 'b')
	    { return; }
	  in++;
	} 
    }
}

int main ()
{
  test ("aab");
  _stub();
  return 0;
}
void _stub() { if (!( (_br_1==2) )) __VERIFIER_error(); }

OS: Ubuntu 18.04
Version: latest seahorn/seahorn-llvm5:nightly
Commandline: sea bpf --bmc=mono -O0 --inline FILE.c
Expected result: TRUE
Tool result: FALSE

[kuhar]

_br_3 is undefined but used in test. Possible typo?

[MCFuzzer]

Thank you so much for your report! It's a typo, fixed.