From 385672ce5dd4f616fe698bcbc7abeae4993668b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 12:23:05 -0700 Subject: [PATCH] Skip is_string_equality rewrite when monadic regex is enabled When smt.seq.regex_monadic is on, 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. The word equation blows up theory_seq on long concatenations before final_check (hence monadic) is ever reached. Evaluated on 1476 regex benchmarks (10s timeout): solved 1160 -> 1341 vs legacy, +193 newly solved, 0 sat<->unsat soundness disagreements. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/smt/seq_regex.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 2b6aaa98ee..89d213818d 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -275,8 +275,12 @@ namespace smt { if (coallesce_in_re(lit)) return; - - if (is_string_equality(lit)) + + // 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())