From 5de0b8a87fbae6a717ec909b3a39278c0e950e15 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 29 Sep 2025 13:20:46 -0700
Subject: [PATCH] do not set use_nra_model to true

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nra_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index b368fdfec..85a55cd6b 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -404,7 +404,7 @@ struct solver::imp {
             lemma |= inq;
         }
         IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
-        m_nla_core.set_use_nra_model(true);
+        //m_nla_core.set_use_nra_model(true);
         return l_false;
     }