From 6b433b54e240540108e09fe4ea2a563d3d3e03ba Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 11 May 2020 16:38:48 -0700
Subject: [PATCH] disable the call to nlsat from nla_solver

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

diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 3180c58eb..c5403b66f 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -34,7 +34,7 @@ lbool solver::run_nra(lp::explanation & expl) {
 lbool solver::check(vector<lemma>& l, lp::explanation& expl) {    
     set_use_nra_model(false);
     lbool ret = m_core->check(l);
-    if (ret == l_undef) {
+    if (false && ret == l_undef) { // disable the call to nlsat
         ret = run_nra(expl);
         if (ret == l_true || expl.size() > 0) {
             set_use_nra_model(true);