From e54dfb5b01c021d2bf3602662646879cb6c2e243 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 17 Dec 2024 16:21:26 +0000 Subject: [PATCH] Update expr_safe_replace.cpp --- src/ast/rewriter/expr_safe_replace.cpp | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 2ca3b5e24..1eae5d19b 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -160,7 +160,26 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { replace(q->get_no_pattern(i), tmp); nopats.push_back(tmp); } - replace(q->get_expr(), new_body); + + bool all_vars = true; + unsigned max_idx = 0; + for (unsigned i = 0, e = m_src.size(); i < e; ++i) { + auto *s = m_src.get(i); + if (!(all_vars = is_var(s))) + break; + max_idx = std::max(max_idx, to_var(s)->get_idx()); + } + if (all_vars) { + m_args.reset(); + m_args.resize(max_idx + num_decls); + for (unsigned i = 0, e = m_src.size(); i < e; ++i) { + m_args[to_var(m_src.get(i))->get_idx() + num_decls] = m_dst.get(i); + } + var_subst subst(m); + new_body = subst(q->get_expr(), m_args); + } else { + replace(q->get_expr(), new_body); + } } b = m.update_quantifier(q, pats.size(), pats.data(), nopats.size(), nopats.data(), new_body); m_refs.push_back(b);