diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 339b920d3..8f9299dbf 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -1801,12 +1801,12 @@ namespace lp {
             lp_status st = lra.find_feasible_solution();
             if (st == lp_status::CANCELLED)
                 return false;
-            if ((int)st >= (int)lp::lp_status::FEASIBLE) 
+            if (lp::is_sat(st))
                 return false;            
             lra.get_infeasibility_explanation(m_infeas_explanation);
             return true;
         }
-
+        
 
 // returns true only on a conflict
         bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper) {
@@ -1840,10 +1840,8 @@ namespace lp {
             lra.update_column_type_and_bound(j, kind, bound, dep);
 
             lp_status st = lra.find_feasible_solution();
-            if ((int)st >= (int)lp::lp_status::FEASIBLE) {
+            if (is_sat(st) || st == lp::lp_status::CANCELLED)
                 return false;
-            }
-            if (st == lp_status::CANCELLED) return false;
             lra.get_infeasibility_explanation(m_infeas_explanation);
             return true;
         }
@@ -2069,7 +2067,7 @@ namespace lp {
                 TRACE("dio_br", tout << "st:" << lp_status_to_string(st) << std::endl;);
                 if (st == lp_status::CANCELLED)
                     return lia_move::undef;
-                else if ((int)st >= (int)(lp_status::FEASIBLE)) {
+                else if (lp::is_sat(st)) {
                     // have a feasible solution
                     unsigned n_of_ii = get_number_of_int_inf();
                     TRACE("dio_br", tout << "n_of_ii:" << n_of_ii << "\n";);
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 11ea140c0..5ed17be01 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -74,11 +74,14 @@ enum class lp_status {
     OPTIMAL
 };
 
+inline bool is_sat(lp_status st) {
+    return st == lp_status::FEASIBLE || st == lp_status::OPTIMAL;
+}
+
 // when the ratio of the vector length to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only
 template <typename X>
 unsigned ratio_of_index_size_to_all_size() {
-        return 10;
-    
+    return 10;
 }
 
 const char* lp_status_to_string(lp_status status);