From a7bfdcd0ea4d9d4b6b080e3140e6e01836212806 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jan 2024 11:17:59 -0800 Subject: [PATCH] readd big cuts Signed-off-by: Nikolaj Bjorner --- src/math/lp/gomory.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 7916f66f7..dbe1194cb 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -561,11 +561,10 @@ public: bool feas = _check_feasible(); lra.pop(1); - if (lia.settings().get_cancel_flag()) - return lia_move::undef; - - if (!feas) - return lia_move::conflict; + if (!feas) + for (auto const& cut : big_cuts) + add_cut(cut); + } // this way we create bounds for the variables in polar cases even where the terms had big numbers