diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index 7398475fa..4b0863db3 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -161,6 +161,9 @@ namespace nla {
 
     void emonomials::remove_cg(lpvar v) {
         cell* c = m_use_lists[v].m_head;
+        if (c == nullptr) {
+            return;
+        }
         cell* first = c;
         inc_visited();
         do {
@@ -206,6 +209,10 @@ namespace nla {
     */
     void emonomials::insert_cg(lpvar v) {
         cell* c = m_use_lists[v].m_head;
+        if (c == nullptr) {
+            return;
+        }
+
         cell* first = c;
         inc_visited();
         do {
diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h
index 76b1242a7..70b8645c1 100644
--- a/src/util/lp/emonomials.h
+++ b/src/util/lp/emonomials.h
@@ -210,7 +210,12 @@ namespace nla {
         /**
            \brief obtain the representative canonized monomial up to sign.
         */
-        signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
+        //signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
+        signed_vars const& rep(signed_vars const& sv) const {
+            unsigned j = -1;
+            m_cg_table.find(sv.var(), j);
+            return m_canonized[m_var2index[j]];
+        }
 
         /**
            \brief the original sign is defined as a sign of the equivalence class representative.
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 0b07dde5c..1b748d102 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -46,10 +46,16 @@ bool lar_solver::get_track_pivoted_rows() const {
 
 
 lar_solver::~lar_solver(){
-    for (auto c : m_constraints)
+    TRACE("lar_solver", tout << "~enter\n";);
+    for (auto c : m_constraints) {
+        TRACE("lar_solver", tout << c << "\n";);
         delete c;
+    }
     for (auto t : m_terms)
         delete t;
+
+    TRACE("lar_solver", tout << "~exit\n";);
+    
 }
 
 bool lar_solver::is_term(var_index j) const {
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index d5f288f74..15c6d60c9 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -77,14 +77,14 @@ public:
 class core {
 public:
     var_eqs                  m_evars;
-    emonomials               m_emons;
-    lp::lar_solver           m_lar_solver;
+    lp::lar_solver&          m_lar_solver;
     vector<lemma> *          m_lemma_vec;
     svector<lpvar>           m_to_refine;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
     monotone                 m_monotone;
+    emonomials               m_emons;
 
     core(lp::lar_solver& s);