From 89a2ac133f6dc896aa6aa04a3c7f87673831cfe8 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 9 Jun 2026 16:56:05 +0200 Subject: [PATCH] Derived by the wrong "leading character" --- src/smt/theory_nseq.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index d7fefa08a..401c24431 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -463,8 +463,11 @@ namespace smt { euf::snode* re_node = mem.m_regex; euf::snode* str_node = mem.m_str; do { - // eliminate leading character by derivatives - re_node = m_sgraph.brzozowski_deriv(re_node, mem.m_str->first()); + // eliminate leading character by derivatives; derive by the + // CURRENT leading char (str_node->first()), not the original + // mem.m_str->first() — otherwise a multi-char prefix is derived + // by its first char repeatedly (unsound). + re_node = m_sgraph.brzozowski_deriv(re_node, str_node->first()); str_node = m_sgraph.drop_first(str_node); } while (!str_node->is_empty() && str_node->first()->is_char());