From b47a94c089fcd5aa873471d98ea76175a12db23d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 14:13:44 -0700 Subject: [PATCH] Update seq_regex.cpp --- src/smt/seq_regex.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 89d213818d..6a974c8a75 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -121,6 +121,8 @@ namespace smt { } void seq_regex::propagate_accept_legacy(literal lit, expr* s, expr* r) { + if (is_string_equality(lit)) + return; expr_ref regex(r, m); if (!m.is_value(s)) { expr_ref s_approx = get_overapprox_regex(s); @@ -275,13 +277,6 @@ namespace smt { if (coallesce_in_re(lit)) return; - - // With the monadic end-game enabled, keep contains-style memberships (s in .*P.*) - // as regex memberships routed to the monadic solver instead of rewriting them into - // a word equation s = f1 ++ P ++ f2, whose word-equation solving blows up on long - // concatenations before final_check is ever reached. - if (!th.use_monadic_regex() && is_string_equality(lit)) - return; if (th.use_monadic_regex()) add_monadic_membership(lit, s, r);