From 8af9a20e01e92523a593cb71776a5fc476463f82 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:26:40 -0700 Subject: [PATCH] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d7d9cb1f3..c2649f20f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1890,7 +1890,10 @@ br_status seq_rewriter::mk_seq_map(expr* f, expr* seqA, expr_ref& result) { return BR_REWRITE2; } if (str().is_concat(seqA, s1, s2)) { - result = str().mk_concat(str().mk_map(f, s1), str().mk_map(f, s2)); + // introduce temporaries to ensure deterministic evaluation order of recursive map calls + auto m1 = str().mk_map(f, s1); + auto m2 = str().mk_map(f, s2); + result = str().mk_concat(m1, m2); return BR_REWRITE2; } return BR_FAILED; @@ -1910,8 +1913,9 @@ br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& resu } if (str().is_concat(seqA, s1, s2)) { expr_ref j(m_autil.mk_add(i, str().mk_length(s1)), m()); - auto a = str().mk_mapi(f, i, s1); - result = str().mk_concat(a, str().mk_mapi(f, j, s2)); + auto left = str().mk_mapi(f, i, s1); + auto right = str().mk_mapi(f, j, s2); + result = str().mk_concat(left, right); return BR_REWRITE2; } return BR_FAILED;