// Purpose: test that procedure verification with a simple while loop works
// Description: a module with a single procedure. The procedure has a local variable x and returns a value y. The procedure begins by assigning 1 to x, and then loops while x is less than 10. The loop body increments x by 1. The procedure ends by assigning the value of x to y and returning y. We then verify that the procedure always returns 10.
// Expectation: verification should pass
// Validation: inserting a bug into how while loops are handled in the verifier should cause verification to fail. For example, not accounting for the body of the loop after the loop condition is met.

module main {
    procedure p ()
        returns (y: integer)
        ensures y == 10;
    {
        var x: integer;
        x = 1;
        while (x < 10) {
            x = x + 1;
        }
        y = x;
    }

    control {
        verify(p);
        check;
        print_results;
    }
}
