diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 096469e5e..cda8e3260 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -1463,10 +1463,9 @@ namespace lp {
         }
 
         // we have m_espace and m_lspace filled with an lra_term and the variables are substituted by S and fresh
-        lia_move tighten_bounds_for_term_column_bp() {
-            return lia_move::undef;
-            std::cout << "tighten_bounds_for_term_column_bp\n";
+        lia_move tighten_bounds_for_term_column_bp(unsigned j) {
             remove_fresh_from_espace();
+            // transform to lar variables
             for (auto & p: m_espace.m_data) p.m_j = local_to_lar_solver(p.var()); // have to restore it for the cleanup to work
             
             TRACE("dio",
@@ -1479,21 +1478,23 @@ namespace lp {
             m_prop_bounds.clear();
             bound_analyzer_on_row<std_vector<iv>, dioph_eq::imp>::analyze_row(m_espace.m_data, impq(- m_c), *this);
             lia_move r =  lia_move::undef;
-            bool change = false;
-            u_dependency * fixed_dep  = explain_fixed_in_meta_term(m_lspace.m_data); // not efficient : todo
+            u_dependency * dep  = explain_fixed_in_meta_term(m_lspace.m_data); // not efficient : todo
+            dep = lra.join_deps(explain_fixed(lra.get_term(j)), dep);
+            if (is_fixed(j)) dep = lra.join_deps(dep, lra.get_bound_constraint_witnesses_for_column(j));
             for (auto& pb: m_prop_bounds) {
-                pb.m_dep = lra.join_deps(pb.m_dep, fixed_dep);
+                pb.m_dep = lra.join_deps(pb.m_dep, dep);
                 if (update_bound(pb)) {
-                    change = true;
+                    TRACE("dio", tout << "change after update_bound pb.m_j:" << pb.m_j << "\n";);
+                    auto st = lra.find_feasible_solution();
+                    if (st == lp_status::INFEASIBLE) {
+                        lra.get_infeasibility_explanation(m_infeas_explanation);
+                        TRACE("dio", tout << "inf explanation:\n"; lra.print_explanation(tout, m_infeas_explanation););                      
+                        r = lia_move::conflict;
+                        break;
+                    }
+                    TRACE("dio", tout << "lra is feasible\n";);                        
                 }
             }
-            if (change) {
-                auto st = lra.find_feasible_solution();
-                if (st == lp_status::INFEASIBLE) {
-                    lra.get_infeasibility_explanation(m_infeas_explanation);
-                    r = lia_move::conflict;
-                }                
-            }
             for (auto & p: m_espace.m_data) p.m_j = lar_solver_to_local(p.var()); 
             return r;
         }
@@ -1501,7 +1502,7 @@ namespace lp {
         lia_move tighten_bounds_for_term_column(unsigned j) {
             auto r = tighten_bounds_for_term_column_gcd(j);
             if (r == lia_move::undef)
-                r = tighten_bounds_for_term_column_bp();
+                r = tighten_bounds_for_term_column_bp(j);
             return r;
         }
 
@@ -1513,7 +1514,12 @@ namespace lp {
             SASSERT(get_extended_term_value(term_to_tighten).is_zero() && all_vars_are_int(term_to_tighten));
             // q is the queue of variables that can be substituted in term_to_tighten
             protected_queue q;
-            TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;);
+            TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(term_to_tighten, tout) << std::endl;
+                  for( const auto& p : term_to_tighten) {
+                      lra.print_column_info(p.var(), tout);
+                  }
+                );
+            
             init_substitutions(term_to_tighten, q);
             if (q.empty()) // todo: maybe still go ahead and process it?
                 return lia_move::undef;
@@ -1526,7 +1532,7 @@ namespace lp {
             subs_with_S_and_fresh(q);          
             SASSERT(subs_invariant(term_to_tighten));
             mpq g = gcd_of_coeffs(m_espace.m_data, true);
-            TRACE("dioph_eq", tout << "after process_q_with_S\nt:";  print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
+            TRACE("dio", tout << "after process_q_with_S\nt:";  print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
 
             if (g.is_one())
                 return lia_move::undef;
@@ -1734,10 +1740,11 @@ namespace lp {
         }
 
         // return true iff the column bound has been changed
-        bool update_bound(const prop_bound& pb) {
-            lra.update_column_type_and_bound(pb.m_j, get_bound_kind(pb), pb.m_bound, pb.m_dep);            
-            if (lra.column_is_fixed(pb.m_j)) std::cout << "new fixed " << pb.m_j << "\n";
-            return lra.columns_with_changed_bounds().contains(pb.m_j);
+        bool update_bound(const prop_bound& pb) {            
+            TRACE("dio", tout << "pb: " << "x" << pb.m_j << ", low:" << pb.m_is_low << " , strict:" << pb.m_strict << " , bound:" << pb.m_bound << "\n"; lra.print_column_info(pb.m_j, tout, true););
+            bool r = lra.update_column_type_and_bound(pb.m_j, get_bound_kind(pb), pb.m_bound, pb.m_dep);
+            TRACE("dio", tout << "after: "; lra.print_column_info(pb.m_j, tout);tout <<"return " << r << "\n";);
+            return r;
         }
         
         bool row_has_int_inf(unsigned ei) {
@@ -1767,10 +1774,12 @@ namespace lp {
                     tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":"
                       << rs << std::endl;);
                 rs = (rs - m_c) / g;
-                TRACE("dio", tout << "(rs - m_c) / g:" << rs << std::endl;);
+                TRACE("dio", tout << "((rs - m_c) / g):" << rs << std::endl;);
                 if (!rs.is_int()) {
                     if (tighten_bound_kind(g, j, rs, is_upper, b_dep))
                         return lia_move::conflict;
+                } else {
+                    TRACE("dio", tout << "no improvement in the bound\n";);
                 }
             }
             
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 2ed233122..a249f827b 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1867,14 +1867,14 @@ namespace lp {
         }
     }
 
-    void lar_solver::update_column_type_and_bound(unsigned j,
+    bool lar_solver::update_column_type_and_bound(unsigned j,
         const mpq& right_side,
         constraint_index constr_index) {
         TRACE("lar_solver_feas", tout << "j = " << j << " was " << (this->column_is_feasible(j)?"feas":"non-feas") << std::endl;);
         m_constraints.activate(constr_index);
         lconstraint_kind kind = m_constraints[constr_index].kind();
         u_dependency* dep = m_constraints[constr_index].dep();
-        update_column_type_and_bound(j, kind, right_side, dep);
+        return update_column_type_and_bound(j, kind, right_side, dep);
     }
 
 
@@ -1956,7 +1956,8 @@ namespace lp {
         }
         ls.add_var_bound(tv, c.kind(), c.rhs());
     }
-    void lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    // return true iff a bound has been changed or or the criss-crossed bounds have been found
+    bool lar_solver::update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         // SASSERT(validate_bound(j, kind, right_side, dep));
         TRACE(
             "lar_solver_feas",
@@ -1972,11 +1973,12 @@ namespace lp {
             });
         bool was_fixed = column_is_fixed(j);
         mpq rs = adjust_bound_for_int(j, kind, right_side);
+        bool r;
         if (column_has_upper_bound(j))
-            update_column_type_and_bound_with_ub(j, kind, rs, dep);
+            r = update_column_type_and_bound_with_ub(j, kind, rs, dep);
         else
-            update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
-
+            r = update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
+ 
         if (!was_fixed && column_is_fixed(j) && m_fixed_var_eh)
             m_fixed_var_eh(j);
 
@@ -1987,6 +1989,7 @@ namespace lp {
         TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j) ? "feas" : "non-feas") << ", and " << (this->column_is_bounded(j) ? "bounded" : "non-bounded") << std::endl;);
         if (m_update_column_bound_callback)
             m_update_column_bound_callback(j);
+        return r;
     }
 
     void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
@@ -2021,27 +2024,27 @@ namespace lp {
         }
     };
    
-    void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    bool lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         SASSERT(column_has_upper_bound(j));
         if (column_has_lower_bound(j)) {
-            update_bound_with_ub_lb(j, kind, right_side, dep);
+            return update_bound_with_ub_lb(j, kind, right_side, dep);
         }
         else {
-            update_bound_with_ub_no_lb(j, kind, right_side, dep);
+            return update_bound_with_ub_no_lb(j, kind, right_side, dep);
         }
     }
 
-    void lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    bool lar_solver::update_column_type_and_bound_with_no_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         SASSERT(!column_has_upper_bound(j));
         if (column_has_lower_bound(j)) {
-            update_bound_with_no_ub_lb(j, kind, right_side, dep);
+            return update_bound_with_no_ub_lb(j, kind, right_side, dep);
         }
         else {
-            update_bound_with_no_ub_no_lb(j, kind, right_side, dep);
+            return update_bound_with_no_ub_no_lb(j, kind, right_side, dep);
         }
     }
 
