From 4e21e126a8bef9e1035d67430593700d61a2683b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 21 Oct 2023 19:58:07 -0700
Subject: [PATCH] update add_lemmas to use check-feasible

---
 src/sat/smt/arith_solver.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index ebfe93dfe..cbccf7fa8 100644
--- 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);