- When removing a fresh var xt, collect all fresh defs that transitively reference it

- Remove them all from m_fresh_k2xt_terms and m_row2fresh_defs
    - Mark rows containing those vars in m_changed_rows for recalculation
    - Move remove_irrelevant_fresh_defs() before the recalculate loop so all affected rows get recalculated

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/dioph_eq.cpp

@@ -752,6 +752,7 @@ namespace lp {
             
             m_var_register.shrink(m_e_matrix.column_count());
 
+            remove_out_of_bounds_fresh_defs();
             remove_irrelevant_fresh_defs_for_row(i);
 
             if (m_k2s.has_val(i)) 
@@ -907,7 +908,6 @@ namespace lp {
                 return;
             }
             substitute_on_q(ei);
-            SASSERT(entry_invariant(ei));
         }
 
         void substitute_on_q_with_entry_in_S(unsigned ei, unsigned j, const mpq& alpha) {
@@ -1016,17 +1016,86 @@ namespace lp {
             }
         }
 
+        // Remove fresh definitions whose terms reference the given variable
+        // Mark rows containing stale fresh variable for recalculation
+        void handle_stale_var_in_matrix(unsigned xt) {
+            if (xt >= m_e_matrix.column_count())
+                return;
+            // Mark all rows containing xt for recalculation
+            for (const auto& cell : m_e_matrix.m_columns[xt])
+                m_changed_rows.insert(cell.var());
+        }
+
+        // Collect all fresh vars that directly or transitively reference removed_xt
+        void collect_dependent_fresh_vars(unsigned removed_xt, std_vector<unsigned>& to_remove) {
+            std_vector<unsigned> newly_found;
+            for (const auto& p : m_fresh_k2xt_terms.m_bij.key_val_pairs()) {
+                unsigned xt = p.second;
+                if (xt == removed_xt) continue;
+                if (std::find(to_remove.begin(), to_remove.end(), xt) != to_remove.end())
+                    continue; // already marked for removal
+                const lar_term& term = m_fresh_k2xt_terms.get_by_val(xt).first;
+                // Check if term contains removed_xt or any var already marked for removal
+                if (term.contains(removed_xt)) {
+                    newly_found.push_back(xt);
+                } else {
+                    for (unsigned marked : to_remove)
+                        if (term.contains(marked)) {
+                            newly_found.push_back(xt);
+                            break;
+                        }
+                }
+            }
+            for (unsigned xt : newly_found)
+                to_remove.push_back(xt);
+            // Recurse if we found new ones (they might have dependents too)
+            if (!newly_found.empty())
+                for (unsigned xt : newly_found)
+                    collect_dependent_fresh_vars(xt, to_remove);
+        }
+
+        // Deep clean: remove fresh var and all dependents, clean m_e_matrix
+        void deep_remove_fresh_var(unsigned removed_xt) {
+            if (!m_fresh_k2xt_terms.has_second_key(removed_xt))
+                return;
+            
+            // Collect all vars that need to be removed (removed_xt and its dependents)
+            std_vector<unsigned> to_remove;
+            to_remove.push_back(removed_xt);
+            collect_dependent_fresh_vars(removed_xt, to_remove);
+            
+            // Remove them all
+            for (unsigned xt : to_remove) {
+                if (!m_fresh_k2xt_terms.has_second_key(xt))
+                    continue;
+                // Get the row before erasing
+                unsigned row = m_fresh_k2xt_terms.get_by_val(xt).second;
+                m_fresh_k2xt_terms.erase_by_second_key(xt);
+                // Update m_row2fresh_defs
+                auto it = m_row2fresh_defs.find(row);
+                if (it != m_row2fresh_defs.end()) {
+                    it->second.erase(std::remove(it->second.begin(), it->second.end(), xt), it->second.end());
+                    if (it->second.empty())
+                        m_row2fresh_defs.erase(it);
+                }
+                // Mark rows containing xt for recalculation
+                handle_stale_var_in_matrix(xt);
+            }
+        }
+
         void remove_irrelevant_fresh_defs_for_row(unsigned ei) {
             auto it = m_row2fresh_defs.find(ei);
             if (it == m_row2fresh_defs.end()) return;
-            for (unsigned xt : it->second) {
+            // Copy the list since deep_remove_fresh_var modifies m_row2fresh_defs
-                if (m_fresh_k2xt_terms.has_second_key(xt))
+            std_vector<unsigned> xts_to_remove = it->second;
-                    m_fresh_k2xt_terms.erase_by_second_key(xt);
+            for (unsigned xt : xts_to_remove)
-            }
+                deep_remove_fresh_var(xt);
-            m_row2fresh_defs.erase(it);
+            // Ensure the row entry is removed (might already be gone)
+            m_row2fresh_defs.erase(ei);
         }
 
-        void remove_irrelevant_fresh_defs() {
+        // Remove fresh definitions for columns that are out of bounds after shrinking
+        void remove_out_of_bounds_fresh_defs() {
             std_vector<unsigned> xt_to_remove;
             std_vector<unsigned> rows_to_remove_the_defs_from;
             for (const auto& p : m_fresh_k2xt_terms.m_bij.key_val_pairs()) {
@@ -1037,17 +1106,18 @@ namespace lp {
                 }
             }
 
-            for (unsigned xt : xt_to_remove) {
+            for (unsigned xt : xt_to_remove)
-                m_fresh_k2xt_terms.erase_by_second_key(xt);
+                deep_remove_fresh_var(xt);
-            }
 
-            for (unsigned ei : m_changed_rows) {
+            for (unsigned ei : rows_to_remove_the_defs_from)
                 remove_irrelevant_fresh_defs_for_row(ei);
-            }
+        }
 
-            for (unsigned ei : rows_to_remove_the_defs_from) {
+        void remove_irrelevant_fresh_defs() {
+            remove_out_of_bounds_fresh_defs();
+
+            for (unsigned ei : m_changed_rows)
                 remove_irrelevant_fresh_defs_for_row(ei);
-            }
         }
 
         // this is a non-const function - it can set m_some_terms_are_ignored to true
@@ -1089,6 +1159,9 @@ namespace lp {
             for (unsigned ei : more_changed_rows)
                 m_changed_rows.insert(ei);
             
+            // Remove irrelevant fresh defs first - this may add more rows to m_changed_rows
+            remove_irrelevant_fresh_defs();
+            
             for (unsigned ei : m_changed_rows) {
                 if (ei >= m_e_matrix.row_count())
                     continue;
@@ -1100,11 +1173,11 @@ namespace lp {
                 if (!m_e_matrix.m_columns.empty() && m_e_matrix.m_columns.back().size() == 0) {
                     m_e_matrix.m_columns.pop_back();
                     m_var_register.shrink(m_e_matrix.column_count());
+                    remove_out_of_bounds_fresh_defs();
                 }
                 if (!m_l_matrix.m_columns.empty() && m_l_matrix.m_columns.back().size() == 0)
                     m_l_matrix.m_columns.pop_back();
             }
-            remove_irrelevant_fresh_defs();
             eliminate_substituted_in_changed_rows();
             m_changed_f_columns.reset();
             m_changed_rows.reset();