diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 3bbef73e3..7fc23ccc6 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -70,18 +70,17 @@ class lp_bound_propagator {
     };
 
     static int other(int x, int y, int z) { SASSERT(x == z || y == z); return x == z ? y : x; }
-    std::ostream& print(std::ostream & out, const vertex* v) const {
-        out << "c = " << v->column() << ", P = {";
+    std::ostream& print_vert(std::ostream & out, const vertex* v) const {
+        out << "(c = " << v->column() << ", parent = {";
         if (v->parent()) { out << "(" << v->parent()->column() << ")";}
         else { out << "null"; }
         out <<  "} , lvl = " << v->level();
-        if (fixed_phase()) {
-            out << " fixed phase";
-        } if (m_pol.contains(v->column())) {
+        if (m_pol.contains(v->column())) {
             out << (pol(v) == -1? " -":" +");
         } else {
             out << " not in m_pol";
         }
+        out << ')';
         return out;
     }
 
@@ -103,14 +102,12 @@ class lp_bound_propagator {
     // x[m_root->column()] - m_pol[j].pol()*x[j] == const;
     // to bind polarity and the vertex in the table
     struct pol_vert {
-        int           m_polarity { -2 };
-        unsigned      m_row_index { 0 };
-        const vertex* m_v { nullptr };
-    pol_vert() {}
-    pol_vert(int p, unsigned r, const vertex* v): m_polarity(p), m_row_index(r), m_v(v) {}
+        int m_polarity;
+        const vertex* m_v;
+        pol_vert() {}
+        pol_vert(int p, const vertex* v): m_polarity(p), m_v(v) {}
         int pol() const { return m_polarity; }
         const vertex* v() const { return m_v; }
-        unsigned row() const { return m_row_index; }
     };
     u_map<pol_vert>                                     m_pol; 
     // if m_pos.contains(j) then  x[j] = x[m_root->column()] + o
@@ -211,18 +208,31 @@ public:
     }
     
     void try_add_equation_with_lp_fixed_tables(const vertex *v) {
+        static int count = 0;
+        std::cout << ++count << std::endl;
+        if (count == 21)
+            enable_trace("cheap_eq");
         SASSERT(m_fixed_vertex);
         unsigned v_j = v->column();
         unsigned j = null_lpvar;
         if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) 
             return;
-        TRACE("cheap_eq", tout << "found j = " << j << " v_j = " << v_j << " for v = ";
-              print(tout, v) << "\n in lp.fixed tables\n";);
-        vector<edge> path;
-        find_path_on_tree(path, v, m_fixed_vertex);
+
+        TRACE("cheap_eq", tout << "v_j = "; lp().print_column_info(v_j, tout) << std::endl;);
+        TRACE("cheap_eq", tout << "v = "; print_vert(tout, v) << std::endl;);        
+        TRACE("cheap_eq", tout << "found j " << j << std::endl;
+              lp().print_column_info(j, tout)<< std::endl;);
+        TRACE("cheap_eq", tout << "found j = " << j << std::endl;);
+        vector<edge> path = connect_u_v_in_tree(v, m_fixed_vertex);
         explanation ex = get_explanation_from_path(path);
+        TRACE("cheap_eq", tout << "path expl = \n"; print_expl(tout, ex) << std::endl;);
+        TRACE("cheap_eq", tout << "fixed vert= \n";   print_vert(tout, m_fixed_vertex) << std::endl;);
+        TRACE("cheap_eq", tout << "fix vert expl = \n"; print_expl(tout, m_fixed_vertex_explanation) << std::endl;);
         ex.add_expl(m_fixed_vertex_explanation);
+        explain_fixed_column(j, ex);
+        TRACE("cheap_eq", tout << "full expl = \n"; print_expl(tout, ex) << std::endl;);
         add_eq_on_columns(ex, j, v->column());
+        
     }
 
     void try_add_equation_with_val_table(const vertex *v) {
@@ -238,9 +248,8 @@ public:
             return;
     
         TRACE("cheap_eq", tout << "found j=" << j << " for v=";
-              print(tout, v) << "\n in m_vals_to_verts\n";);
-        vector<edge> path;
-        find_path_on_tree(path, u, v);
+              print_vert(tout, v) << "\n in m_vals_to_verts\n";);
+        vector<edge> path = connect_u_v_in_tree(u, v);
         explanation ex = get_explanation_from_path(path);
         ex.add_expl(m_fixed_vertex_explanation);
         add_eq_on_columns(ex, j, v_j);
@@ -260,39 +269,30 @@ public:
     // pol for polarity
     int pol(const vertex* v) const { return pol(v->column()); }
     int pol(unsigned j) const { return m_pol[j].pol(); }
-    void set_polarity(const vertex* v, unsigned r, int p) {
+    void set_polarity(const vertex* v, int p) {
         SASSERT(p == 1 || p == -1);
         unsigned j = v->column();
         SASSERT(!m_pol.contains(j));
-        m_pol.insert(j, pol_vert(p, r, v));
+        m_pol.insert(j, pol_vert(p, v));
     }
 
     void check_and_set_polarity(vertex* v, int polarity, unsigned row_index) {
         pol_vert prev_pol;
         if (!m_pol.find(v->column(), prev_pol)) {
-            set_polarity(v, row_index, polarity);
+            set_polarity(v, polarity);
             return;
         }
         if (prev_pol.pol() == polarity)
             return;
-        return;
-        //
-        // TODO disabled pending fix for #5127
-        // the explanation is missing some terms. 
-        // Probably because in this case there isn't a single, but two paths
-        // from u to v. The bounds for the fixed variables for the two paths
-        // have to be taken into account.
-        // 
         const vertex *u = prev_pol.v();
         // we have a path L between u and v with p(L) = -1, that means we can
         // create an equality of the form x + x = a, where x = v->column() = u->column()
-        vector<edge> path;
-        find_path_on_tree(path, u, v);
+        vector<edge> path = connect_u_v_in_tree(u, v);
         m_fixed_vertex_explanation = get_explanation_from_path(path);
         explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
         set_fixed_vertex(v);
         TRACE("cheap_eq", 
-              tout << "polarity switch: " << row_index << " pol: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
+              tout << "polarity switch: " << polarity << "\nv = "; print_vert(tout , v) << "\nu = "; print_vert(tout, u) << "\n";
               tout << "fixed vertex explanation\n";
               for (auto p : m_fixed_vertex_explanation) 
                   lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci()););
@@ -326,7 +326,7 @@ public:
         }
         TRACE("cheap_eq", print_row(tout, row_index););
         m_root = alloc_v(x);
-        set_polarity(m_root, row_index, 1); // keep m_root in the positive table
+        set_polarity(m_root, 1); // keep m_root in the positive table
         if (not_set(y)) {
             set_fixed_vertex(m_root);
             explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
@@ -389,10 +389,10 @@ public:
     }
 
     void check_for_eq_and_add_to_val_table(vertex* v,  map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>>& table) {
-        TRACE("cheap_eq", tout << "v = "; print(tout, v) << "\n";);
+        TRACE("cheap_eq", tout << "v = "; print_vert(tout, v) << "\n";);
         const vertex *k; // the other vertex
         if (table.find(val(v), k)) {
-            TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";);
+            TRACE("cheap_eq", tout << "found k " ; print_vert(tout, k) << "\n";);
             if (k->column() != v->column() &&
                 is_int(k->column()) == is_int(v->column()) &&
                 !is_equal(k->column(), v->column())) {
@@ -401,13 +401,13 @@ public:
                 TRACE("cheap_eq", tout << "no report\n";);
             }
         } else {
-            TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print(tout, v) << "} \n";);
+            TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print_vert(tout, v) << "} \n";);
             table.insert(val(v), v);
         }
     }
     
     void check_for_eq_and_add_to_val_tables(vertex* v) {
-        TRACE("cheap_eq_det", print(tout, v) << "\n";);
+        TRACE("cheap_eq_det", print_vert(tout, v) << "\n";);
         if (!fixed_phase()) {
             if (pol(v->column()) == -1)
                 check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg);
@@ -443,16 +443,22 @@ public:
         SASSERT(v_i != v_j);
         SASSERT(lp().get_column_value(v_i->column()) == lp().get_column_value(v_j->column()));
         TRACE("cheap_eq", tout << v_i->column() << " = " << v_j->column() << "\nu = ";
-              print(tout, v_i) << "\nv = "; print(tout, v_j) <<"\n";
+              print_vert(tout, v_i) << "\nv = "; print_vert(tout, v_j) <<"\n";
               );
         
-        vector<edge> path;
-        find_path_on_tree(path, v_i, v_j);
+        vector<edge> path = connect_u_v_in_tree(v_i, v_j);
         lp::explanation exp = get_explanation_from_path(path);
         add_eq_on_columns(exp, v_i->column(), v_j->column());
         
     }
 
