diff --git a/regression/smv/modules/self1.desc b/regression/smv/modules/self1.desc
index de780717d..1f2bdd045 100644
--- a/regression/smv/modules/self1.desc
+++ b/regression/smv/modules/self1.desc
@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 self1.smv
 
-^EXIT=0$
+^file .* line 4: no support for self$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This does not parse.
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index fc1bdcf6a..00497e678 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -36,6 +36,7 @@ IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(smv_range)
 IREP_ID_ONE(smv_resize)
 IREP_ID_ONE(smv_toint)
+IREP_ID_ONE(smv_self)
 IREP_ID_ONE(smv_set)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index d71ea3c96..8913fa500 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -738,6 +738,11 @@ basic_expr : constant
              unary($$, ID_member, $1);
              stack_expr($$).set(ID_component_name, stack_expr($3).id());
            }
+           | self_Token
+           {
+             // This rule is part of "complex_identifier" in the NuSMV manual.
+             init($$, ID_smv_self);
+           }
            | basic_expr '(' basic_expr ')'
            {
              // Not in the NuSMV grammar.
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index e80f10e30..b36b45f9a 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1928,6 +1928,11 @@ void smv_typecheckt::convert(exprt &expr)
     tmp.set_identifier(id2string(tmp.get_identifier()) + '.' + index_string);
     expr = tmp;
   }
+  else if(expr.id() == ID_smv_self)
+  {
+    throw errort().with_location(expr.source_location())
+      << "no support for self";
+  }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")
   {