SMV: fix traces of models with module instances

This removes identifiers that denote module instances from traces of SMV
models.

Author: kroening

regression/smv/modules/trace1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 trace1.smv
 --numbered-trace
 ^\[.*\] AG \!a\.c\.d: REFUTED$
@@ -16,6 +16,4 @@ trace1.smv
 ^a@1 = .*$
 ^b@1 = .*$
 ^a.c@1 = .*$
-^b.d@1 = .*$
 --
-The trace contains entries for the module instances.

src/trans-netlist/trans_to_netlist.cpp

@@ -225,7 +225,8 @@ void convert_trans_to_netlistt::map_vars(
     }
     else if(
       symbol.type.id() == ID_module || symbol.type.id() == ID_module_instance ||
-      symbol.type.id() == ID_primitive_module_instance)
+      symbol.type.id() == ID_primitive_module_instance ||
+      symbol.type.id() == ID_smv_module_instance)
     {
       return; // ignore modules
     }

src/trans-word-level/trans_trace_word_level.cpp

@@ -53,10 +53,11 @@ trans_tracet compute_trans_trace(
     {
       const symbolt &symbol=ns.lookup(it->second);
 
-      if(!symbol.is_type &&
-         !symbol.is_property &&
-         symbol.type.id()!=ID_module &&
-         symbol.type.id()!=ID_module_instance)
+      if(
+        !symbol.is_type && !symbol.is_property &&
+        symbol.type.id() != ID_module &&
+        symbol.type.id() != ID_module_instance &&
+        symbol.type.id() != ID_smv_module_instance)
       {
         if(symbol.is_macro)
         {