diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index fe326ab22..b70c39c6e 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -79,7 +79,7 @@ namespace smt {
                 expr * arg1   = m_app1->get_arg(i);
                 expr * arg2   = m_app2->get_arg(i);
                 if (arg1 != arg2) {
-                    app * eq  = ctx.mk_eq_atom(arg1, arg2);
+                    app * eq  = m.mk_eq(arg1, arg2);
                     app_ref neq(m.mk_not(eq), m);
                     if (std::find(lits.begin(), lits.end(), neq.get()) == lits.end()) {
                         lits.push_back(neq);
@@ -89,7 +89,7 @@ namespace smt {
             }
             proof * antecedents[2];
             antecedents[0]   = m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr());
-            app * eq         = ctx.mk_eq_atom(m_app1, m_app2);
+            app * eq         = m.mk_eq(m_app1, m_app2);
             antecedents[1]   = mk_hypothesis(m, eq, true, m_app1, m_app2);
             proof * false_pr = m.mk_unit_resolution(2, antecedents);
             lits.push_back(eq);
@@ -485,9 +485,9 @@ namespace smt {
         justification * js = nullptr;
         if (m.proofs_enabled()) {
             js = alloc(dyn_ack_eq_justification, n1, n2, r, 
-                       to_app(ctx.bool_var2expr(eq1.var())), 
-                       to_app(ctx.bool_var2expr(eq2.var())),
-                       to_app(ctx.bool_var2expr(eq3.var())));
+                       m.mk_eq(n1, r),
+                       m.mk_eq(n2, r),
+                       m.mk_eq(n1, n2));
         }
         clause * cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 8da396009..94144e0bd 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1256,8 +1256,7 @@ namespace smt {
 
     void conflict_resolution::mk_conflict_proof(b_justification conflict, literal not_l) {
         SASSERT(conflict.get_kind() != b_justification::BIN_CLAUSE);
-        SASSERT(conflict.get_kind() != b_justification::AXIOM);
-        SASSERT(not_l == null_literal || conflict.get_kind() == b_justification::JUSTIFICATION);
+        SASSERT(not_l == null_literal || conflict.get_kind() == b_justification::AXIOM || conflict.get_kind() == b_justification::JUSTIFICATION);
         TRACE("mk_conflict_proof", m_ctx.display_literals(tout << "lemma literals:", m_lemma) << "\n";);
 
         reset();
@@ -1350,6 +1349,7 @@ namespace smt {
             m_lemma_proof = pr;
         else
             m_lemma_proof = m.mk_lemma(pr, fact);
+        TRACE("mk_conflict_proof", tout << mk_pp(m_lemma_proof, m) << "\n";);
         m_new_proofs.reset();
         reset();
     }