// Purpose: check that procedures cannot modify their returns
// Description: an empty module with a procedure that modifies its return
// Expectation: There should be a compilation error saying that the procedure modifies its return
// 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) returns (y: integer)
        modifies y;
    {
        y = 0;
    }
}
