diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index aab7b1388..b09280d35 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1123,9 +1123,7 @@ namespace pdr {
             n->mk_instantiate(r0, r1, binding);
             proof_ref p1(m), p2(m);
             p1 = r0->get_proof();
-            if (!p1) {
-                r0->display(dctx, std::cout);
-            }
+            IF_VERBOSE(0, if (!p1) r0->display(dctx, verbose_stream()););
             SASSERT(p1);
             pfs[0] = p1;
             rls[0] = r1;
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 93e31ff23..9303181b6 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 #include "dl_mk_array_blast.h"
 #include "qe_util.h"
+#include "scoped_proof.h"
 
 namespace datalog {
 
@@ -270,7 +271,7 @@ namespace datalog {
             }
         }
         
-        expr_ref fml2(m), body(m), head(m);
+        expr_ref fml1(m), fml2(m), body(m), head(m);
         body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
         head = r.get_head();
         sub(body);
@@ -287,9 +288,17 @@ namespace datalog {
         proof_ref p(m);
         rule_set new_rules(m_ctx);
         rm.mk_rule(fml2, p, new_rules, r.name());
+        
 
         rule_ref new_rule(rm);
         if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
+            if (r.get_proof()) {
+                scoped_proof _sc(m);
+                r.to_formula(fml1);
+                p = m.mk_rewrite(fml1, fml2);
+                p = m.mk_modus_ponens(r.get_proof(), p);
+                new_rule->set_proof(m, p);                
+            }
             rules.add_rule(new_rule.get());
             rm.mk_rule_rewrite_proof(r, *new_rule.get());
             TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n"););
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 91481ed5a..112541541 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include "filter_model_converter.h"
 #include "dl_mk_interp_tail_simplifier.h"
 #include "fixedpoint_params.hpp"
+#include "scoped_proof.h"
 
 namespace datalog {
 
@@ -268,7 +269,8 @@ namespace datalog {
                 r->to_formula(fml);
                 if (blast(r, fml)) {
                     proof_ref pr(m);
-                    if (m_context.generate_proof_trace()) {
+                    if (r->get_proof()) {
+                        scoped_proof _sc(m);
                         pr = m.mk_asserted(fml); // loses original proof of r.
                     }
                     // TODO add logic for pc:
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index 0ad4d61ab..57948a2ff 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
@@ -341,7 +341,6 @@ namespace datalog {
             }
             head = mk_head(source, *result, r.get_head(), cnt);
             fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
-            rule_ref_vector added_rules(rm);
             proof_ref pr(m);
             rm.mk_rule(fml, pr, *result);
             TRACE("dl", result->last()->display(m_ctx, tout););