// Purpose: Tests that groups are imported when an entire module is imported
// Description: The module has two modules. One module defines a group of integers, containing 0,1,2 and 3. The second module imports everything from first module and has a property that checks that all members of the group are less than 4.
// Expectation: property passes
// Validation: Inserting a bug into the ModuleImportRewriter pass will make this fail.

module m1 {
    group myGroup : integer = {0, 1, 2, 3};
}

module main {
    import m1;

    property test1 : finite_forall (int : integer) in myGroup :: int < 4; //Should pass


    control {
        v = unroll(0);
        check;
        print_results;
    }
}
