From 9f6eb4f45588b5a889ae37b003ab3dcb75de92bc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 24 Mar 2026 19:57:43 -0700
Subject: [PATCH] remove unused fields

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq/seq_nielsen.h      |  7 +------
 src/smt/seq/seq_nielsen_pp.cpp | 20 --------------------
 2 files changed, 1 insertion(+), 26 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 769281b92..4aaccf0e1 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -484,8 +484,6 @@ namespace seq {
         nielsen_node*           m_tgt;
         vector<nielsen_subst>   m_subst;
         vector<char_subst>      m_char_subst;     // character-level substitutions (mirrors ZIPT's SubstC)
-        ptr_vector<str_eq>      m_side_str_eq;    // side constraints: string equalities
-        ptr_vector<str_mem>     m_side_str_mem;    // side constraints: regex memberships
         vector<int_constraint>  m_side_int;        // side constraints: integer equalities/inequalities
         bool                    m_is_progress;     // does this edge represent progress?
         bool                    m_len_constraints_computed = false; // lazily computed substitution length constraints
@@ -503,12 +501,9 @@ namespace seq {
         vector<char_subst> const& char_substs() const { return m_char_subst; }
         void add_char_subst(char_subst const& s) { m_char_subst.push_back(s); }
 
-        void add_side_str_eq(str_eq* eq) { m_side_str_eq.push_back(eq); }
-        void add_side_str_mem(str_mem* mem) { m_side_str_mem.push_back(mem); }
+
         void add_side_int(int_constraint const& ic) { m_side_int.push_back(ic); }
 
-        ptr_vector<str_eq> const& side_str_eq() const { return m_side_str_eq; }
-        ptr_vector<str_mem> const& side_str_mem() const { return m_side_str_mem; }
         vector<int_constraint> const& side_int() const { return m_side_int; }
 
         bool is_progress() const { return m_is_progress; }
diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp
index f84e2f927..f9e7031fe 100644
--- a/src/smt/seq/seq_nielsen_pp.cpp
+++ b/src/smt/seq/seq_nielsen_pp.cpp
@@ -605,26 +605,6 @@ namespace seq {
                     out << "?" << cs.m_var->id()
                         << " &#8594; ?" << cs.m_val->id();
                 }
-                // side constraints: string equalities
-                for (auto const* eq : e->side_str_eq()) {
-                    if (!first) out << "<br/>";
-                    first = false;
-                    out << "<font color=\"gray\">"
-                        << snode_label_html(eq->m_lhs, m)
-                        << " = "
-                        << snode_label_html(eq->m_rhs, m)
-                        << "</font>";
-                }
-                // side constraints: regex memberships
-                for (auto const* mem : e->side_str_mem()) {
-                    if (!first) out << "<br/>";
-                    first = false;
-                    out << "<font color=\"gray\">"
-                        << snode_label_html(mem->m_str, m)
-                        << " &#8712; "
-                        << snode_label_html(mem->m_regex, m)
-                        << "</font>";
-                }
                 // side constraints: integer equalities/inequalities
                 for (auto const& ic : e->side_int()) {
                     if (!first) out << "<br/>";