From 2d1f4d5d93e348af5f7c94756c4d215bd51f49b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Nov 2023 10:53:15 +0100 Subject: [PATCH] remove verbose logging --- src/smt/theory_arith_int.h | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index da1ee6bc7..4746040ce 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -437,17 +437,11 @@ namespace smt { */ template bool theory_arith::is_gomory_cut_target(row const & r) { - TRACE("gomory_cut", r.display(tout);); theory_var b = r.get_base_var(); for (auto& e : r) { // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed). - if (!e.is_dead() && e.m_var != b && (!at_bound(e.m_var) || !get_value(e.m_var).is_rational())) { - TRACE("gomory_cut", tout << "row is not gomory cut target:\n"; - display_var(tout, e.m_var); - tout << "at_bound: " << at_bound(e.m_var) << "\n"; - tout << "infinitesimal: " << !get_value(e.m_var).is_rational() << "\n";); + if (!e.is_dead() && e.m_var != b && (!at_bound(e.m_var) || !get_value(e.m_var).is_rational())) return false; - } } return true; }