From cc957011f2f10b134d005f38a41f6082b1642b52 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 29 Sep 2025 13:12:15 -0700
Subject: [PATCH] remove the too early return

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nra_solver.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 5ba367837..b368fdfec 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -355,7 +355,8 @@ struct solver::imp {
             m_nla_core.set_use_nra_model(true);
             break;
         case l_false:
-            return add_lemma(clause);
+            r = add_lemma(clause);
+            break;
         default:
             break;
         }
@@ -397,13 +398,14 @@ struct solver::imp {
                 UNREACHABLE();
                 return l_undef;
             }
-            // NSB review: what is this???
+            // Ignore a lemma which is satisfied
             if (m_nla_core.ineq_holds(inq))
                 return l_undef;
             lemma |= inq;
-            IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
-            return l_false;
         }
+        IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
+        m_nla_core.set_use_nra_model(true);
+        return l_false;
     }
 
     void constraint_core2ex(lp::explanation& ex) {