+    std::ostream& print_expl(std::ostream & out, const explanation& exp) const {
+        for (auto p : exp) {
+            lp().constraints().display(out, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
+        }
+        return out;
+    }
+    
     void add_eq_on_columns(const explanation& exp, lpvar j, lpvar k) {
         SASSERT(j != k);
         unsigned je = lp().column_to_reported_index(j);
@@ -460,10 +466,8 @@ public:
         TRACE("cheap_eq", 
               tout << "reporting eq " << j  << ", " << k << "\n";
               tout << "reported idx " << je << ", " << ke << "\n";
-              for (auto p : exp) {
-                  lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
-              }
-              tout << "theory_vars  v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";
+              print_expl(tout, exp);
+              tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";
               );
         
         m_imp.add_eq(je, ke, exp);
@@ -492,14 +496,17 @@ public:
     }
 
     void explain_fixed_in_row(unsigned row, explanation& ex) const {
-        TRACE("cheap_eq", tout << "explain-row " << row << "\n";);
-        for (const auto & c : lp().get_row(row)) 
-            if (lp().is_fixed(c.var())) 
+                TRACE("cheap_eq",
+        tout << lp().get_row(row) << std::endl;
+              );
+        for (const auto & c : lp().get_row(row)) {
+            if (lp().is_fixed(c.var())) {
                 explain_fixed_column(c.var(), ex);
+            }
+        }
     }
 
     void explain_fixed_column(unsigned j, explanation & ex) const {
-        TRACE("cheap_eq", tout << "explain-column " << j << "\n";);
         SASSERT(column_is_fixed(j));
         constraint_index lc, uc;            
         lp().get_bound_constraint_witnesses_for_column(j, lc, uc);
@@ -507,8 +514,9 @@ public:
         ex.push_back(uc);        
     }
     
-    void find_path_on_tree(vector<edge> & path, const vertex* u, const vertex* v) const {
-        TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = ";print(tout, v) << "\n";); 
+    vector<edge> connect_u_v_in_tree(const vertex* u, const vertex* v) const {
+        vector<edge> path;
+        TRACE("cheap_eq_details", tout << "u = " ; print_vert(tout, u); tout << "\nv = ";print_vert(tout, v) << "\n";); 
         vector<edge> v_branch;
         // equalize the levels
         while (u->level() > v->level()) {
@@ -521,18 +529,18 @@ public:
             v = v->parent();
         }
         SASSERT(u->level() == v->level());
-        TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = "; print(tout, v) << "\n";); 
+        TRACE("cheap_eq_details", tout << "u = " ; print_vert(tout, u); tout << "\nv = "; print_vert(tout, v) << "\n";); 
         while (u != v) {
             path.push_back(u->edge_from_parent().reverse());
             v_branch.push_back(v->edge_from_parent());
             u = u->parent();
             v = v->parent();
         }
-        
         for (unsigned i = v_branch.size(); i--; ) {
            path.push_back(v_branch[i]);
         }
         TRACE("cheap_eq", print_path(path, tout););
+        return path;
     }
     
     bool tree_is_correct() const {
@@ -553,11 +561,11 @@ public:
         return true;
     }
     std::ostream& print_tree(std::ostream & out, vertex* v) const {
-        print(out, v);
+        print_vert(out, v);
         out << "\nchildren :\n";
         for (auto c : v->edges()) {
             out << "row = ";
-            print_row(out << c.row() << ": ", c.row());
+            print_row(out, c.row());
             print_tree(out, c.target());
         }
         return out;
@@ -625,7 +633,7 @@ public:
     }
     
     void set_fixed_vertex(vertex *v) {        
-        TRACE("cheap_eq", if (v) print(tout, v); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";);
+        TRACE("cheap_eq", if (v) print_vert(tout, v); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";);
         SASSERT(!m_fixed_vertex || v == nullptr);
         m_fixed_vertex = v;
     }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ec66cdcfd..a417c413e 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3052,7 +3052,7 @@ public:
         scoped_trace_stream _sts(th, fn);
 
        
-        // SASSERT(validate_eq(x, y));
+        SASSERT(validate_eq(x, y));
         ctx().assign_eq(x, y, eq_justification(js));
     }