From eba6a66e6f3d7923bd43a5d4a32e6c1f8ac76e33 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 13 Nov 2025 19:24:31 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index fe7e760a2..4e19eb555 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1177,12 +1177,6 @@ namespace nlsat { TRACE(nlsat_sort, display(tout << "mk_clause:\n", *cls) << "\n";); std::sort(cls->begin(), cls->end(), lit_lt(*this)); TRACE(nlsat, display(tout << " after sort:\n", *cls) << "\n";); - if (learned && m_log_lemmas) { - log_lemma(verbose_stream(), *cls); - } - if (learned && m_check_lemmas) { - check_lemma(cls->size(), cls->data(), false, cls->assumptions()); - } if (learned) m_learned.push_back(cls); else