SE547: CBMC: CBMC Algorithm [9/19]

3) Unwind function calls and loops: just left with if, forward goto and assignment.

void test (int x, int y) {
  int i; int z; z=0;
  assume (x < y);
  i=x;
  if (i<y) { z=z+1; i=i+1; }
  if (i<y) { z=z+1; i=i+1; }
  if (i<y) { z=z+1; i=i+1; }
  if (i<y) { assume (false); } // what is this doing here?
  assert (z > 0);
}

This is for --unwind 3 --no-unwinding-assertions.