diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 047a5daff..97c8a0b3f 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -52,6 +52,7 @@ struct solver::imp {
     */
     lbool check() {        
         SASSERT(need_check());
+        m_zero = nullptr;
         m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
         m_zero = alloc(scoped_anum, am());
         m_term_set.clear();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1f7094886..ebf37daa1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3389,14 +3389,14 @@ public:
         if (t.is_term()) {
 
             m_todo_terms.push_back(std::make_pair(t, rational::one()));
-
+            TRACE("nl_value", tout << t.to_string() << "\n";);
             TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n";
                   lp().print_term(lp().get_term(t), tout) << "\n";);
 
             m_nla->am().set(r, 0);
             while (!m_todo_terms.empty()) {
                 rational wcoeff = m_todo_terms.back().second;
-                t = m_todo_terms.back().first;
+                t = m_todo_terms.back().first;                
                 m_todo_terms.pop_back();
                 lp::lar_term const& term = lp().get_term(t);
                 TRACE("nl_value", lp().print_term(term, tout) << "\n";);