From eaffe4646861764ba4d7db07e79d87c59d62b21e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Jun 2020 10:27:21 -0700
Subject: [PATCH] revert debug changes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_core.cpp   | 2 +-
 src/math/lp/nra_solver.cpp | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 24227da11..00db7bc42 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1497,7 +1497,7 @@ lbool core::check(vector<lemma>& l_vec) {
             m_tangents.tangent_lemma();
     }
 
-    if (!done() && m_nla_settings.run_nra()) {
+    if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {
         ret = m_nra.check();
         m_stats.m_nra_calls ++;
     }
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 2ea7d5c10..9b96671d3 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -73,8 +73,6 @@ struct solver::imp {
         }
         // TBD: add variable bounds?
 
-        m_nlsat->display(std::cout);
-
         lbool r = l_undef;
         try {
             r = m_nlsat->check();