From 40b980079b6bb8351549a7f2c8557148aa9e54c3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:14:02 -0700 Subject: [PATCH] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 351dde879..0ea11248d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4082,7 +4082,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // tl = rest of reverse(r2) i.e. butlast of r2 //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one())); hd = mk_seq_last(r2); - m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); + // factor nested constructor calls to enforce deterministic argument evaluation order + auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))); + auto a_eq = m().mk_eq(hd, ele); + m_br.mk_and(a_non_empty, a_eq, result); tl = re().mk_to_re(mk_seq_butlast(r2)); return re_and(result, re().mk_reverse(tl)); }