From b7d2b12209a60a8a0af67de5c4bc4d575f689804 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 4 Jun 2025 17:48:21 -0700
Subject: [PATCH] add sequence_matcht::condition()

This adds a wrapper method that returns the condition of a potential SVA
sequence match.
---
 src/trans-word-level/property.cpp | 11 ++++++-----
 src/trans-word-level/sequence.cpp | 10 +++++-----
 src/trans-word-level/sequence.h   | 11 ++++++++---
 3 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index ab63e691..52438370 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -558,7 +558,7 @@ static obligationst property_obligations_rec(
       {
         // The sequence must not match.
         if(!match.empty_match())
-          obligations.add(match.end_time, not_exprt{match.condition});
+          obligations.add(match.end_time, not_exprt{match.condition()});
       }
 
       return obligations;
@@ -629,7 +629,7 @@ static obligationst property_obligations_rec(
       for(auto &rhs_obligation : rhs_obligations_rec.map)
       {
         auto rhs_conjunction = conjunction(rhs_obligation.second);
-        auto cond = implies_exprt{lhs_match_point.condition, rhs_conjunction};
+        auto cond = implies_exprt{lhs_match_point.condition(), rhs_conjunction};
         result.add(rhs_obligation.first, cond);
       }
     }
@@ -667,7 +667,7 @@ static obligationst property_obligations_rec(
       {
         // relies on NNF
         t = std::max(t, no_timeframes - 1);
-        disjuncts.push_back(match.condition);
+        disjuncts.push_back(match.condition());
       }
       else
       {
@@ -676,7 +676,8 @@ static obligationst property_obligations_rec(
             followed_by.consequent(), property_start, no_timeframes)
             .conjunction();
 
-        disjuncts.push_back(and_exprt{match.condition, obligations_rec.second});
+        disjuncts.push_back(
+          and_exprt{match.condition(), obligations_rec.second});
         t = std::max(t, obligations_rec.first);
       }
     }
@@ -704,7 +705,7 @@ static obligationst property_obligations_rec(
       // empty matches are not considered
       if(!match.empty_match())
       {
-        disjuncts.push_back(match.condition);
+        disjuncts.push_back(match.condition());
         max = std::max(max, match.end_time);
       }
     }
diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp
index 4dacc17e..62d5567e 100644
--- a/src/trans-word-level/sequence.cpp
+++ b/src/trans-word-level/sequence.cpp
@@ -189,7 +189,7 @@ sequence_matchest instantiate_sequence(
 
       for(auto &rhs_match : rhs_matches)
       {
-        auto cond = and_exprt{lhs_match.condition, rhs_match.condition};
+        auto cond = and_exprt{lhs_match.condition(), rhs_match.condition()};
         result.push_back({rhs_match.end_time, cond});
       }
     }
@@ -221,7 +221,7 @@ sequence_matchest instantiate_sequence(
         {
           result.emplace_back(
             lhs_match.end_time,
-            and_exprt{lhs_match.condition, rhs_match.condition});
+            and_exprt{lhs_match.condition(), rhs_match.condition()});
         }
       }
     }
@@ -276,7 +276,7 @@ sequence_matchest instantiate_sequence(
 
     for(auto &rhs_match : rhs_matches)
     {
-      exprt::operandst conjuncts = {rhs_match.condition};
+      exprt::operandst conjuncts = {rhs_match.condition()};
 
       for(mp_integer new_t = t; new_t <= rhs_match.end_time; ++new_t)
       {
@@ -315,7 +315,7 @@ sequence_matchest instantiate_sequence(
           if(match_lhs.end_time <= match_rhs.end_time)
           {
             // return the rhs end_time
-            auto cond = and_exprt{match_lhs.condition, match_rhs.condition};
+            auto cond = and_exprt{match_lhs.condition(), match_rhs.condition()};
             result.emplace_back(match_rhs.end_time, std::move(cond));
           }
         }
@@ -343,7 +343,7 @@ sequence_matchest instantiate_sequence(
       for(auto &match_rhs : matches_rhs)
       {
         auto end_time = std::max(match_lhs.end_time, match_rhs.end_time);
-        auto cond = and_exprt{match_lhs.condition, match_rhs.condition};
+        auto cond = and_exprt{match_lhs.condition(), match_rhs.condition()};
         result.emplace_back(std::move(end_time), std::move(cond));
       }
 
diff --git a/src/trans-word-level/sequence.h b/src/trans-word-level/sequence.h
index a332eb4d..ef93adf6 100644
--- a/src/trans-word-level/sequence.h
+++ b/src/trans-word-level/sequence.h
@@ -20,11 +20,16 @@ class sequence_matcht
 public:
   sequence_matcht(mp_integer __end_time, exprt __condition)
     : _is_empty_match(false),
-      end_time(std::move(__end_time)),
-      condition(std::move(__condition))
+      _condition(std::move(__condition)),
+      end_time(std::move(__end_time))
   {
   }
 
+  exprt condition() const
+  {
+    return _condition;
+  }
+
   bool empty_match() const
   {
     return _is_empty_match;
@@ -32,10 +37,10 @@ class sequence_matcht
 
 protected:
   bool _is_empty_match;
+  exprt _condition;
 
 public:
   mp_integer end_time;
-  exprt condition;
 
   static sequence_matcht empty_match(mp_integer end_time)
   {