From 712cd68e8c8accc9215a82f0c8f5a9e6aa77d0bb Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Wed, 6 May 2026 16:38:26 +0200
Subject: [PATCH] Don't add duplicate equations and membership constraints to
 Nielsen root

---
 src/smt/seq/seq_nielsen.cpp | 12 ++++++++++++
 src/smt/theory_nseq.cpp     |  9 +++++++++
 2 files changed, 21 insertions(+)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 92b49d7e4..b18c80c72 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -460,12 +460,24 @@ namespace seq {
         dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
         str_eq eq(lhs, rhs, dep);
         eq.sort();
+        // check if root node contains this equation already
+        if (std::ranges::any_of(m_root->str_eqs(), [&](const str_eq& e) {
+            return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs;
+        }))
+            // already present, no need to add again
+            return;
         m_root->add_str_eq(eq);
     }
 
     void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) {
         if (!root())
             create_root();
+        // check if root node contains this membership constraint already
+        if (std::ranges::any_of(m_root->str_mems(), [&](const str_mem& e) {
+            return e.m_regex == regex && e.m_str == str;
+        }))
+            // already present, no need to add again
+            return;
         dep_tracker dep = m_dep_mgr.mk_leaf(l);
         m_root->add_str_mem(str_mem(str, regex, dep));
     }
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 36833ec0a..620dc2c87 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -992,6 +992,15 @@ namespace smt {
 #ifdef Z3DEBUG
         std::cout << "Conflict with " << lits.size() << " literals and " << eqs.size() << " equalities" << std::endl;
         std::cout << "The root node contained " << m_nielsen.root()->str_mems().size() << " memberships and " << m_nielsen.root()->str_eqs().size() << " equalities" << std::endl;
+        unsigned idx = 0;
+        for (auto& eq : m_nielsen.root()->str_eqs()) {
+            std::cout << "[" << (idx++) << "]: " << seq::eq_pp(eq, m);
+        }
+        idx = 0;
+        for (auto& mem : m_nielsen.root()->str_mems()) {
+            std::cout << "[" << (idx++) << "]: " << seq::mem_pp(m, mem);
+        }
+        std::flush(std::cout);
 #endif
     }