diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index e55726af6..39c9879a6 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -465,8 +465,6 @@ namespace euf {
 
     void solver::display_inferred(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
         expr_ref hint(proof_hint, m);
-        if (!proof_hint)
-            verbose_stream() << hint << "\n";
         if (!hint)
             hint = m.mk_const(m_smt, m.mk_proof_sort()); 
         visit_expr(out, hint);
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 51783f0a5..21e3883e8 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -240,9 +240,6 @@ namespace euf {
             m_literals[i] = lits[i];
         base_ptr += sizeof(literal) * n_lits;
         m_eqs = reinterpret_cast<enode_pair*>(base_ptr);
-        if (!pma) {
-            verbose_stream() << "null\n";
-        }
         for (i = 0; i < n_eqs; ++i) {
             m_eqs[i] = eqs[i];
             if (m_eqs[i].first->get_id() > m_eqs[i].second->get_id())