update add_lemmas to use check-feasible

Z3Prover · Oct 22, 2023 · 4e21e12 · 4e21e12
1 parent c9d298e
commit 4e21e12
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -1484,6 +1484,13 @@ namespace arith {
     }
 
     void solver::add_lemmas() {
+        if (m_nla->check_feasible()) {
+            auto is_sat = make_feasible();
+            if (l_false == is_sat) {
+                get_infeasibility_explanation_and_set_conflict();
+                return;
+            }
+        }
         for (auto const& ineq : m_nla->literals()) {
             auto lit = mk_ineq_literal(ineq);
             ctx.mark_relevant(lit);