From a7310462dfaaccef2db0e1deef50dedd2393e164 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 23 Feb 2025 19:38:20 -0800 Subject: [PATCH] throttle down cuts from proofs Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 1 - src/math/lp/lp_settings.h | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 2491f9577..2fe6cf37d 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1647,7 +1647,6 @@ namespace lp { return lia_move::conflict; } } - std::cout << "new tbs:" << m_tightened_columns.size() << "\n"; return lia_move::undef; } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 4c84edb40..842c91bc2 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -258,7 +258,7 @@ private: bool m_dio_enable_gomory_cuts = false; bool m_dio_enable_hnf_cuts = true; unsigned m_dio_branching_period = 100; // do branching rarely - unsigned m_dio_report_branch_with_term_tigthening_period = 4; // report the branch with term tigthening every 2 iterations + unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening public: bool print_external_var_name() const { return m_print_external_var_name; }