diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index aa4ec4ac2..835e0d09c 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -355,7 +355,6 @@ namespace smt {
 
     void dyn_ack_manager::del_clause_eh(clause * cls) {
         m_context.m_stats.m_num_del_dyn_ack++;
-        
         app_pair p((app*)nullptr,(app*)nullptr);
         if (m_clause2app_pair.find(cls, p)) {
             SASSERT(p.first && p.second);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 8ca5ea887..e551f584a 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2928,12 +2928,12 @@ namespace smt {
         m_model_generator->reset();
         for (theory* t : m_theory_set) 
             t->flush_eh();
-        undo_trail_stack(0);
-        m_qmanager = nullptr;
         del_clauses(m_aux_clauses, 0);
         del_clauses(m_lemmas, 0);
         del_justifications(m_justifications, 0);
         reset_tmp_clauses();
+        undo_trail_stack(0);
+        m_qmanager = nullptr;
         if (m_is_diseq_tmp) {
             m_is_diseq_tmp->del_eh(m, false);
             m.dec_ref(m_is_diseq_tmp->get_owner());
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 25db74dc7..88c530857 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -258,7 +258,7 @@ struct purify_arith_proc {
         }
 
         void push_cnstr_pr(proof * def_pr) {
-            if (produce_proofs())
+            if (produce_proofs()) 
                 m_new_cnstr_prs.push_back(m().mk_th_lemma(u().get_family_id(), m_new_cnstrs.back(), 1, &def_pr));
         }
 
@@ -725,15 +725,15 @@ struct purify_arith_proc {
         r(q->get_expr(), new_body, new_body_pr);
         unsigned num_vars = r.cfg().m_new_vars.size();
         expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs;
-        cnstrs.push_back(new_body);
-        new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr());
+        if (true || !cnstrs.empty()) {
+            cnstrs.push_back(new_body);
+            new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr());
+        }
         TRACE("purify_arith", 
               tout << "num_vars: " << num_vars << "\n";
               tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";);
         if (num_vars == 0) {
             result = m().update_quantifier(q, new_body);
-            if (m_produce_proofs)
-                result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
         }
         else {
             // Add new constraints
@@ -757,11 +757,12 @@ struct purify_arith_proc {
             (*replacer)(new_body, new_body);
             new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight());
             result = m().update_quantifier(q, new_body);
-            if (m_produce_proofs) {
-                auto& cnstr_prs = r.cfg().m_new_cnstr_prs;
-                result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr())); 
-                r.cfg().push_cnstr_pr(result_pr);
-            }
+        }
+        if (m_produce_proofs) {
+            auto& cnstr_prs = r.cfg().m_new_cnstr_prs;
+            result_pr = m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr());
+            result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
+            r.cfg().push_cnstr_pr(result_pr);
         }
     }
 
@@ -784,6 +785,7 @@ struct purify_arith_proc {
         // add cnstraints
         sz = r.cfg().m_new_cnstrs.size();
         TRACE("purify_arith", tout << r.cfg().m_new_cnstrs << "\n";);
+        TRACE("purify_arith", tout << r.cfg().m_new_cnstr_prs << "\n";);
         for (unsigned i = 0; i < sz; i++) {
             m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr);
         }
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 3a29384dd..a55b1cafc 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -591,9 +591,11 @@ bool goal::is_well_formed() const {
         if (!::is_well_sorted(m(), t))
             return false;
 #if 0
-        SASSERT(m().get_fact(pr(i)) == form(i));
-        if (m().get_fact(pr(i)) != form(i))
+        if (m().get_fact(pr(i)) != form(i)) {
+            TRACE("tactic", tout << mk_ismt2_pp(pr(i), m()) << "\n" << mk_ismt2_pp(form(i), m()) << "\n";);
+            SASSERT(m().get_fact(pr(i)) == form(i));
             return false;
+        }
 #endif
     }
     return true;