From 5a95b40bdb6938d77b5c2fbe0f152c8fe8c9ace2 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Thu, 5 Mar 2026 18:17:04 +0100
Subject: [PATCH] Canceling out common variables is a simplification step now

---
 src/smt/seq/seq_nielsen.cpp | 52 ++++++++++---------------------------
 1 file changed, 14 insertions(+), 38 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index cd67bd9f6..6e039190c 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -618,26 +618,11 @@ namespace seq {
                 changed = true;
             }
 
-            // pass 2: detect symbol clashes and empty-propagation
+            // pass 2: detect symbol clashes, empty-propagation, and prefix cancellation
             for (str_eq& eq : m_str_eq) {
                 if (!eq.m_lhs || !eq.m_rhs)
                     continue;
 
-                // both sides start with a concrete character: check match
-                if (eq.m_lhs->is_char() && eq.m_rhs->is_char()) {
-                    if (eq.m_lhs->id() != eq.m_rhs->id()) {
-                        // symbol clash
-                        m_is_general_conflict = true;
-                        m_reason = backtrack_reason::symbol_clash;
-                        return simplify_result::conflict;
-                    }
-                    // same char: drop from both sides
-                    eq.m_lhs = sg.drop_first(eq.m_lhs);
-                    eq.m_rhs = sg.drop_first(eq.m_rhs);
-                    changed = true;
-                    continue;
-                }
-
                 // one side empty, the other not empty => conflict or substitution
                 if (eq.m_lhs->is_empty() && !eq.m_rhs->is_empty()) {
                     if (handle_empty_side(sg, eq.m_rhs, eq.m_dep, changed))
@@ -650,20 +635,28 @@ namespace seq {
                     continue;
                 }
 
-                // prefix matching: lhs and rhs both start with the same char => cancel
+                // prefix cancellation: strip any common leading tokens.
+                // Same char or same variable on both sides can always be cancelled.
+                // Two different concrete characters is a symbol clash.
                 {
                     euf::snode_vector lhs_toks, rhs_toks;
                     eq.m_lhs->collect_tokens(lhs_toks);
                     eq.m_rhs->collect_tokens(rhs_toks);
                     unsigned prefix = 0;
-                    while (prefix < lhs_toks.size() && prefix < rhs_toks.size() &&
-                           lhs_toks[prefix]->is_char() && rhs_toks[prefix]->is_char()) {
-                        if (lhs_toks[prefix]->id() != rhs_toks[prefix]->id()) {
+                    while (prefix < lhs_toks.size() && prefix < rhs_toks.size()) {
+                        euf::snode* lt = lhs_toks[prefix];
+                        euf::snode* rt = rhs_toks[prefix];
+                        if (lt->id() == rt->id() && (lt->is_char() || lt->is_var())) {
+                            // identical token on both sides: cancel
+                            ++prefix;
+                        } else if (lt->is_char() && rt->is_char()) {
+                            // different concrete characters: symbol clash
                             m_is_general_conflict = true;
                             m_reason = backtrack_reason::symbol_clash;
                             return simplify_result::conflict;
+                        } else {
+                            break;
                         }
-                        ++prefix;
                     }
                     if (prefix > 0) {
                         eq.m_lhs = sg.drop_left(eq.m_lhs, prefix);
@@ -884,23 +877,6 @@ namespace seq {
             euf::snode* lhead = lhs_toks[0];
             euf::snode* rhead = rhs_toks[0];
 
-            // same-head variable cancellation: x·A = x·B → A = B
-            if (lhead->is_var() && lhead->id() == rhead->id()) {
-                euf::snode* ltail = m_sg.drop_first(eq.m_lhs);
-                euf::snode* rtail = m_sg.drop_first(eq.m_rhs);
-                nielsen_node* child = mk_child(node);
-                // replace the equation with the tails
-                for (str_eq& ceq : child->str_eqs()) {
-                    if (ceq.m_lhs == eq.m_lhs && ceq.m_rhs == eq.m_rhs) {
-                        ceq.m_lhs = ltail;
-                        ceq.m_rhs = rtail;
-                        break;
-                    }
-                }
-                mk_edge(node, child, true);
-                return true;
-            }
-
             // variable definition: x = t where x ∉ vars(t) → subst x → t
             if (lhead->is_var() && eq.m_rhs->is_empty()) {
                 nielsen_node* child = mk_child(node);