diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 2a99fe10c..9342df445 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1231,6 +1231,10 @@ rational core::val(const factorization& f) const {
 
 void core::add_empty_lemma() {
     m_lemma_vec->push_back(lemma());
+    if (lp_settings().stats().m_nla_calls == 5 && m_lemma_vec->size() == 11) {
+        TRACE("nla_solver", tout << "bad lemma\n";);
+    }
+        
 }
     
 void core::negate_relation(unsigned j, const rational& a) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3305126c7..cbdad08d1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2221,11 +2221,13 @@ public:
         switch (r) {
         case l_false: {
             m_stats.m_nla_lemmas += lv.size();
+            int i = 0;
             for(const nla::lemma & l : lv) {
                 m_lemma = l; //todo avoid the copy
                 m_explanation = l.expl();
                 m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size());
                 false_case_of_check_nla();
+                i++;
             }
             break;
         }
@@ -3371,7 +3373,7 @@ public:
                 c.neg();
                 ctx().mark_as_relevant(c);
             }
-
+            TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
             // DEBUG_CODE(
             //     for (literal const& c : m_core) {
             //         if (ctx().get_assignment(c) == l_true) {