diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 18b335ecb..ee8b79be5 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -76,6 +76,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     bool                m_ignore_patterns_on_ground_qbody = true;
     bool                m_rewrite_patterns = true;
     bool                m_enable_der = true;
+    bool                m_nested_der = false;
 
 
     ast_manager & m() const { return m_b_rw.m(); }
@@ -92,6 +93,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
         m_rewrite_patterns = p.rewrite_patterns();
         m_enable_der     = p.enable_der();
+        m_nested_der     = _p.get_bool("nested_der", false);
     }
 
     void updt_params(params_ref const & p) {
@@ -843,8 +845,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             result = r;
         }
 
-        if (der_change) {
+        if (der_change && !m_nested_der) {
             th_rewriter rw(m());
+            params_ref p;
+            p.set_bool("nested_der", true);
+            rw.updt_params(p);
             rw(result, r, p2);
             if (m().proofs_enabled() && result.get() != r.get()) 
                 result_pr = m().mk_transitivity(result_pr, p2);