// Purpose: tests that importing types from a module only imports types
// Description: This test has two modules. A submodule defines a type and a variable. The main module defines a variable with the same name as the variable in the submodule, and imports the types from the submodule, and uses the type.
// Expected: UCLID will throw no errors.
// Validation: If we comment out  passManager.addPass(new ModuleTypesImportCollector()) in UclidMain.scala, we will see an error that type T was used without declaration.


module module1 {
    type T = integer;
    var x: integer;
}

// Import types from module1
module main {
    type * = module1.*;

    var x: T;
    init {
    	x = 0;
    }

    next{
    }

    invariant foo: x==0;

    control{
    	unroll(3);
    }

}
