From ad965ac89663016d6842a89fbab1583605d2ddf7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2020 14:29:02 -0600 Subject: [PATCH] fix #2817 - rows may apparently not be correct (root cause of this tbd), but avoid Gomory on incorrect rows Signed-off-by: Nikolaj Bjorner --- src/util/lp/gomory.cpp | 3 ++- src/util/lp/int_solver.cpp | 3 +++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index ffcbd14c8..55d944885 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -268,7 +268,8 @@ public: for (auto & p : m_row) { m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), tout); } - tout << "inf_col = " << m_inf_col << std::endl;); + tout << "inf_col = " << m_inf_col << std::endl; + ); // gomory will be t <= k and the current solution has a property t > k m_k = 1; diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index e5a28182e..88122d8d0 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -147,6 +147,9 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) { if (!is_gomory_cut_target(row)) return create_branch_on_column(j); + if (!m_lar_solver->row_is_correct(row_of_basic_column(j))) + return lia_move::undef; + m_upper = true; return mk_gomory_cut(j, row); }