mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

Update seq_regex.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-02 14:13:44 -07:00
parent ee319167ad
commit b47a94c089
1 changed files with 2 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/seq_regex.cpp
View file

@ -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);