// Purpose: test that multiple modules with the same name are correctly combined
// Description: four main modules. The first has one variable x, the second has one variable y, the third has an invariant that x == y, and the fourth has a control block that runs induction. The variables x and y both start at 1. At every step, the value of x and y are incremented by 1.
// Expectation: Verification should pass.
// Validation: Inserting a bug into module combination where blocks are not correctly combined will cause verification to fail.

module main {
    var x: integer;

    init {
        y = 1;
    }

    next {
        x' = y + 1;
    }
}

module main {
    var y: integer;

    init {
        x = 1;
    }

    next {
        y' = x + 1;
    }
}

module main {
    invariant x_eq_y: x == y;
}

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