From 8ccf4cd8f77fe9145947613c33657f2b29bdf7f6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:19:24 -0700 Subject: [PATCH] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0ea11248d..4380504d5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2404,7 +2404,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { } expr* b; if (str().is_itos(a, b)) { - result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one()); + auto a = m_autil.mk_ge(b, zero()); + result = m().mk_ite(a, b, minus_one()); return BR_DONE; } if (str().is_ubv2s(a, b)) { @@ -2415,7 +2416,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { expr* c = nullptr, *t = nullptr, *e = nullptr; if (m().is_ite(a, c, t, e)) { - result = m().mk_ite(c, str().mk_stoi(t), str().mk_stoi(e)); + auto a = str().mk_stoi(t); + result = m().mk_ite(c, a, str().mk_stoi(e)); return BR_REWRITE_FULL; }