From 3a2bbf4802cf40b97c7340188dfac888c6702691 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 09:13:21 -0700 Subject: [PATCH] param eval order --- src/ast/rewriter/seq_rewriter.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4c325f171..129582daa 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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, eps, b1) && re().is_epsilon(eps))) { - result = m().mk_ite(m().mk_eq(str().mk_length(a), zero()), - m().mk_true(), - re().mk_in_re(a, b1)); + // deterministic evaluation order: build sub-expressions first + auto len_a = str().mk_length(a); + 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; } if (str().is_empty(a)) {