module Module {
  var x: integer;
  var x1: integer;
  var x2: integer;
  var x3: integer;

  procedure step()
    modifies x1;
    modifies x2;
    modifies x3;
    modifies x;
  {
    x1 = x1;
    x1 = (x1 + 1);
    x2 = x2;
    x2 = (x2 + 1);
    x3 = x3;
    x3 = (x3 + 1);
    x = x1;
    x = x2;
    x = x3;
  }

  next {
    call step();
  }
  invariant spec: (x == 2);

}
