From 423a7b6888001bb9f696dba184833d715e4b5600 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Jul 2023 09:46:59 -0700 Subject: [PATCH] also add separate cut rule Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_proof.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 55b5eff72..39c9879a6 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -255,7 +255,6 @@ namespace euf { smt_proof_hint* solver::mk_smt_hint(symbol const& n, unsigned nl, literal const* lits, unsigned ne, expr_pair const* eqs, unsigned nd, expr_pair const* deqs) { if (!use_drat()) return nullptr; - TRACE("euf", tout << "SMT hint " << n << "\n"); push(value_trail(m_lit_tail)); push(restore_vector(m_proof_literals));