From 4734687458703b5e9540cf1e7f008b51bde63442 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 10 Nov 2025 12:30:25 -0800
Subject: [PATCH] SMV: ID for smv_cases

This adds an irep ID for "smv_cases".
---
 src/hw_cbmc_irep_ids.h        | 1 +
 src/smvlang/parser.y          | 2 +-
 src/smvlang/smv_typecheck.cpp | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index cdfce027b..bf8fdad18 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -21,6 +21,7 @@ IREP_ID_ONE(smv_abs)
 IREP_ID_ONE(smv_bitimplies)
 IREP_ID_ONE(smv_bit_selection)
 IREP_ID_ONE(smv_bool)
+IREP_ID_ONE(smv_cases)
 IREP_ID_ONE(smv_count)
 IREP_ID_ONE(smv_enumeration)
 IREP_ID_ONE(smv_extend)
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 47b06e0cd..6bf8cb6eb 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -949,7 +949,7 @@ complex_identifier:
            ;
 
 cases      :
-           { init($$, "smv_cases"); }
+           { init($$, ID_smv_cases); }
            | cases case
            { $$=$1; mto($$, $2); }
            ;
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 91a68783c..555164633 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1955,7 +1955,7 @@ void smv_typecheckt::convert(exprt &expr)
 
     expr.id(ID_constraint_select_one);
   }
-  else if(expr.id()=="smv_cases") // cases
+  else if(expr.id() == ID_smv_cases) // cases
   {
     if(expr.operands().size()<1)
     {