start using lar_solver::is_feasible() (#5697)

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Dec 6, 2021 · 9b4f3a7 · 9b4f3a7
1 parent 7758b51
commit 9b4f3a7
Showing 1 changed file with 7 additions and 14 deletions.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1529,7 +1529,7 @@ class theory_lra::imp {
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
         lbool is_sat = l_true;
         SASSERT(lp().ax_is_correct());
-        if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) {
+        if (!lp().is_feasible() || lp().has_changed_columns()) {
             is_sat = make_feasible();
         }
         final_check_status st = FC_DONE;
@@ -3083,21 +3083,14 @@ class theory_lra::imp {
         TRACE("pcs",  tout << lp().constraints(););
         auto status = lp().find_feasible_solution();
         TRACE("arith_verbose", display(tout););
-        switch (status) {
-        case lp::lp_status::INFEASIBLE:
-            return l_false;
-        case lp::lp_status::FEASIBLE:
-        case lp::lp_status::OPTIMAL:
-            //            SASSERT(lp().all_constraints_hold());
+        if (lp().is_feasible())
             return l_true;
-        case lp::lp_status::TIME_EXHAUSTED:
-
-        default:
-            TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
+        if (status == lp::lp_status::INFEASIBLE)  
+            return l_false;
+        TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
             // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, 
             // FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE
-            return l_undef;
-        }
+        return l_undef;
     }
 
     lp::explanation     m_explanation;
@@ -3467,7 +3460,7 @@ class theory_lra::imp {
             st = lp::lp_status::UNBOUNDED;
         }
         else {
-            if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) 
+            if (!lp().is_feasible() || lp().has_changed_columns()) 
                 make_feasible();
 
             vi = get_lpvar(v);