SE547: CBMC: CBMC Algorithm [10/19]

4) Rename all variables to be unique.

void test (int x0, int y0) {
  int i0; int z0; int i1; int z1; ... int i6; int z6; z0=0;
  assume (x0 < y0);
  i0=x0;
  if (i0<y0) { z1=z0+1; i1=i0+1; }
  z2=(i0<y0?z1,z0); i2=(i0<y0?i1,i0); // what is this doing here?
  if (i2<y0) { z3=z2+1; i3=i2+1; } 
  z4=(i2<y0?z3,z32; i4=(i2<y0?i3,i2); // what is this doing here?
  if (i4<y0) { z5=z4+1; i5=i4+1; } 
  z6=(i4<y0?z5,z4); i6=(i4<y0?i5,i4); // what is this doing here?
  if (i6<y0) { assume (false); }
  assert (z6 > 0);
}

(If you've taken CSC548: this is SSA form with phi-functions.)