-    void lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    bool lar_solver::update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j));
         lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed ||
                   m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed);
@@ -2057,7 +2060,7 @@ namespace lp {
                     set_crossed_bounds_column_and_deps(j, true, dep);
                 }
                 else {
-                    if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
+                    if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return false;
                     m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
                     set_upper_bound_witness(j, dep);
                     insert_to_columns_with_changed_bounds(j);
@@ -2072,9 +2075,7 @@ namespace lp {
                 if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
                     set_crossed_bounds_column_and_deps(j, false, dep);
                 } else {
-                    if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                        return;
-                    }
+                    if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) return false;
                     m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
                     set_lower_bound_witness(j, dep);
                     m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed);
@@ -2107,9 +2108,10 @@ namespace lp {
         numeric_pair<mpq> const& hi = m_mpq_lar_core_solver.m_r_upper_bounds[j];
         if (lo == hi)
             m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
+        return true;
     }
     
-    void lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    bool lar_solver::update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
         lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
 
@@ -2136,7 +2138,7 @@ namespace lp {
             case GE: {
                 auto low = numeric_pair<mpq>(right_side, y_of_bound);
                 if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                    return;
+                    return false;
                 }
                 m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
                 set_lower_bound_witness(j, dep);
@@ -2161,9 +2163,10 @@ namespace lp {
             default:
                 UNREACHABLE();
         }
+        return true;
     }
    
