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();