SE547: CBMC: CBMC Algorithm [7/19]

1) Start with a C program with assert(...) and assume(...) statements.

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

file:assume-assert.c Is this program OK?