SMV output: use IVAR

The SMV netlist and SMV word-level output now use IVAR for input variables.

Author: kroening

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$

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;
     }
   }

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';