diff --git a/regression/smv/enums/name_collision1.desc b/regression/smv/enums/name_collision1.desc
new file mode 100644
index 000000000..fa029e06d
--- /dev/null
+++ b/regression/smv/enums/name_collision1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+name_collision1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This crashes.
diff --git a/regression/smv/enums/name_collision1.smv b/regression/smv/enums/name_collision1.smv
new file mode 100644
index 000000000..e84e1c4a5
--- /dev/null
+++ b/regression/smv/enums/name_collision1.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_var: { red, green, yellow, off };
+
+-- identifier already used
+VAR red : boolean;
diff --git a/regression/smv/enums/name_collision2.desc b/regression/smv/enums/name_collision2.desc
new file mode 100644
index 000000000..7bc17f348
--- /dev/null
+++ b/regression/smv/enums/name_collision2.desc
@@ -0,0 +1,9 @@
+CORE
+name_collision2.smv
+
+^file .* line 8: enum red already declared, at file .* line 3$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/smv/enums/name_collision2.smv b/regression/smv/enums/name_collision2.smv
new file mode 100644
index 000000000..44430726e
--- /dev/null
+++ b/regression/smv/enums/name_collision2.smv
@@ -0,0 +1,8 @@
+MODULE main
+
+VAR red : boolean;
+
+-- The identifier "red" is already used.
+-- NuSMV doesn't error this, but yields an error when attempting
+-- to use the identifier.
+VAR some_var: { red, green, yellow, off };
diff --git a/regression/smv/enums/name_collision3.desc b/regression/smv/enums/name_collision3.desc
new file mode 100644
index 000000000..91c3ea2f6
--- /dev/null
+++ b/regression/smv/enums/name_collision3.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+name_collision3.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This crashes.
diff --git a/regression/smv/enums/name_collision3.smv b/regression/smv/enums/name_collision3.smv
new file mode 100644
index 000000000..566350d6b
--- /dev/null
+++ b/regression/smv/enums/name_collision3.smv
@@ -0,0 +1,9 @@
+MODULE submodule
+
+MODULE main
+
+VAR some_var: { red, green, yellow, off };
+
+-- identifier already used
+VAR red : submodule;
+
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index c6e1ee639..d2e37796c 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -676,6 +676,11 @@ enum_element: IDENTIFIER_Token
            {
              $$=$1;
              PARSER.module->enum_set.insert(stack_expr($1).id_string());
+
+             exprt expr(ID_symbol);
+             expr.set(ID_identifier, stack_expr($1).id());
+             PARSER.set_source_location(expr);
+             PARSER.module->add_enum(std::move(expr));
            }
            ;
 
diff --git a/src/smvlang/smv_parse_tree.cpp b/src/smvlang/smv_parse_tree.cpp
index ad780c5f8..8af63bb84 100644
--- a/src/smvlang/smv_parse_tree.cpp
+++ b/src/smvlang/smv_parse_tree.cpp
@@ -74,6 +74,8 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
   case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS";
   case smv_parse_treet::modulet::itemt::DEFINE:
     return "DEFINE";
+  case smv_parse_treet::modulet::itemt::ENUM:
+    return "ENUM";
   case smv_parse_treet::modulet::itemt::VAR:
     return "VAR";
 
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index df48c9185..610e61ee8 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -48,6 +48,7 @@ class smv_parse_treet
         ASSIGN_NEXT,
         CTLSPEC,
         DEFINE,
+        ENUM,
         FAIRNESS,
         INIT,
         INVAR,
@@ -127,6 +128,11 @@ class smv_parse_treet
         return item_type==INIT;
       }
 
+      bool is_enum() const
+      {
+        return item_type == ENUM;
+      }
+
       bool is_var() const
       {
         return item_type == VAR;
@@ -261,6 +267,12 @@ class smv_parse_treet
       items.emplace_back(itemt::VAR, std::move(expr), std::move(location));
     }
 
+    void add_enum(exprt expr)
+    {
+      auto location = expr.source_location();
+      items.emplace_back(itemt::ENUM, std::move(expr), std::move(location));
+    }
+
     mc_varst vars;
     enum_sett enum_set;
 
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 7ec964c8b..3d03f1b2b 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1877,6 +1877,7 @@ void smv_typecheckt::typecheck(
     item.equal_expr().type() = bool_typet{};
     return;
 
+  case smv_parse_treet::modulet::itemt::ENUM:
   case smv_parse_treet::modulet::itemt::VAR:
     return;
   }
@@ -1984,6 +1985,19 @@ void smv_typecheckt::create_var_symbols(
 
       symbol_table.insert(std::move(symbol));
     }
+    else if(item.is_enum())
+    {
+      irep_idt base_name = to_symbol_expr(item.expr).get_identifier();
+      irep_idt identifier = module + "::var::" + id2string(base_name);
+
+      auto symbol_ptr = symbol_table.lookup(identifier);
+      if(symbol_ptr != nullptr)
+      {
+        throw errort{}.with_location(item.expr.source_location())
+          << "enum " << base_name << " already declared, at "
+          << symbol_ptr->location;
+      }
+    }
   }
 }