From a41549eee69986b3cede4408f4f416811879bae0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Oct 2025 10:06:43 -0700 Subject: [PATCH] parameter eval order Signed-off-by: Lev Nachmanson --- src/ast/rewriter/seq_rewriter.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 44c29561d..351dde879 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2988,7 +2988,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref } else { // observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first - m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_first(r1), e), c1); + { + auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))); + auto eq_first = m().mk_eq(mk_seq_first(r1), e); + m_br.mk_and(is_non_empty, eq_first, c1); + } m_br.mk_and(path, c1, c2); if (m().is_false(c2)) result = nothing(); @@ -3001,7 +3005,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref if (re().is_to_re(r2, r1)) { // here r1 is a sequence // observe that the precondition |r1|>0 of mk_seq_last is implied by c1 - m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_last(r1), e), c1); + { + auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))); + auto eq_last = m().mk_eq(mk_seq_last(r1), e); + m_br.mk_and(is_non_empty, eq_last, c1); + } m_br.mk_and(path, c1, c2); if (m().is_false(c2)) result = nothing();