diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp
index 800644d9e..398af6103 100644
--- a/src/tactic/core/distribute_forall_tactic.cpp
+++ b/src/tactic/core/distribute_forall_tactic.cpp
@@ -52,6 +52,9 @@ class distribute_forall_tactic : public tactic {
                     new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
                 }
                 result = m.mk_and(new_args.size(), new_args.c_ptr());
+                if (m.proofs_enabled()) {
+                    result_pr = m.mk_push_quant(old_q, result);
+                }
                 return true;
             }
 
@@ -70,6 +73,9 @@ class distribute_forall_tactic : public tactic {
                     new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
                 }
                 result = m.mk_and(new_args.size(), new_args.c_ptr());
+                if (m.proofs_enabled()) {
+                    result_pr = m.mk_push_quant(old_q, result);
+                }
                 return true;
             }
 
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 6f55ca2f7..a2ce8a801 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -483,10 +483,11 @@ reduce_args_tactic::~reduce_args_tactic() {
 void reduce_args_tactic::operator()(goal_ref const & g, 
                                     goal_ref_buffer & result) {
     SASSERT(g->is_well_sorted());
-    fail_if_proof_generation("reduce-args", g);
     fail_if_unsat_core_generation("reduce-args", g);
     result.reset();
-    m_imp->operator()(*(g.get()));
+    if (!m_imp->m().proofs_enabled()) {
+        m_imp->operator()(*(g.get()));
+    }
     g->inc_depth();
     result.push_back(g.get());
     SASSERT(g->is_well_sorted());
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index b9f0ee138..32725eba0 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -401,6 +401,7 @@ void goal::display_with_proofs(std::ostream& out) const {
         out << "\n  |-";
         if (pr(i)) {
             out << mk_ismt2_pp(pr(i), m(), 4);
+            SASSERT(m().get_fact(pr(i)) == form(i));
         }
         out << "\n  " << mk_ismt2_pp(form(i), m(), 2);
     }
diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index 66a26be00..bb283b32f 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -657,8 +657,8 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
 
 void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
     if (m_manager.proofs_enabled()) {
+        TRACE("tactic", tout << "PRE_DEMODULATOR=true is not supported when proofs are enabled.";);
         // Let us not waste time with proof production
-        warning_msg("PRE_DEMODULATOR=true is not supported when proofs are enabled.");
         new_exprs.append(n, exprs);
         new_prs.append(n, prs);
         return;