From 0027ae21e8125d83f235888f652532406e36b87f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 5 Jan 2025 17:00:54 -1000
Subject: [PATCH] bug fixes

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/dioph_eq.cpp | 21 +++++++++++++++------
 src/math/lp/lar_term.h   |  7 ++-----
 2 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 35e60d9ba..f411bc4a6 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -292,14 +292,14 @@ namespace lp {
                 TRACE("dioph_eq", m_s.lra.print_term(*m_t, tout); tout << ", m_t->j() =" << m_t->j() << std::endl;);
                 if (!contains(m_s.m_active_terms, m_t)) {
                     for (int i = m_s.m_added_terms.size() - 1; i >= 0; --i) {
-                        if (m_s.m_added_terms[i] == m_t) // the address is the same
-                            if (i != m_s.m_added_terms.size() -1) m_s.m_added_terms[i] = m_s.m_added_terms.back();
-                            m_s.m_added_terms.pop_back();
-                            break;
+                        if (m_s.m_added_terms[i] != m_t) continue;
+                        // the address is the same
+                        if (i != m_s.m_added_terms.size() -1) m_s.m_added_terms[i] = m_s.m_added_terms.back();
+                        m_s.m_added_terms.pop_back();
+                        return; // all is done since the term has not made it to entries, etc
                     }
-                    return;
                 }
-                NOT_IMPLEMENTED_YET();
+                // deregister the term that has been activated
                 for (const auto & p: m_t->ext_coeffs()) {                    
                     auto it = m_s.m_columns_to_terms.find(p.var());
                     SASSERT(it != m_s.m_columns_to_terms.end());
@@ -309,6 +309,15 @@ namespace lp {
                     }
                         
                 }
+                TRACE("dioph_eq", 
+                      tout << "the deleted term column in m_l_matrix" << std::endl;
+                      for  (auto p: m_s.m_l_matrix.column(m_t->j())) {
+                          tout << p.coeff()<< ", row " << p.var() << std::endl;
+                      }
+                      tout << "m_l_matrix has " << m_s.m_l_matrix.column_count() << std::endl;
+                      tout << "and" << m_s.m_l_matrix.row_count() << " rows" << std::endl;
+                    );
+                NOT_IMPLEMENTED_YET();
              }
         };
 
diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index 26ed64e95..c28630c21 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -36,7 +36,7 @@ public:
     lpvar j() const { return m_j; }
     void set_j(unsigned j) { 
         m_j = j;
-    }
+        }
     void add_monomial(const mpq& c, unsigned j) {
         if (c.is_zero())
             return;
@@ -275,10 +275,7 @@ public:
         const_iterator(u_map<mpq>::iterator it) : m_it(it) {}
         bool operator==(const const_iterator &other) const { return m_it == other.m_it; }
         bool operator!=(const const_iterator &other) const { return !(*this == other); }
-          // Return a pointer to the same object returned by operator*.
-        const ival* operator->() const {
-            return &(**this); 
-        }
+        
     };
    
     bool is_normalized() const {