diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 204c76287..f49b80b15 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2816,7 +2816,7 @@ proof * ast_manager::mk_goal(expr * f) {
 }
 
 proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
-    if (!p1 || !p2) return nullptr;
+    if (!p2 || !p1) return p1;
     SASSERT(has_fact(p1));
     SASSERT(has_fact(p2));
     CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))),
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 3a2f0dabd..345fffc23 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -68,11 +68,12 @@ public:
         proof_ref new_pr1(m), new_pr2(m);
         for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
             rw1(g->form(idx), new_f1, new_pr1);
-            TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
+            TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;);
             rw2(false, new_f1, new_f2, new_pr2);
+            TRACE("card2bv", tout << "Rewriting " << new_f2 << "\n" << new_pr2 << std::endl;);
             if (m.proofs_enabled()) {
-                new_pr1  = m.mk_modus_ponens(g->pr(idx), new_pr1);
-                new_pr1  = m.mk_modus_ponens(new_pr1, new_pr2);
+                new_pr1 = m.mk_transitivity(new_pr1, new_pr2);
+                new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1);
             }
             g->update(idx, new_f2, new_pr1, g->dep(idx));
         }
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 4c64c0a30..372913ffb 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -195,15 +195,21 @@ public:
                 TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";);
             }
         }
-        for (unsigned i = 0; i < g->size(); i++) {
+        for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {
             checkpoint();
 
             expr_ref   new_curr(m), tmp(m);
-            proof_ref  new_pr(m);
+            proof_ref  pr1(m), pr2(m), new_pr(m);
             rep(g->form(i), tmp);
+            if (g->form(i) != tmp && m.proofs_enabled()) {
+                pr1 = m.mk_rewrite(g->form(i), tmp);
+            }
             m_rw(tmp, new_curr, new_pr);
-            if (m.proofs_enabled() && !new_pr) {
-                new_pr = m.mk_rewrite(g->form(i), new_curr);
+            if (m.proofs_enabled() && tmp != new_curr) {
+                pr2 = m.mk_rewrite(tmp, new_curr);
+            }
+            if (m.proofs_enabled()) {
+                new_pr = m.mk_transitivity(pr1, pr2);
                 new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
             }
             // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";);
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 6ec2cbd38..ca76cafc7 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -44,7 +44,6 @@ struct simplify_tactic::imp {
 
     void operator()(goal & g) {
         tactic_report report("simplifier", g);
-        TRACE("before_simplifier", g.display(tout););
         m_num_steps = 0;
         if (g.inconsistent())
             return;
@@ -63,9 +62,8 @@ struct simplify_tactic::imp {
             }
             g.update(idx, new_curr, new_pr, g.dep(idx));
         }
-        TRACE("after_simplifier_bug", g.display(tout););
+        TRACE("simplifier", g.display(tout););
         g.elim_redundancies();
-        TRACE("after_simplifier", g.display(tout););
         TRACE("after_simplifier_detail", g.display_with_dependencies(tout););
     }
 
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 286f2864a..757067cb0 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -588,7 +588,7 @@ bool goal::is_well_formed() const {
         expr * t = form(i);
         if (!::is_well_sorted(m(), t))
             return false;
-#if 0
+#if 1
         SASSERT(m().get_fact(pr(i)) == form(i));
         if (m().get_fact(pr(i)) != form(i))
             return false;
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 6f2d844e1..4c5031d32 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -41,7 +41,6 @@ struct tactic_report::imp {
     ~imp() {
         m_watch.stop();
         double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
-        SASSERT(m_goal.is_well_formed());
         TRACE("tactic", m_goal.display(tout););
         IF_VERBOSE(0, 
                    verbose_stream() << "(" << m_id
@@ -51,6 +50,7 @@ struct tactic_report::imp {
                    << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
                    << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
                    << ")" << std::endl);
+        SASSERT(m_goal.is_well_formed());
     }
 };