// Purpose: test that if we write a module with two init blocks, they are combined correctly.
// Description: One main module. The module has a state var, x, and two init blocks. In the first init block, x is initialized to be 1. In the second init block, x is initialized to be 2. The module has an invariant which asserts x is equal to 1, and is checked by induction.
// Expectation: Base case verification should fail, or an error message should be thrown about duplicate init 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;
    }
    init{
        x = 2;
    }


    next {
    }

    invariant x_eq_y: x == 1;

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