From 342dccdc0223b10f03369b037d529b396f70843b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 19 Sep 2024 14:11:27 -0700
Subject: [PATCH] correctly process cancellation in gomory cuts

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/gomory.cpp | 5 ++++-
 src/math/lp/lia_move.h | 3 ++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 7b4347af5..6b7817769 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -527,7 +527,7 @@ public:
             has_small_cut = true;
             add_cut(cc.m_t, cc.m_k, cc.m_dep);
             if (lia.settings().get_cancel_flag())
-                return lia_move::undef;
+                return lia_move::cancelled;
         }
 
         if (big_cuts.size()) {
@@ -544,6 +544,9 @@ public:
         
         if (!_check_feasible())
             return lia_move::conflict;
+
+        if (lra.get_status() == lp_status::CANCELLED)
+            return lia_move::cancelled;        
         
         if (!lia.has_inf_int())
             return lia_move::sat;
diff --git a/src/math/lp/lia_move.h b/src/math/lp/lia_move.h
index 12e3d8e35..75ff67dcd 100644
--- a/src/math/lp/lia_move.h
+++ b/src/math/lp/lia_move.h
@@ -26,7 +26,8 @@ namespace lp {
         conflict,
         continue_with_check,
         undef,
-        unsat
+        unsat,
+        cancelled
     };
     inline std::string lia_move_to_string(lia_move m) {
         switch (m) {