From 2ea1c740713ad026942b1eb40dc137421c1e266c Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 21 May 2026 19:12:15 +0200 Subject: [PATCH] Make var-nielsen case non-recursive --- src/smt/seq/seq_nielsen.cpp | 10 ++++------ src/smt/seq/seq_nielsen.h | 4 ++-- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 77d3cb29c..3b47ae516 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2345,12 +2345,10 @@ namespace seq { const bool fwd = od == 0; euf::snode* lhead = dir_token(eq.m_lhs, fwd); euf::snode* rhead = dir_token(eq.m_rhs, fwd); - if (!lhead || !rhead) - continue; + SASSERT(lhead && rhead); + SASSERT(lhead->id() != rhead->id()); if (!lhead->is_var() || !rhead->is_var()) continue; - if (lhead->id() == rhead->id()) - continue; // x·A = y·B where x,y are distinct variables (classic Nielsen) // child 1: x → ε (progress) @@ -2371,7 +2369,7 @@ namespace seq { } // child 3: x → y·x (no progress) { - euf::snode* replacement = dir_concat(m_sg, rhead, lhead, fwd); + euf::snode* replacement = dir_concat(m_sg, rhead, get_tail(lhead, compute_length_expr(rhead).get(), fwd), fwd); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, false); const nielsen_subst s(lhead, replacement, @@ -2382,7 +2380,7 @@ namespace seq { } // child 4: y → x·y (no progress) { - euf::snode* replacement = dir_concat(m_sg, lhead, rhead, fwd); + euf::snode* replacement = dir_concat(m_sg, lhead, get_tail(rhead, compute_length_expr(lhead).get(), fwd), fwd); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, false); const nielsen_subst s(rhead, replacement, diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 96e9003d8..d216ec259 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -501,9 +501,9 @@ namespace seq { dep_tracker dep; // tracks which input constraints contributed static expr_ref simplify(expr* f, ast_manager& m) { - th_rewriter th(m); + //th_rewriter th(m); expr_ref fml(f, m); - th(fml); + //th(fml); return fml; }