diff --git a/regression/smv/modules/module_with_enum1.desc b/regression/smv/modules/module_with_enum1.desc
index 65c4a3a1e..c084046a6 100644
--- a/regression/smv/modules/module_with_enum1.desc
+++ b/regression/smv/modules/module_with_enum1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-smt-backend
 module_with_enum1.smv
 
 ^EXIT=0$
@@ -6,4 +6,3 @@ module_with_enum1.smv
 --
 ^warning: ignoring
 --
-The enum literal is not found.
diff --git a/regression/smv/modules/module_with_enum2.desc b/regression/smv/modules/module_with_enum2.desc
new file mode 100644
index 000000000..adef84fe6
--- /dev/null
+++ b/regression/smv/modules/module_with_enum2.desc
@@ -0,0 +1,9 @@
+CORE
+module_with_enum2.smv
+
+^file .* line 11: enum a already declared, at file .* line 7$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/smv/modules/module_with_enum2.smv b/regression/smv/modules/module_with_enum2.smv
new file mode 100644
index 000000000..31654c080
--- /dev/null
+++ b/regression/smv/modules/module_with_enum2.smv
@@ -0,0 +1,13 @@
+MODULE main
+
+VAR sub : my-module;
+
+-- There is an enum in another module with the same identifier,
+-- which is an error!
+VAR a : boolean;
+
+MODULE my-module
+
+VAR some_enum : { a, b };
+
+ASSIGN some_enum := a;
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 997f1170b..6ab873594 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -664,7 +664,7 @@ enum_list  : enum_element
 enum_element: IDENTIFIER_Token
            {
              $$=$1;
-             PARSER.module->enum_set.insert(stack_expr($1).id_string());
+             PARSER.parse_tree.enum_set.insert(stack_expr($1).id_string());
              PARSER.module->add_enum(
                smv_identifier_exprt{stack_expr($1).id(), PARSER.source_location()});
            }
@@ -907,6 +907,7 @@ identifier : IDENTIFIER_Token
 
 variable_identifier: complex_identifier
            {
+             // Could be a variable, or an enum
              auto id = merge_complex_identifier(stack_expr($1));
              init($$, ID_smv_identifier);
              stack_expr($$).set(ID_identifier, id);
diff --git a/src/smvlang/smv_parse_tree.cpp b/src/smvlang/smv_parse_tree.cpp
index 6ebfa02b8..2b6747311 100644
--- a/src/smvlang/smv_parse_tree.cpp
+++ b/src/smvlang/smv_parse_tree.cpp
@@ -30,6 +30,7 @@ void smv_parse_treet::swap(smv_parse_treet &smv_parse_tree)
 {
   smv_parse_tree.module_list.swap(module_list);
   smv_parse_tree.module_map.swap(module_map);
+  smv_parse_tree.enum_set.swap(enum_set);
 }
 
 /*******************************************************************\
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index 80500cb9b..7d4cf34d8 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -291,8 +291,6 @@ class smv_parse_treet
       elements.emplace_back(
         elementt::ENUM, std::move(expr), std::move(location));
     }
-
-    enum_sett enum_set;
   };
 
   using module_listt = std::list<modulet>;
@@ -302,7 +300,10 @@ class smv_parse_treet
     std::unordered_map<irep_idt, module_listt::iterator, irep_id_hash>;
   module_mapt module_map;
 
-  void swap(smv_parse_treet &smv_parse_tree);
+  // enums are global
+  enum_sett enum_set;
+
+  void swap(smv_parse_treet &);
   void clear();
 
   void show(std::ostream &) const;
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 4a3f9647d..d8137836d 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -277,9 +277,9 @@ void smv_typecheckt::instantiate(
     auto copy = src_element;
 
     // replace the parameter identifiers,
-    // and add the prefix to non-parameter identifiers
+    // and add the prefix to non-parameter, non-enum identifiers
     copy.expr.visit_post(
-      [&parameter_map, &prefix](exprt &expr)
+      [&parameter_map, &prefix, this](exprt &expr)
       {
         if(expr.id() == ID_smv_identifier)
         {
@@ -287,8 +287,15 @@ void smv_typecheckt::instantiate(
           auto parameter_it = parameter_map.find(identifier);
           if(parameter_it != parameter_map.end())
           {
+            // It's a parameter
             expr = parameter_it->second;
           }
+          else if(
+            smv_parse_tree.enum_set.find(identifier) !=
+            smv_parse_tree.enum_set.end())
+          {
+            // It's an enum, leave as is
+          }
           else
           {
             // add the prefix
@@ -1774,7 +1781,8 @@ void smv_typecheckt::convert(exprt &expr)
       identifier.find("::") == std::string::npos, "conversion is done once");
 
     // enum or variable?
-    if(modulep->enum_set.find(identifier) == modulep->enum_set.end())
+    if(
+      smv_parse_tree.enum_set.find(identifier) == smv_parse_tree.enum_set.end())
     {
       std::string id = module + "::var::" + identifier;