From e2a52ed6eeccbdf5ce01d9b04b7acac347fd20e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 11:15:19 -0700 Subject: [PATCH] #5259 again --- src/ast/rewriter/th_rewriter.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 8e00bf657..1f80d57a6 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -52,9 +52,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg { arith_util m_a_util; bv_util m_bv_util; expr_safe_replace m_rep; + bool m_new_subst { false }; expr_ref_vector m_pinned; unsigned long long m_max_memory; // in bytes - unsigned m_max_steps; + unsigned m_max_steps; bool m_pull_cheap_ite; bool m_flat; bool m_cache_all; @@ -688,6 +689,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return; if (patterns.empty()) return; + if (m_new_subst) { + m_rep.reset(); + for (auto kv : m_subst->sub()) + m_rep.insert(kv.m_key, kv.m_value); + m_new_subst = false; + } expr_ref tmp(m()); for (unsigned i = 0; i < patterns.size(); ++i) { m_rep(patterns[i], tmp); @@ -806,9 +813,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void set_substitution(expr_substitution * s) { reset(); m_subst = s; - m_rep.reset(); - for (auto kv : m_subst->sub()) - m_rep.insert(kv.m_key, kv.m_value); + m_new_subst = true; } void reset() {