function call in invariant body #3711

int mk( const int ofs )
{
  int res;
  res = res < 0 ? -res : res;
  res = (res % 128) * 2 + ofs;
  return res;
}  

int in_range( const int n )
{
  return 0 <= n && n < 256;
}  

int main()
{
  int qn;
  int qm;

  //--------------------------------------------------
  // FAILS
  qn = mk(0);
  qm = mk(1);
  
  __ESBMC_loop_invariant(
      0 <= qn && qn < 256 &&
      in_range( qm ) &&
      (qn != qm)
  );
  for (int count = 0; count < 10; count++)
  {
    qn = (qn + 2) % 256;
    qm = (qm + 2) % 256;
  }

  //--------------------------------------------------
  // PASSES
  qn = mk(0);
  qm = mk(1);
  
  __ESBMC_loop_invariant(
      0 <= qn && qn < 256 &&
      (qn != qm) &&
      in_range( qm )
  );
  for (int count = 0; count < 10; count++)
  {
    qn = (qn + 2) % 256;
    qm = (qm + 2) % 256;
  }

  //--------------------------------------------------
  // PASSES
  qn = mk(0);
  qm = mk(1);
  
  __ESBMC_loop_invariant(
      in_range( qm ) &&
      0 <= qn && qn < 256 &&
      (qn != qm)
  );
  for (int count = 0; count < 10; count++)
  {
    qn = (qn + 2) % 256;
    qm = (qm + 2) % 256;
  }
  
  //--------------------------------------------------
  // PASSES
  qn = mk(0);
  qm = mk(1);
  
  __ESBMC_loop_invariant(
      0 <= qn && qn < 256 &&
      0 <= qm && qm < 256 &&
      (qn != qm)
  );
  for (int count = 0; count < 10; count++)
  {
    qn = (qn + 2) % 256;
    qm = (qm + 2) % 256;
  }

}