// Purpose: check that procedures cannot modify their parameters
// Description: an empty module with a procedure that modifies its parameter
// Expectation: There should be a compilation error saying that the procedure modifies its parameter
// Validation: removing the check should result in an error on the solver side, if you added a trivial check.

module main {
    procedure f(x: integer)
        modifies x;
    {
        var y: integer;
        y = 0;
    }
}
