diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 1dbe3be67..02ad786dd 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -493,7 +493,6 @@ namespace smt {
         TRACE("lemma", tout << strm.str() << "\n";);
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
-        if (m_lemma_id==6998) exit(0);
         return m_lemma_id;
     }
 
diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index 8132d7ed4..cccedff52 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -150,7 +150,6 @@ monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
 
 void emonomials::remove_cg(lpvar v) {
     cell* c = m_use_lists[v].m_head;
-    CTRACE("nla_solver", v == 14, tout << c << "\n";);
     if (c == nullptr) {
         return;
     }
@@ -160,7 +159,6 @@ void emonomials::remove_cg(lpvar v) {
         unsigned idx = c->m_index;
         c = c->m_next;
         monomial & m = m_monomials[idx];
-        CTRACE("nla_solver", v == 14, tout << m << "\n";);
         if (!is_visited(m)) {
             set_visited(m);
             remove_cg(idx, m);
@@ -201,7 +199,6 @@ void emonomials::remove_cg(unsigned idx, monomial& m) {
 */
 void emonomials::insert_cg(lpvar v) {
     cell* c = m_use_lists[v].m_head;
-    CTRACE("nla_solver", v == 14, tout << c << "\n";);
 
     if (c == nullptr) {
         return;
@@ -213,7 +210,6 @@ void emonomials::insert_cg(lpvar v) {
         unsigned idx = c->m_index;
         c = c->m_next;
         monomial & m = m_monomials[idx];
-        CTRACE("nla_solver", v == 14, tout << m << "\n";);
         if (!is_visited(m)) {
             set_visited(m);
             insert_cg(idx, m);
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index 25cebd2d9..69f823ead 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -112,9 +112,7 @@ void core::push() {
      
 void core::pop(unsigned n) {
     TRACE("nla_solver", tout << "n = " << n << "\n";);
-    TRACE("nla_solver", tout << "before pop mons = " << pp_emons(*this, m_emons) << "\n";);   
     m_emons.pop(n); 
-    TRACE("nla_solver", tout << "after pop mons = " << pp_emons(*this, m_emons) << "\n";);   
 }
 
 rational core::product_value(const unsigned_vector & m) const {
diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp
index f215c0bbb..daec49ff3 100644
--- a/src/util/lp/var_eqs.cpp
+++ b/src/util/lp/var_eqs.cpp
@@ -120,8 +120,6 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
 }
 
 void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const {
-    static int ddd=0;
-    TRACE("nla_solver", tout << ++ddd << "\n";);
     SASSERT(find(v1) == find(v2));
     if (v1 == v2) {
         return;