correctly process cancellation in gomory cuts

Signed-off-by: Lev Nachmanson <[email protected]>
Z3Prover · Sep 19, 2024 · 342dccd · 342dccd
1 parent b99c4a4
commit 342dccd
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -527,7 +527,7 @@ struct create_cut {
             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 @@ struct create_cut {
 
         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
@@ -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) {