diff --git a/CHANGELOG b/CHANGELOG
index 414302293..35b634f35 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,6 +1,7 @@
 # EBMC 5.9
 
 * SMV: word constants
+* SMV: IVAR declarations
 
 # EBMC 5.8
 
diff --git a/regression/smv/ivar/ivar1.desc b/regression/smv/ivar/ivar1.desc
index e6cb0032c..9eee67cbf 100644
--- a/regression/smv/ivar/ivar1.desc
+++ b/regression/smv/ivar/ivar1.desc
@@ -1,8 +1,11 @@
 CORE
 ivar1.smv
-
-^file .* line 3: No support for IVAR declarations$
-^EXIT=1$
+--bound 1
+^\[.*\] some_input: REFUTED$
+^\[.*\] !some_input: REFUTED$
+^\[.*\] X some_input: REFUTED$
+^\[.*\] X !some_input: REFUTED$
+^EXIT=10$
 ^SIGNAL=0$
 --
 --
diff --git a/regression/smv/ivar/ivar1.smv b/regression/smv/ivar/ivar1.smv
index eb9ff90a8..f192a80f4 100644
--- a/regression/smv/ivar/ivar1.smv
+++ b/regression/smv/ivar/ivar1.smv
@@ -1,3 +1,9 @@
 MODULE main
 
 IVAR some_input : boolean;
+
+-- these should all fail
+LTLSPEC some_input
+LTLSPEC !some_input
+LTLSPEC X some_input
+LTLSPEC X !some_input
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index d876587d1..527531336 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -402,10 +402,23 @@ var_declaration:
            ;
 
 ivar_declaration:
-             IVAR_Token simple_var_list
+             IVAR_Token ivar_simple_var_list
+           ;
+
+ivar_simple_var_list:
+             identifier ':' simple_type_specifier ';'
            {
-             yyerror("No support for IVAR declarations");
-             YYERROR;
+             irep_idt identifier = stack_expr($1).id();
+             stack_expr($1).id(ID_smv_identifier);
+             stack_expr($1).set(ID_identifier, identifier);
+             PARSER.module->add_ivar(stack_expr($1), stack_type($3));
+           }
+           | ivar_simple_var_list identifier ':' simple_type_specifier ';'
+           {
+             irep_idt identifier = stack_expr($2).id();
+             stack_expr($2).id(ID_smv_identifier);
+             stack_expr($2).set(ID_identifier, identifier);
+             PARSER.module->add_ivar(stack_expr($2), stack_type($4));
            }
            ;
 
diff --git a/src/smvlang/smv_parse_tree.cpp b/src/smvlang/smv_parse_tree.cpp
index 8af63bb84..3dea7dcd9 100644
--- a/src/smvlang/smv_parse_tree.cpp
+++ b/src/smvlang/smv_parse_tree.cpp
@@ -76,6 +76,8 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
     return "DEFINE";
   case smv_parse_treet::modulet::itemt::ENUM:
     return "ENUM";
+  case smv_parse_treet::modulet::itemt::IVAR:
+    return "IVAR";
   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 610e61ee8..f150515a7 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -52,6 +52,7 @@ class smv_parse_treet
         FAIRNESS,
         INIT,
         INVAR,
+        IVAR,
         LTLSPEC,
         TRANS,
         VAR
@@ -133,6 +134,11 @@ class smv_parse_treet
         return item_type == ENUM;
       }
 
+      bool is_ivar() const
+      {
+        return item_type == IVAR;
+      }
+
       bool is_var() const
       {
         return item_type == VAR;
@@ -260,6 +266,13 @@ class smv_parse_treet
       items.emplace_back(itemt::TRANS, std::move(expr), std::move(location));
     }
 
+    void add_ivar(exprt expr, typet type)
+    {
+      expr.type() = std::move(type);
+      auto location = expr.source_location();
+      items.emplace_back(itemt::IVAR, std::move(expr), std::move(location));
+    }
+
     void add_var(exprt expr, typet type)
     {
       expr.type() = std::move(type);
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 7312d9796..b68d9a016 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -2033,6 +2033,7 @@ void smv_typecheckt::typecheck(
     return;
 
   case smv_parse_treet::modulet::itemt::ENUM:
+  case smv_parse_treet::modulet::itemt::IVAR:
   case smv_parse_treet::modulet::itemt::VAR:
     return;
   }
@@ -2075,7 +2076,7 @@ void smv_typecheckt::create_var_symbols(
 
   for(const auto &item : items)
   {
-    if(item.is_var())
+    if(item.is_var() || item.is_ivar())
     {
       irep_idt base_name = to_smv_identifier_expr(item.expr).identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
@@ -2318,7 +2319,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
     // non-variable items
     for(auto &item : smv_module.items)
-      if(!item.is_var())
+      if(!item.is_var() && !item.is_ivar())
         convert(item);
 
     flatten_hierarchy(smv_module);