// Purpose: check procedures can't modify inputs
// Description: a module with a single input and a procedure that modifies it.
// Expectation: UCLID5 should give an error saying that procedures can't modify inputs.
// Validation: Removing this check could make this verification pass, which it shouldn't.


module main {
    input x: integer;

    procedure p()
        modifies x;
    {
        x = x + 1;
    }

    init {
        x = 0;
    }

    next {
        call p();
    }

    invariant x_gte_0: x >= 0;

    control {
        induction;
        check;
        print_results;
    }
}
