SE547: CBMC: CBMC Algorithm [11/19]

5) Calculate the constraints of the program C, and the properties we're checking of the program P.

Constraints:

  z0=0;
  x0 < y0;
  i0=x0;
  i0<y0 => z1=z0+1;  i0<y0 => i1=i0+1; 
  z2=(i0<y0?z1,z0); i2=(i0<y0?i1,i0);
  i2<y0 => z3=z2+1;  i2<y0 => i3=i0+1; 
  z4=(i2<y0?z3,z2); i4=(i2<y0?i3,i2);
  i4<y0 => z5=z4+1;  i4<y0 => i5=i0+1; 
  z6=(i4<y0?z5,z4); i6=(i4<y0?i5,i4);
  i6<y0 => false

Properties:

  z6 > 0;