// Purpose: tests that a local variable in the procedure can have the same name as one of the procedure arguments.
// Description: The module defines an inlined procedure called increment, which returns a value that is equal to the input plus one. The procedure is called from two other procedures, f1 and f2. f1 calls the procedure with an input variable that has the same name as the procedure argument. f2 calls the procedure with an input variable that has a different name. Both procedures return the result, and have ensures statements that check the result is equal to the input plus one.
// Expectation: All checks should pass
// Validation: Revert commit 110e8645c6e243795918c7d1a8c4db6e56242f87, or checkout at commit cf31a22644147a4f4b2a3619463bec0d446d318e.
// Comment: v hard. writing this description was hard.

module main {

    procedure [inline] increment(x : integer) returns (y : integer)
    {
        y = x + 1;
    }

    procedure f1(x : integer) returns (y : integer)
        ensures y == x + 1;
    {
        call (y) = increment(x);
    }

    procedure f2(y : integer) returns (x : integer)
        ensures x == y + 1;
    {
        call (x) = increment(y);
    }

    control {
        verify(f1);
        verify(f2);
        check;
        print_results;
    }
}
