diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index b9b3a7f85..a04c96f4f 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -21,6 +21,7 @@ Notes:
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/act_cache.h"
+#include "util/obj_hashtable.h"
 
 /**
    \brief Common infrastructure for AST rewriters.
@@ -60,6 +61,7 @@ protected:
     proof_ref_vector           m_result_pr_stack;
     // --------------------------
 
+    obj_hashtable<expr>        m_blocked;
     expr *                     m_root;
     unsigned                   m_num_qvars;
     struct scope {
@@ -112,6 +114,8 @@ protected:
     void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); }
     
     void elim_reflex_prs(unsigned spos);
+    void block(expr* t) { m_blocked.insert(t); }
+    bool is_blocked(expr* t) const { return m_blocked.contains(t); }
 public:
     rewriter_core(ast_manager & m, bool proof_gen);
     virtual ~rewriter_core();
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 2707c229f..4bf829be6 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -195,14 +195,15 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
             if (process_const<ProofGen>(to_app(t)))
                 return true;
             TRACE("rewriter_const", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r, m()) << "\n";);
-#if 1
-#else
-            // disabled pending fix for loop/stack overflow in case of recursive expansion (possible)
-            rewriter_tpl rw(m(), false, m_cfg);
-            expr_ref result(m());
-            rw(m_r, result, m_pr);
-            m_r = result;
-#endif
+            if (!is_blocked(t)) {
+                rewriter_tpl rw(m(), false, m_cfg);
+                for (auto* s : m_blocked)
+                    rw.block(s);
+                rw.block(t);
+                expr_ref result(m());
+                rw(m_r, result, m_pr);
+                m_r = result;
+            }
             set_new_child_flag(t, m_r);
             result_stack().push_back(m_r);
             return true;