From 099688555987d05ddbb3ae306e03a490c6a2ad96 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 29 Oct 2025 20:29:25 -0700
Subject: [PATCH] SMV: move logic that distinguishes enums and vars to type
 checker

This moves the logic that distinguishes enums and variables from the parser
to the type checker.

This will enable distinguishing complex identifiers with square brackets
[...] from the index operator.
---
 src/smvlang/parser.y          | 28 ++--------------------------
 src/smvlang/smv_typecheck.cpp | 17 ++++++++++++++---
 2 files changed, 16 insertions(+), 29 deletions(-)

diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 564d5b365..d09130e67 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -952,32 +952,8 @@ identifier : IDENTIFIER_Token
 variable_identifier: complex_identifier
            {
              auto id = merge_complex_identifier(stack_expr($1));
-
-             bool is_enum=(PARSER.module->enum_set.find(id)!=
-                           PARSER.module->enum_set.end());
-             bool is_var=(PARSER.module->vars.find(id)!=
-                          PARSER.module->vars.end());
-
-             if(is_var && is_enum)
-             {
-               yyerror("identifier `"+id2string(id)+"' is ambiguous");
-               YYERROR;
-             }
-             else if(is_enum)
-             {
-               init($$, ID_constant);
-               stack_expr($$).type()=typet(ID_smv_enumeration);
-               stack_expr($$).set(ID_value, id);
-             }
-             else // not an enum, probably a variable
-             {
-               init($$, ID_smv_identifier);
-               stack_expr($$).set(ID_identifier, id);
-               auto var_it = PARSER.module->vars.find(id);
-               if(var_it!= PARSER.module->vars.end())
-                 stack_expr($$).type()=var_it->second.type;
-               //PARSER.module->vars[stack_expr($1).id()];
-             }
+             init($$, ID_smv_identifier);
+             stack_expr($$).set(ID_identifier, id);
            }
            | STRING_Token
            {
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 4e0e58d07..eb9d49e84 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1708,10 +1708,21 @@ void smv_typecheckt::convert(exprt &expr)
     DATA_INVARIANT(
       identifier.find("::") == std::string::npos, "conversion is done once");
 
-    std::string id = module + "::var::" + identifier;
+    // enum or variable?
+    if(modulep->enum_set.find(identifier) == modulep->enum_set.end())
+    {
+      std::string id = module + "::var::" + identifier;
 
-    expr.set(ID_identifier, id);
-    expr.id(ID_symbol);
+      expr.set(ID_identifier, id);
+      expr.id(ID_symbol);
+    }
+    else
+    {
+      expr.id(ID_constant);
+      expr.type() = typet(ID_smv_enumeration);
+      expr.set(ID_value, identifier);
+      expr.remove(ID_identifier);
+    }
   }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")