mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-06 07:16:13 +00:00
Code Activity

Derived by the wrong "leading character"

Browse source
This commit is contained in:
CEisenhofer 2026-06-09 16:56:05 +02:00
parent 7a909aedb7
commit 89a2ac133f
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_nseq.cpp
View file

@ -463,8 +463,11 @@ namespace smt {
euf::snode* re_node = mem.m_regex; euf::snode* re_node = mem.m_regex;
euf::snode* str_node = mem.m_str; euf::snode* str_node = mem.m_str;
do { do {
// eliminate leading character by derivatives // eliminate leading character by derivatives; derive by the
re_node = m_sgraph.brzozowski_deriv(re_node, mem.m_str->first()); // 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); str_node = m_sgraph.drop_first(str_node);
} while (!str_node->is_empty() && str_node->first()->is_char()); } while (!str_node->is_empty() && str_node->first()->is_char());