// Purpose: tests that while loops in procedures are correctly verified
// Description: The module contains a procedure that increments the input value 10 times, in a while loop. The while loop must have an invariant, and the procedure ensures statement should check that the return value is exactly equal to the input plus 10.
// Expectation: Assertions should all pass
// Validation: Several options: easiest is to remove the WhileLoopRewriter pass.
// Comment: adapted from test-while-0.ucl


module main
{

  procedure add10(x : integer)
    returns (y : integer)
    ensures (y == x + 10);
  {
    var i : integer;
    i = 0;
    y = x;
    while (i < 10)
      invariant (y == x + i);
    {
      y = y + 1;
      i = i + 1;
    }
  }

  control {
    v = verify(add10);
    check;
    print_results;
  }
}
