// Purpose: check that multiple modules with the same name are correctly combined for procedures.
// Description: three modules called main. The first declares a variable x. The second declares a procedure p that modifies x. The third verifies p.
// Expectation: verification should pass.
// Validation: If procedures are not combined with modules, then this would crash.

module main {
    var x: integer;
}

module main {
    procedure p()
        requires x > 0;
        ensures x > 0;
        modifies x;
    {
        x = x + 1;
    }
}

module main {
    control {
        verify(p);
        check;
        print_results;
    }
}
