// Purpose: test that we can write modules with two next blocks
// Description: One main module. The module has a state var, x, which is initialized to be 1. The module has two next blocks. The first next block is empty, the second next block increments x by 1. The module has an invariant which asserts x is equal to 1, and is checked by induction.
// Expectation: Verification should fail, or an error message should be thrown about duplicate next blocks.
// 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{}

    next {
        x' = x + 1;
    }

    invariant x_eq_y: x == 1;

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