From 87df0b941bb1732fd0a45788f98689140088ffff Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Fri, 3 Jul 2026 14:47:59 +0200
Subject: [PATCH] No length abstraction on factored regexes [maybe reintroduce
 it later by distinguishing where the regex comes from]

---
 src/smt/seq/seq_nielsen.cpp | 21 +++++++++++++++++++--
 src/smt/theory_nseq.cpp     | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 2 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index b96e4990e3..2f35c8f873 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2676,8 +2676,25 @@ namespace seq {
                     // node's string signature alone.  Make it sticky (survives
                     // hot-restart) and memoize it in the transposition table.
                     node->set_general_conflict();
-                    node->m_unsat_cacheable = true;
-                    m_unsat_node_cache.insert(node);
+                    // EXCEPTION: a lazy-factorization continuation (is_rf_cont)
+                    // aliases its parent's — and ultimately the original, undivided
+                    // membership's — string signature, yet its subtree only explored
+                    // the REMAINING splits of the suspended iterator (the earlier
+                    // splits' child-A branches live under ancestors, not here).  Its
+                    // "string-only unsat" is thus a property of the remaining-splits
+                    // subproblem, NOT of the full signature.  Memoizing it would let a
+                    // structurally-identical ancestor (e.g. the root, on a later
+                    // hot-restart solve) hit the cache and be pruned even though it
+                    // still has the earlier splits to try — a spurious UNSAT.  So we
+                    // keep the node itself dead but do NOT cache it, mirroring the
+                    // cache-lookup and loop-cut exemptions above (both keyed on
+                    // is_rf_cont).
+                    if (!node->is_rf_cont()) {
+                        node->m_unsat_cacheable = true;
+                        m_unsat_node_cache.insert(node);
+                    }
+                    else
+                        node->m_unsat_cacheable = false;
                 }
                 else
                     // Conditional on an ancestor above us; valid for this path only.
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 2bdfe67dd5..a3c365e04f 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -2001,6 +2001,27 @@ namespace smt {
 
         SASSERT(!var_to_mems.empty());
 
+        // A length-coherence propagation `deps -> len(s) != l` is only SOUND when the
+        // memberships behind it hold globally.  A membership `s in R` at a SAT leaf is
+        // globally valid ONLY if it is an original input membership (present verbatim
+        // in the root).  Regex factorization/decomposition splits an input membership
+        // `s.u in R` into a *disjunct* `s in Δ` and keeps the ORIGINAL literal as the
+        // sole dependency — so `s in Δ` is branch-specific: it is one way to satisfy
+        // `s.u in R`, not a consequence of it.  Propagating a length bound derived
+        // from such a Δ (justified only by the original literal) is unsound: two
+        // different factorization branches can yield contradictory bounds (e.g.
+        // len(s) != 0 from a branch where s is non-empty and len(s) = 0 from a branch
+        // where s is empty), both "justified" by the same satisfiable input, closing a
+        // SAT instance as UNSAT.  Guard by matching the leaf membership against the
+        // root's input memberships (snode identity ⇒ same constraint).
+        auto is_original_mem = [&](seq::str_mem const& mem) {
+            for (auto const& rmem : m_nielsen.root()->str_mems())
+                if (rmem.m_str->id() == mem.m_str->id() &&
+                    rmem.m_regex->id() == mem.m_regex->id())
+                    return true;
+            return false;
+        };
+
         for (expr* len_expr : m_relevant_lengths) {
             expr* s = nullptr;
             VERIFY(m_seq.str.is_length(len_expr, s));
@@ -2025,6 +2046,7 @@ namespace smt {
             unsigned_vector const &mem_indices = var_to_mems[var_id];
             euf::snode_vector regexes;
             bool has_view_or_guard = false;
+            bool has_derived = false;
             for (auto i : mem_indices) {
                 SASSERT(mems[i].well_formed());
                 regexes.push_back(mems[i].m_regex);
@@ -2032,6 +2054,10 @@ namespace smt {
                 // (Section 3.3) rather than a real regex; skip length coherence.
                 if (!mems[i].is_plain())
                     has_view_or_guard = true;
+                // Factorization/decomposition-derived (branch-specific) membership:
+                // its length implication is not globally sound (see is_original_mem).
+                if (!is_original_mem(mems[i]))
+                    has_derived = true;
             }
 
             // Skip length coherence for synthetic cycle variables constrained by a
@@ -2042,6 +2068,12 @@ namespace smt {
             if (has_view_or_guard)
                 continue;
 
+            // Skip variables whose leaf memberships are not all original input
+            // memberships: a length bound derived from a branch-specific split
+            // membership cannot be soundly propagated to the outer solver.
+            if (has_derived)
+                continue;
+
             SASSERT(!regexes.empty());
             sort *ele_sort;
             VERIFY(m_seq.is_seq(m_sg.get_str_sort(), ele_sort));