From 7135283135a23bc1d4c41043b1c2a1a58ddd7615 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jul 2023 13:23:17 -0700 Subject: [PATCH] update format and checker for implied-eq Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_proof.cpp | 2 -- src/sat/smt/sat_th.cpp | 3 --- 2 files changed, 5 deletions(-) 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(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())