diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 0815feee7..b3f11a4b4 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -387,7 +387,7 @@ namespace lp {
             }
         };
 
-        void remove_term_callback(const lar_term *t) { 
+        void undo_add_term_method(const lar_term *t) {
             TRACE("d_undo", tout << "t:"<< t<<", t->j():"<< t->j() << std::endl;);
             TRACE("dioph_eq", lra.print_term(*t, tout); tout << ", t->j() =" << t->j() << std::endl;);
             if (!contains(m_active_terms, t)) {
@@ -422,8 +422,18 @@ namespace lp {
                   tout << "and " << m_l_matrix.row_count() << " rows" << std::endl;
                   print_lar_term_L(*t, tout); tout << "; t->j()=" << t->j() << std::endl;
                 );
-            shrink_L_to_sizes();
+            shrink_matrices();
         }
+        
+        struct undo_add_term : public trail {
+            imp& m_s;
+            const lar_term* m_t;
+            undo_add_term(imp& s, const lar_term *t):  m_s(s),   m_t(t) {}
+
+            void undo() {
+                m_s.undo_add_term_method(m_t);
+            }
+        };
       
         struct undo_fixed_column : public trail {
             imp& m_imp;
@@ -504,7 +514,7 @@ namespace lp {
             m_l_matrix.add_rows(mpq(1), i, m_l_matrix.row_count() - 1);
         }
 
-        void shrink_L_to_sizes() {
+        void shrink_matrices() {
             unsigned i = m_l_matrix.row_count() - 1;            
             eliminate_last_term_column();
             remove_last_row_in_matrix(m_l_matrix);
@@ -564,7 +574,9 @@ namespace lp {
                 TRACE("dioph_eq", tout << "not all vars are integrall\n";);
                 return;
             }
-            m_added_terms.push_back(t);    
+            m_added_terms.push_back(t);
+            auto undo = undo_add_term(*this, t);
+            lra.trail().push(undo);
         }
 
         void update_column_bound_callback(unsigned j) {
@@ -578,7 +590,6 @@ namespace lp {
     public:
         imp(int_solver& lia, lar_solver& lra) : lia(lia), lra(lra) {
             lra.m_add_term_callback=[this](const lar_term*t){add_term_callback(t);};
-            lra.m_remove_term_callback = [this](const lar_term*t){remove_term_callback(t);};
             lra.m_update_column_bound_callback = [this](unsigned j){update_column_bound_callback(j);};
         }
         term_o get_term_from_entry(unsigned i) const {
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index a70b54c9d..91efbe389 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1558,11 +1558,8 @@ namespace lp {
             if (col.term() != nullptr) {
                 if (s.m_need_register_terms)
                     s.deregister_normalized_term(*col.term());
-                if (s.m_remove_term_callback) 
-                    s.m_remove_term_callback(col.term());
                 delete col.term();
                 s.m_terms.pop_back();
-                
             }
             s.remove_last_column_from_tableau();            
             s.m_columns.pop_back();
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index f3a4daa6f..e7d429cee 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -408,7 +408,6 @@ public:
     
     public:
     std::function<void (const lar_term*)> m_add_term_callback;
-    std::function<void (const lar_term*)> m_remove_term_callback;
     std::function<void (unsigned)> m_update_column_bound_callback;  
     bool external_is_used(unsigned) const;
     void pop(unsigned k);