Merge pull request #1482 from diffblue/use-smv_module_instance_typet

Use `smv_module_instance_typet`

Author: tautschnig

src/smvlang/smv_typecheck.cpp

@@ -206,21 +206,20 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
 
     if(element.is_var() && element.expr.type().id() == ID_smv_module_instance)
     {
-      exprt &inst =
-        static_cast<exprt &>(static_cast<irept &>(element.expr.type()));
+      auto &instance = to_smv_module_instance_type(element.expr.type());
 
-      for(auto &op : inst.operands())
-        convert(op);
+      for(auto &argument : instance.arguments())
+        convert(argument);
 
       auto instance_base_name =
         to_smv_identifier_expr(element.expr).identifier();
 
       instantiate(
         smv_module,
-        inst.get(ID_identifier),
+        instance.identifier(),
         instance_base_name,
-        inst.operands(),
-        inst.find_source_location());
+        instance.arguments(),
+        instance.source_location());
     }
   }
 }

src/smvlang/smv_types.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef CPROVER_SMV_TYPES_H
 #define CPROVER_SMV_TYPES_H
 
+#include <util/expr.h>
 #include <util/type.h>
 
 #include <set>
@@ -90,6 +91,16 @@ class smv_module_instance_typet : public typet
   {
     set(ID_identifier, _identifier);
   }
+
+  const exprt::operandst &arguments() const
+  {
+    return (const exprt::operandst &)get_sub();
+  }
+
+  exprt::operandst &arguments()
+  {
+    return (exprt::operandst &)get_sub();
+  }
 };
 
 /*! \brief Cast a generic typet to a \ref smv_module_instance_typet