diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 94c8c6990..7339f5fe8 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -741,7 +741,15 @@ namespace nla {
 
         lp::lpvar j = c().lra.add_term(coeffs, UINT_MAX);
         c().lra.update_column_type_and_bound(j, lp::lconstraint_kind::EQ, offset, e.dep());
-        c().m_check_feasible = true; 
+        c().m_check_feasible = true;
+        TRACE(nla_solver,
+            // Print the term as installed (post subst_known_terms), not the
+            // pre-add_term coeffs vector. add_term normalizes/substitutes
+            // term-column references, so coeffs and the resulting row can
+            // diverge if any var is itself a term-column.
+            tout << "grobner-linear-eq: ";
+            c().lra.print_term(c().lra.get_term(j), tout);
+            tout << " = " << offset << "\n";);
         return true;
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 23c102874..b4016dca8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2126,6 +2126,14 @@ public:
         m_explanation = l.expl();
         literal_vector core;
         SASSERT(!m_lemma.is_empty());
+        TRACE(nla_solver,
+            tout << "varmap:";
+            for (lpvar j : m_nla->get_core().collect_vars(l)) {
+                auto ext = lp().local_to_external(j);
+                if (ext != lp::null_lpvar && static_cast<unsigned>(ext) < th.get_num_vars())
+                    tout << " " << lp().get_variable_name(j) << "=" << pp(ext);
+            }
+            tout << "\n";);
         for (auto const& ineq : m_lemma.ineqs()) {
             auto lit = mk_literal(ineq);
             core.push_back(~lit);