// Purpose: tests that if we import types from a module, they must not have the same names as other things in the module we import them to
// 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 an error that the variable is redeclared.
// Validation: Commenting out lines 48-52 and 54 of SemanticAnalyzer.scala removes the error.


module module1 {
    type y = integer;
}

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

    var x: y;
    var y: integer;
    init {
    	x = 0;
    }

    next{
    }

    invariant foo: x==0;

    control{
    	unroll(3);
    }

}
