readd big cuts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 2, 2024 · a7bfdcd · a7bfdcd
1 parent 84997f8
commit a7bfdcd
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -561,11 +561,10 @@ struct create_cut {
             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