mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-22 23:44:34 +00:00
Code Activity

param eval order

Browse source
This commit is contained in:
Lev Nachmanson 2025-10-07 09:13:21 -07:00
parent 6e52b9584c
commit 3a2bbf4802
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/seq_rewriter.cpp
View file

@ -4359,9 +4359,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
(re().is_union(b, b1, eps) && re().is_epsilon(eps)) || (re().is_union(b, b1, eps) && re().is_epsilon(eps)) ||
(re().is_union(b, eps, b1) && re().is_epsilon(eps))) (re().is_union(b, eps, b1) && re().is_epsilon(eps)))
{ {
result = m().mk_ite(m().mk_eq(str().mk_length(a), zero()), // deterministic evaluation order: build sub-expressions first
m().mk_true(), auto len_a = str().mk_length(a);
re().mk_in_re(a, b1)); auto is_empty = m().mk_eq(len_a, zero());
auto in_b1 = re().mk_in_re(a, b1);
result = m().mk_ite(is_empty, m().mk_true(), in_b1);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
if (str().is_empty(a)) { if (str().is_empty(a)) {