SE547: CBMC: CBMC Algorithm [8/19]

2) Preprocess the program: just left with functions, loops, if, goto and assignment.

void test (int x, int y) {
  int i; int z; z=0;
  assume (x < y);
  i=x;
  while (i<y) { z=z+1; i=i+1; }
  assert (z > 0);
}