diff --git a/regression/smv/smv-netlist/smv_netlist1.desc b/regression/smv/smv-netlist/smv_netlist1.desc
index f2978c8b5..7e4587730 100644
--- a/regression/smv/smv-netlist/smv_netlist1.desc
+++ b/regression/smv/smv-netlist/smv_netlist1.desc
@@ -2,7 +2,7 @@ CORE
 smv_netlist1.v
 --smv-netlist
 ^VAR Verilog\.main\.my-bit: boolean;$
-^VAR Verilog\.main\.clk: boolean;$
+^IVAR Verilog\.main\.clk: boolean;$
 ^ASSIGN next\(Verilog\.main\.my-bit\):=!Verilog\.main\.my-bit;$
 ^INIT !Verilog\.main\.my-bit$
 ^EXIT=0$
diff --git a/src/ebmc/output_smv_word_level.cpp b/src/ebmc/output_smv_word_level.cpp
index ba7081074..c54c3b779 100644
--- a/src/ebmc/output_smv_word_level.cpp
+++ b/src/ebmc/output_smv_word_level.cpp
@@ -81,8 +81,13 @@ static void smv_state_variables(
 
     if(symbol.is_state_var)
     {
-      out << "VAR " << symbol.base_name << " : "
-          << smv_type_printert{symbol.type} << ";\n";
+      if(symbol.is_input)
+        out << "IVAR";
+      else
+        out << "VAR";
+
+      out << ' ' << symbol.base_name << " : " << smv_type_printert{symbol.type}
+          << ";\n";
       found = true;
     }
   }
diff --git a/src/trans-netlist/smv_netlist.cpp b/src/trans-netlist/smv_netlist.cpp
index 61244e9d0..1ddba0ea3 100644
--- a/src/trans-netlist/smv_netlist.cpp
+++ b/src/trans-netlist/smv_netlist.cpp
@@ -157,7 +157,7 @@ void smv_netlist(const netlistt &netlist, std::ostream &out)
     {
       if(var.is_input())
       {
-        out << "VAR " << id2smv(var_it.first);
+        out << "IVAR " << id2smv(var_it.first);
         if(var.bits.size() != 1)
           out << "[" << i << "]";
         out << ": boolean;" << '\n';