// Purpose: Check that variable shadowing works correctly
// Description: A module with a single variable y and a procedure f. The procedure declares that it modifies y, but it also declares a local variable y and only modifies that by setting it to 0. Then we have an induction check to see if y is always 0.
// Expectation: The base case should fail and the inductive step should pass.
// Validation: Inserting a bug into the variable shadowing code should cause the verification to pass.

module main {
    var y: integer;

    procedure f()
        modifies y;
    {
        var y: integer;
        y = 0; // this should be modifying the local y, not the global y
    }

    init {
        call f();
    }

    next {
        call f();
    }

    invariant y_is_0: y == 0;

    control {
        induction;
        check;
        print_results;
    }
}