-    void lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    bool lar_solver::update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
         lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
         mpq y_of_bound(0);
@@ -2174,7 +2177,7 @@ namespace lp {
         case LE:
         {
             auto up = numeric_pair<mpq>(right_side, y_of_bound);
-            if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
+            if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return false;
             m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
             set_upper_bound_witness(j, dep);
             insert_to_columns_with_changed_bounds(j);
@@ -2216,9 +2219,10 @@ namespace lp {
         default:
             UNREACHABLE();
         }
+        return true;
     }
    
-    void lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
+    bool lar_solver::update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
         lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j));
 
         mpq y_of_bound(0);
@@ -2255,6 +2259,7 @@ namespace lp {
                 UNREACHABLE();
         }
         insert_to_columns_with_changed_bounds(j);
+        return true;
     }    
 
     lpvar lar_solver::to_column(unsigned ext_j) const {
@@ -2508,7 +2513,6 @@ namespace lp {
         u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
         SASSERT(bdep != nullptr);
         m_crossed_bounds_deps = m_dependencies.mk_join(bdep, dep);
-        insert_to_columns_with_changed_bounds(j);
     }
 
     void lar_solver::collect_more_rows_for_lp_propagation(){
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 2cb2d7c8d..72172abf3 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -156,19 +156,19 @@ class lar_solver : public column_namer {
     void add_constraint_to_validate(lar_solver& ls, constraint_index ci);
     bool m_validate_blocker = false;
     void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
-    void update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
+    bool update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
  public:   
     bool validate_blocker() const { return m_validate_blocker; }
     bool & validate_blocker() { return m_validate_blocker; }   
-	void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
  private:
     void require_nbasis_sort() { m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; }   
-    void update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
-    void update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
-    void update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
-    void update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
-    void update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
-    void update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
+    bool update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
     void register_in_fixed_var_table(unsigned, unsigned&);
     void remove_non_fixed_from_fixed_var_table();
     constraint_index add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side);
@@ -614,11 +614,12 @@ public:
     }
     inline bool column_has_term(lpvar j) const { return m_columns[j].term() != nullptr; }
 
-    std::ostream& print_column_info(unsigned j, std::ostream& out) const {
+    std::ostream& print_column_info(unsigned j, std::ostream& out, bool print_expl = false) const {
         m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
         if (column_has_term(j)) 
             print_term_as_indices(get_term(j), out) << "\n";       
-        display_column_explanation(out, j);
+        if (print_expl)
+            display_column_explanation(out, j);
         return out;
     }
 
@@ -627,10 +628,18 @@ public:
         svector<unsigned> vs1, vs2;
         m_dependencies.linearize(ul.lower_bound_witness(), vs1);
         m_dependencies.linearize(ul.upper_bound_witness(), vs2);
-        if (!vs1.empty())
-            out << "lo: " << vs1;
-        if (!vs2.empty())
-            out << "hi: " << vs2;
+        if (!vs1.empty()) {
+            out << " lo:\n";
+            for (unsigned ci : vs1) {
+                display_constraint(out, ci) << "\n";
+            }
+        }
+        if (!vs2.empty()) {
+            out << " hi:\n";
+            for (unsigned ci : vs2) {
+                display_constraint(out, ci) << "\n";
+            }
+        }     
         if (!vs1.empty() || !vs2.empty())
             out << "\n";
         return out;
diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h
index dbebbf998..48ad13686 100644
--- a/src/math/lp/numeric_pair.h
+++ b/src/math/lp/numeric_pair.h
@@ -239,6 +239,8 @@ struct numeric_pair {
     void neg() { x.neg(); y.neg(); }
     
     std::string to_string() const {
+        if (y.is_zero())
+            return T_to_string(x);
         return std::string("(") + T_to_string(x) + ", "  + T_to_string(y) + ")";
     }