From 2b92edc36cca48737e409c56d3055d7cb7be9917 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 4 Jun 2025 15:36:11 -0700
Subject: [PATCH] remove ltl_sva_to_stringt::resultt::e

This removes an unused member from ltl_sva_to_stringt::resultt.
---
 src/temporal-logic/ltl_sva_to_string.cpp | 30 ++++++++----------------
 src/temporal-logic/ltl_sva_to_string.h   |  4 +---
 2 files changed, 11 insertions(+), 23 deletions(-)

diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
index 7523956b..ea54e4ac 100644
--- a/src/temporal-logic/ltl_sva_to_string.cpp
+++ b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -35,13 +35,10 @@ ltl_sva_to_stringt::suffix(std::string s, const exprt &expr, modet mode)
 {
   auto op_rec = rec(to_unary_expr(expr).op(), mode);
 
-  auto new_e = to_unary_expr(expr);
-  new_e.op() = op_rec.e;
-
   if(op_rec.p == precedencet::ATOM || op_rec.p == precedencet::SUFFIX)
-    return resultt{precedencet::SUFFIX, op_rec.s + s, new_e};
+    return resultt{precedencet::SUFFIX, op_rec.s + s};
   else
-    return resultt{precedencet::SUFFIX, '(' + op_rec.s + ')' + s, new_e};
+    return resultt{precedencet::SUFFIX, '(' + op_rec.s + ')' + s};
 }
 
 ltl_sva_to_stringt::resultt
@@ -49,13 +46,10 @@ ltl_sva_to_stringt::prefix(std::string s, const exprt &expr, modet mode)
 {
   auto op_rec = rec(to_unary_expr(expr).op(), mode);
 
-  auto new_e = to_unary_expr(expr);
-  new_e.op() = op_rec.e;
-
   if(op_rec.p == precedencet::ATOM || op_rec.p == precedencet::PREFIX)
-    return resultt{precedencet::PREFIX, s + op_rec.s, new_e};
+    return resultt{precedencet::PREFIX, s + op_rec.s};
   else
-    return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')', new_e};
+    return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')'};
 }
 
 ltl_sva_to_stringt::resultt
@@ -63,9 +57,8 @@ ltl_sva_to_stringt::infix(std::string s, const exprt &expr, modet mode)
 {
   std::string result;
   bool first = true;
-  exprt new_e = expr; // copy
 
-  for(auto &op : new_e.operands())
+  for(auto &op : expr.operands())
   {
     if(first)
       first = false;
@@ -73,7 +66,6 @@ ltl_sva_to_stringt::infix(std::string s, const exprt &expr, modet mode)
       result += s;
 
     auto op_rec = rec(op, mode);
-    op = op_rec.e;
 
     if(op_rec.p == precedencet::ATOM)
       result += op_rec.s;
@@ -81,7 +73,7 @@ ltl_sva_to_stringt::infix(std::string s, const exprt &expr, modet mode)
       result += '(' + op_rec.s + ')';
   }
 
-  return resultt{precedencet::INFIX, result, new_e};
+  return resultt{precedencet::INFIX, result};
 }
 
 ltl_sva_to_stringt::resultt
@@ -110,12 +102,12 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   else if(expr.is_true())
   {
     // 1 is preferred, but G1 is parsed as an atom
-    return resultt{precedencet::ATOM, "true", expr};
+    return resultt{precedencet::ATOM, "true"};
   }
   else if(expr.is_false())
   {
     // 0 is preferred, but G0 is parsed as an atom
-    return resultt{precedencet::ATOM, "false", expr};
+    return resultt{precedencet::ATOM, "false"};
   }
   else if(expr.id() == ID_F)
   {
@@ -297,7 +289,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // weak closure
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
     auto op_rec = rec(sequence, SVA_SEQUENCE);
-    return resultt{precedencet::ATOM, '{' + op_rec.s + '}', expr};
+    return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
   }
   else if(expr.id() == ID_sva_or)
   {
@@ -539,9 +531,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // a0, a1, a2, a3, a4, ...
     std::string s = "a" + std::to_string(number);
 
-    symbol_exprt new_e{s, expr.type()};
-
-    return resultt{precedencet::ATOM, s, new_e};
+    return resultt{precedencet::ATOM, s};
   }
   else
     throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi";
diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h
index 37a74639..e2a0dfca 100644
--- a/src/temporal-logic/ltl_sva_to_string.h
+++ b/src/temporal-logic/ltl_sva_to_string.h
@@ -34,13 +34,11 @@ class ltl_sva_to_stringt
 
   struct resultt
   {
-    resultt(precedencet _p, std::string _s, exprt _e)
-      : p(_p), s(std::move(_s)), e(std::move(_e))
+    resultt(precedencet _p, std::string _s) : p(_p), s(std::move(_s))
     {
     }
     precedencet p;
     std::string s;
-    exprt e;
   };
 
   numberingt<exprt, irep_hash> atoms;