diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 8e2c4d0d8..8310064df 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -32,7 +32,6 @@ template <typename C, typename B> // C plays a role of a container, B - lp_bound
 class bound_analyzer_on_row {
     const C&                           m_row;
     B &                                m_bp;
-    unsigned                           m_row_index;
     int                                m_column_of_u; // index of an unlimited from above monoid
     // -1 means that such a value is not found, -2 means that at least two of such monoids were found
     int                                m_column_of_l; // index of an unlimited from below monoid
@@ -43,12 +42,10 @@ public :
     bound_analyzer_on_row(
         const C & it,
         const numeric_pair<mpq>& rs,
-        unsigned row_or_term_index,
         B & bp)
         :
         m_row(it),
         m_bp(bp),
-        m_row_index(row_or_term_index),
         m_column_of_u(-1),
         m_column_of_l(-1),
         m_rs(rs)
@@ -57,9 +54,8 @@ public :
     
     static unsigned analyze_row(const C & row,
                             const numeric_pair<mpq>& rs,
-                            unsigned row_or_term_index,
                             B & bp) {
-        bound_analyzer_on_row a(row, rs, row_or_term_index, bp);
+        bound_analyzer_on_row a(row, rs, bp);
         return a.analyze();
     }
 
@@ -281,16 +277,16 @@ private:
 
     void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict)
     {
-        unsigned row_index = this->m_row_index;
         auto* lar = &m_bp.lp();
-        auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index, lar]() {
+        const auto& row = this->m_row;
+        auto explain = [row, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, lar]() {
             (void) strict;
-            TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
+            TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << "\n";);
             int bound_sign = (is_lower_bound ? 1 : -1);
             int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
 
             u_dependency* ret = nullptr;
-            for (auto const& r : lar->get_row(row_index)) {
+            for (auto const& r : row) {
                 unsigned j = r.var();
                 if (j == bound_j)
                     continue;
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 60ddbe374..2491f9577 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -485,6 +485,7 @@ namespace lp {
         indexed_uint_set m_changed_rows;
         indexed_uint_set m_changed_columns;
         indexed_uint_set m_changed_terms;  // a term is defined by its column j, as in lar_solver.get_term(j)
+        indexed_uint_set m_tightened_columns; // the column that got tightened by the tigthening phase, 
         // m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j
         std::unordered_map<unsigned, std::unordered_set<unsigned>> m_columns_to_terms;
 
@@ -1361,6 +1362,7 @@ namespace lp {
             // Copy changed terms to another vector for sorting
             std_vector<unsigned> sorted_changed_terms;
             std_vector<unsigned> cleanup;
+            m_tightened_columns.reset();
             for (unsigned j : m_changed_terms) {
                 if ( 
                     j >= lra.column_count() ||
@@ -1620,8 +1622,11 @@ namespace lp {
             }
         }
 
+        lia_move propagate_bounds_on_tightened_columns() {
+            return lia_move::undef;
+        }
         // m_espace contains the coefficients of the term
-        // m_c contains the constant term
+        // m_c contains the fixed part of the term
         // m_tmp_l is the linear combination of the equations that removes the
         // substituted variables.
         // returns true iff the conflict is found
@@ -1642,6 +1647,7 @@ namespace lp {
                         return lia_move::conflict;
                 }
             }
+            std::cout << "new tbs:" << m_tightened_columns.size() << "\n";
             return lia_move::undef;
         }
 
@@ -1649,7 +1655,7 @@ namespace lp {
         bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper,
                                 u_dependency* prev_dep) {
             // ub = (upper_bound(j) - m_c)/g.
-            // we have x[j] = t = g*t_+ m_c <= upper_bound(j), then
+            // we have xj = t = g*t_+ m_c <= upper_bound(j), then
             // t_ <= floor((upper_bound(j) - m_c)/g) = floor(ub)
             //
             // so xj = g*t_+m_c <= g*floor(ub) + m_c is new upper bound
@@ -1679,6 +1685,7 @@ namespace lp {
             lra.update_column_type_and_bound(j, kind, bound, dep);
             lp_status st = lra.find_feasible_solution();
             if ((int)st >= (int)lp::lp_status::FEASIBLE) {
+                m_tightened_columns.insert(j);
                 return false;
             }
             if (st == lp_status::CANCELLED) return false;
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 681a684ab..7962888e7 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -185,7 +185,6 @@ class lar_solver : public column_namer {
         return bound_analyzer_on_row<row_strip<mpq>, lp_bound_propagator<T>>::analyze_row(
             A_r().m_rows[row_index],
             zero_of_type<numeric_pair<mpq>>(),
-            row_index,
             bp);
     }