SMV: error on duplicate module names

regression/smv/modules/duplicate_module1.desc

@@ -0,0 +1,7 @@
+CORE
+duplicate_module1.smv
+
+^file .* line 10: duplicate module name `main'$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/smv/modules/duplicate_module1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR x : boolean;
+
+MODULE other
+
+VAR y : boolean;
+
+-- duplicate of main
+MODULE main
+
+VAR z : boolean;

src/smvlang/smv_typecheck.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <set>
 #include <stack>
+#include <unordered_set>
 
 class smv_typecheckt:public typecheckt
 {
@@ -3214,6 +3215,19 @@ void smv_typecheckt::typecheck()
   if(module_identifier != "smv::main")
     return;
 
+  // check for duplicate module names
+  {
+    std::unordered_set<irep_idt, irep_id_hash> module_names;
+    for(const auto &module : smv_parse_tree.module_list)
+    {
+      if(!module_names.insert(module.base_name).second)
+      {
+        throw errort().with_location(module.source_location)
+          << "duplicate module name `" << module.base_name << "'";
+      }
+    }
+  }
+
   // build the index
   index = smv_indext{smv_parse_tree};