From 81ee95dc0e9b5aff205ff703f2a9b13e3c387b47 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 27 Jul 2025 13:51:44 -0700
Subject: [PATCH] SMV: submodules are now taken from module items

This avoids the use of the vars map in the parse tree.
---
 src/smvlang/smv_typecheck.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 059dbbf3a..3afe2a5c6 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -192,21 +192,22 @@ Function: smv_typecheckt::flatten_hierarchy
 
 void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
 {
-  for(auto &var_it : smv_module.vars)
+  for(auto &item : smv_module.items)
   {
-    smv_parse_treet::mc_vart &var = var_it.second;
-
-    if(var.type.id()=="submodule")
+    if(item.is_var() && item.expr.type().id() == "submodule")
     {
-      exprt &inst=static_cast<exprt &>(static_cast<irept &>(var.type));
+      exprt &inst =
+        static_cast<exprt &>(static_cast<irept &>(item.expr.type()));
 
       for(auto &op : inst.operands())
         convert(op, NORMAL);
 
+      auto instance_base_name = to_symbol_expr(item.expr).get_identifier();
+
       instantiate(
         smv_module,
         inst.get(ID_identifier),
-        var_it.first,
+        instance_base_name,
         inst.operands(),
         inst.find_source_location());
     }