check cancel flag to avoid unsound conflicts

src/math/lp/int_solver.cpp

@@ -208,6 +208,7 @@ namespace lp {
 #endif
         m_cut_vars.reset();
         if (r == lia_move::undef) r = int_branch(*this)();
+        if (settings().get_cancel_flag()) r = lia_move::undef;        
         return r;
     }
 
@@ -854,14 +855,16 @@ namespace lp {
 
         struct ex { explanation m_ex; lar_term m_term; mpq m_k; bool m_is_upper; };
         vector<ex> cuts;
-        for (unsigned i = 0; i < num_cuts && has_inf_int() && !settings().get_cancel_flag(); ++i) {
+        for (unsigned i = 0; i < num_cuts && has_inf_int(); ++i) {
             m_ex->clear();
             m_t.clear();
             m_k.reset();
             auto r = cut_fn();
             if (r != lia_move::cut)
                 break;
             cuts.push_back({ *m_ex, m_t, m_k, is_upper() });
+            if (settings().get_cancel_flag())
+                return lia_move::undef;
         }
         m_cut_vars.reset();
 
@@ -882,7 +885,7 @@ namespace lp {
 
         auto _check_feasible = [&](void) {
             auto st = lra.find_feasible_solution();
-            if (!lra.is_feasible()) {                
+            if (!lra.is_feasible() && !settings().get_cancel_flag()) {
                 lra.get_infeasibility_explanation(*m_ex);
                 return false;
             }
@@ -910,6 +913,9 @@ namespace lp {
             bool feas = _check_feasible();
             lra.pop(1);
 
+            if (settings().get_cancel_flag())
+                return lia_move::undef;
+
             if (!feas)
                 return lia_move::conflict;
 

src/math/lp/nla_core.cpp

@@ -1567,6 +1567,8 @@ lbool core::check() {
               {1, check3} };
         check_weighted(3, checks);
 
+        if (lp_settings().get_cancel_flag())
+            return l_undef;
         if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible)
             return l_false;
     }