diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 9278ae5ae..c29688020 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -74,6 +74,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     bool                m_push_ite_bv = true;
     bool                m_ignore_patterns_on_ground_qbody = true;
     bool                m_rewrite_patterns = true;
+    bool                m_enable_der = true;
 
 
     ast_manager & m() const { return m_b_rw.m(); }
@@ -89,6 +90,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_push_ite_bv    = p.push_ite_bv();
         m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
         m_rewrite_patterns = p.rewrite_patterns();
+        m_enable_der     = p.enable_der();
     }
 
     void updt_params(params_ref const & p) {
@@ -827,11 +829,17 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         expr_ref r(m());
 
         bool der_change = false;
-        if (is_quantifier(result) && to_quantifier(result)->get_num_patterns() == 0) {
+        if (m_enable_der && is_quantifier(result) && to_quantifier(result)->get_num_patterns() == 0) {
             m_der(to_quantifier(result), r, p2);
             der_change = result.get() != r.get();
             if (m().proofs_enabled() && der_change)
-                result_pr = m().mk_transitivity(result_pr, p2);            
+                result_pr = m().mk_transitivity(result_pr, p2);
+
+            if (der_change) {
+                verbose_stream() << result << "\n";
+                verbose_stream() << "==>\n";
+                verbose_stream() << r << "\n";
+            }
             result = r;
         }
 
diff --git a/src/params/rewriter_params.pyg b/src/params/rewriter_params.pyg
index 290f7b1da..20490606c 100644
--- a/src/params/rewriter_params.pyg
+++ b/src/params/rewriter_params.pyg
@@ -8,6 +8,7 @@ def_module_params('rewriter',
                           ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
                           ("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
                           ("cache_all", BOOL, False, "cache all intermediate results."),
+			  ("enable_der", BOOL, True, "enable destructive equality resolution to quantifiers."),
                           ("rewrite_patterns", BOOL, False, "rewrite patterns."),
                           ("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))