From 987099c765d76c48ca5168b7d0cdde7aed47b7a8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 May 2021 10:54:21 -0700
Subject: [PATCH] Hoist creation of m_rep for #5259

---
 src/ast/rewriter/th_rewriter.cpp | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 99f26234a..8e00bf657 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -51,6 +51,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     recfun_rewriter     m_rec_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
+    expr_safe_replace   m_rep;
     expr_ref_vector     m_pinned;
     unsigned long long  m_max_memory; // in bytes
     unsigned            m_max_steps;
@@ -685,12 +686,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     void apply_subst(ptr_buffer<expr>& patterns) {
         if (!m_subst)
             return;
+        if (patterns.empty())
+            return;
         expr_ref tmp(m());
-        expr_safe_replace rep(m());
-        for (auto kv : m_subst->sub())
-            rep.insert(kv.m_key, kv.m_value);
         for (unsigned i = 0; i < patterns.size(); ++i) {
-            rep(patterns[i], tmp);
+            m_rep(patterns[i], tmp);
             m_pinned.push_back(tmp);
             patterns[i] = tmp;
         }
@@ -796,6 +796,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_rec_rw(m),
         m_a_util(m),
         m_bv_util(m),
+        m_rep(m),
         m_pinned(m),
         m_used_dependencies(m),
         m_subst(nullptr) {
@@ -805,6 +806,9 @@ 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);
     }
 
     void reset() {