From 7cc5a73bd8118cc04a507ec8d494aecc8f713883 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 2 Jul 2026 20:47:15 +0200 Subject: [PATCH] Fixed wrong models in case the string witness fails --- src/smt/seq_model.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index d527b30ba5..aa9b91cc43 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -511,16 +511,20 @@ namespace smt { expr_ref witness(m); // We checked non-emptiness during Nielsen already lbool wr = m_rewriter.some_string_in_re(re_expr, str); - if (wr != l_true) { + if (wr == l_true) { + witness = m_seq.str.mk_string(str); + } + else { // some_seq_in_re can fail (l_undef / l_false) on regexes it does // not fully support — notably projection operators (re.proj), // but also some plain Boolean-closure / large length-intersected // shapes. Fall back to a derivative-automaton BFS that builds an - // accepting word of the requested length directly. + // accepting word of the requested length directly. It sets + // `witness` itself -- do NOT overwrite it from `str`, which + // some_string_in_re left untouched (i.e. still empty) on failure. wr = derivative_witness(m_sg.mk(re_expr), witness); } if (wr == l_true) { - witness = m_seq.str.mk_string(str); m_trail.push_back(witness); m_factory->register_value(witness); return witness;