// Purpose: test that modules with the same name are correctly combined
// Description: two main modules. The first has one variable x, which it initialises to be equal to 1 in the init block. It has an empty next block. The second module has a next block, which increments x by 1, and an invariant that asserts that x is always equal to 1. The second module also contains a control block which checks the property by induction.

// Expectation: Verification should fail.
// Validation: Inserting a bug into module combination where blocks are not correctly combined will cause verification to fail.
// Comment: existing bug in UCLID5

module main {
    var x: integer;

    init {
        x = 1;
    }

    next{}
}

module main {

    next {
        x' = x + 1;
    }

    invariant x_eq_y: x == 1;

    control {
        v = induction;
        check;
        print_results;
    }
}
