diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 7795af30f..040f754ef 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1544,6 +1544,7 @@ lbool core::check() {
         scoped_limits sl(m_reslim);
         sl.push_child(&m_nra_lim);
         ret = m_nra.check_assignment();
+        IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";);
     }
 
     if (no_effect()) {
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 3817bf70b..f25cd97e4 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -358,6 +358,8 @@ struct solver::imp {
                         default:
                             UNREACHABLE();
                     }
+
+                    IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
                 }
                 m_nla_core.set_use_nra_model(true);
                 break;
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 234109939..c7fa51825 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -2316,6 +2316,10 @@ namespace nlsat {
         m_imp->m_simplify_cores = f;
     }
 
+    void explain::set_linear_project(bool f) {
+        m_imp->m_linear_project = f;
+    }
+
     void explain::set_full_dimensional(bool f) {
         m_imp->m_full_dimensional = f;
     }
@@ -2336,10 +2340,6 @@ namespace nlsat {
         (*m_imp)(n, ls, result);
     }
 
-    void explain::linear_project(unsigned n, literal const* ls, scoped_literal_vector& result) {
-        m_imp->linear_project(n, ls, result);
-    }
-
     void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
         m_imp->project(x, n, ls, result);
     }
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index de9502c9b..316a1367e 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -66,8 +66,6 @@ namespace nlsat {
         */
         void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result);
 
-        void linear_project(unsigned n, literal const* ls, scoped_literal_vector& result);
-
         
         /**
            \brief projection for a given variable.
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index a6f11256a..0961f4ee0 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2078,7 +2078,9 @@ namespace nlsat {
             // assignment does not satisfy the constraints -> create lemma
             SASSERT(best_literal != null_literal);
             m_lazy_clause.reset();
-            m_explain.linear_project(1, &best_literal, m_lazy_clause);
+            m_explain.set_linear_project(true);
+            m_explain.main_operator(1, &best_literal, m_lazy_clause);
+            m_explain.set_linear_project(false);
             m_lazy_clause.push_back(~best_literal);
 
             core.clear();