diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 8a4fc3707..bf69ceb2b 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -477,9 +477,17 @@ namespace lp {
         }
         return false;
     }
-
-    bool lar_solver::remove_from_basis(unsigned j) {
-        return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j);
+// returns true iff the row of j has a non-fixed column different from j
+    bool lar_solver::remove_from_basis(unsigned j) {    
+        lp_assert(is_base(j));
+        unsigned i = row_of_basic_column(j);
+        for (const auto & c : A_r().m_rows[i]) {
+            if (j != c.var() && !is_fixed(c.var())) {
+                return m_mpq_lar_core_solver.m_r_solver.remove_from_basis_core(c.var(), j);
+            }
+            
+        }
+        return false;
     }
 
     lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const {
@@ -621,6 +629,54 @@ namespace lp {
             m_touched_rows.insert(rid);
     }
 
+    void lar_solver::remove_fixed_vars_from_base() {
+	   // this will allow to disable and restore the tracking of the touched rows
+        flet<indexed_uint_set*> f(m_mpq_lar_core_solver.m_r_solver.m_touched_rows, nullptr);
+        unsigned num = A_r().column_count();
+        unsigned_vector to_remove;
+        for (unsigned j : m_fixed_base_var_set) {
+            if (j >= num || !is_base(j) || !is_fixed(j)) {
+                to_remove.push_back(j);
+                continue;
+            }
+
+            lp_assert(is_base(j) && is_fixed(j));
+            auto const& r = basic2row(j);
+            for (auto const& c : r) {
+                unsigned j_entering = c.var();
+                if (!is_fixed(j_entering)) {
+                    pivot(j_entering, j);
+                    to_remove.push_back(j);
+                    lp_assert(is_base(j_entering));
+                    break;
+                }
+            }
+        }
+        for (unsigned j : to_remove) {
+            m_fixed_base_var_set.remove(j);
+        }
+        lp_assert(fixed_base_removed_correctly());
+    }
+#ifdef Z3DEBUG    
+    bool lar_solver::fixed_base_removed_correctly() const {
+        for (unsigned i = 0; i < A_r().row_count(); i++) {
+            unsigned j = get_base_column_in_row(i);
+            if (column_is_fixed(j)) {
+                for (const auto & c : A_r().m_rows[i] ) {
+                    if (!column_is_fixed(c.var())) {
+                        TRACE("lar_solver", print_row(A_r().m_rows[i], tout) << "\n";
+                        for(const auto & c : A_r().m_rows[i]) {
+                            print_column_info(c.var(), tout) << "\n";
+                        });
+                        return false;
+                    }
+                }                
+            }
+        }
+        return true;
+    }
+#endif
+
     bool lar_solver::use_tableau_costs() const {
         return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
     }
@@ -1726,6 +1782,10 @@ namespace lp {
             update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
         else
             update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
+         if (is_base(j) && column_is_fixed(j)) {
+            m_fixed_base_var_set.insert(j);
+         }
+            
         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;);    
     }
     void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 54abba579..a4a0e87b0 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -107,6 +107,8 @@ class lar_solver : public column_namer {
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_fixed_var_table_int;
     // maps values to non-integral fixed vars
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_fixed_var_table_real;
+    // the set of fixed variables which are also base variables
+    indexed_uint_set                                   m_fixed_base_var_set;
     // end of fields
 
     ////////////////// methods ////////////////////////////////
@@ -316,11 +318,14 @@ class lar_solver : public column_namer {
 
     void set_value_for_nbasic_column(unsigned j, const impq& new_val);
 
+    void remove_fixed_vars_from_base();
+
     inline unsigned get_base_column_in_row(unsigned row_index) const {
         return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index);
     }
-
-    // lp_assert(implied_bound_is_correctly_explained(ib, explanation)); }
+#ifdef Z3DEBUG
+    bool fixed_base_removed_correctly() const;
+#endif
     constraint_index mk_var_bound(var_index j, lconstraint_kind kind, const mpq& right_side);
     void activate_check_on_equal(constraint_index, var_index&);
     void activate(constraint_index);
@@ -328,26 +333,23 @@ class lar_solver : public column_namer {
     void add_column_rows_to_touched_rows(lpvar j);
     template <typename T>
     void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) {
-        unsigned num_prop = 0;
-        for (unsigned i : m_touched_rows) {
-            num_prop += calculate_implied_bounds_for_row(i, bp);
-            if (settings().get_cancel_flag())
-                return;
-        }
-        // these two loops should be run sequentially
-        // since the first loop might change column bounds
-        // and add fixed columns this way
+        remove_fixed_vars_from_base();
         if (settings().propagate_eqs()) {
             bp.clear_for_eq();
             for (unsigned i : m_touched_rows) {
                 unsigned offset_eqs = stats().m_offset_eqs;
-                bp.cheap_eq_tree(i);
+                bp.cheap_eq_on_nbase(i);
                 if (settings().get_cancel_flag())
                     return;
                 if (stats().m_offset_eqs > offset_eqs)
                     m_row_bounds_to_replay.push_back(i);
             }
         }
+        for (unsigned i : m_touched_rows) {
+            calculate_implied_bounds_for_row(i, bp);
+            if (settings().get_cancel_flag())
+                return;
+        }
         m_touched_rows.reset();
     }
 
@@ -424,9 +426,10 @@ class lar_solver : public column_namer {
     bool try_to_patch(lpvar j, const mpq& val,
                       const Blocker& is_blocked,
                       const ChangeReport& change_report) {
-        if (is_base(j)) {
+        if (is_base(j))  {
             TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
-            remove_from_basis(j);
+            if (!remove_from_basis(j))
+               return false;
         }
 
         impq ival(val);
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 6056444e8..e2c0d6c92 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -12,104 +12,7 @@
 namespace lp {
 template <typename T>
 class lp_bound_propagator {
-    class edge;  // forward definition
-    // vertex represents a column
-    // The set of vertices is organized in a tree.
-    // The edges of the tree are rows,
-    // Vertices with m_neg set to false grow with the same rate as the root.
-    // Vertices with m_neq set to true diminish with the same rate as the roow grows.
-    // When two vertices with the same m_neg have the same value of columns
-    // then we have an equality between the columns.
-    class vertex {
-        unsigned m_column;
-        vector<edge> m_edges;
-        edge m_edge_from_parent;
-        unsigned m_level;  // the distance in hops to the root;
-                           // it is handy to find the common ancestor
-       public:
-        vertex() {}
-        vertex(unsigned column) : m_column(column),
-                                  m_level(0) {}
-        unsigned column() const { return m_column; }
-        const vertex* parent() const { return m_edge_from_parent.source(); }
-        vertex* parent() { return m_edge_from_parent.source(); }
-        unsigned level() const { return m_level; }
-        void set_edge_from_parent(edge& e) { m_edge_from_parent = e; }
-        const edge& edge_from_parent() const { return m_edge_from_parent; }
-
-        void add_child(int row, vertex* child) {
-            SASSERT(*this != *child);
-            SASSERT(child->parent() == nullptr);
-            edge e = edge(this, child, row);
-            m_edges.push_back(e);
-            child->set_edge_from_parent(e);
-            child->m_level = m_level + 1;
-        }
-        const vector<edge>& edges() const { return m_edges; }
-        bool operator==(const vertex& o) const {
-            return m_column == o.m_column;
-        }
-        bool operator!=(const vertex& o) const {
-            return m_column != o.m_column;
-        }
-    };
-
-    class edge {
-        vertex* m_source;
-        vertex* m_target;
-        int m_row;
-
-       public:
-        edge(vertex* source, vertex* target, int row) : m_source(source), m_target(target), m_row(row) {}
-        edge() : m_source(nullptr), m_target(nullptr), m_row(-1) {}
-        const vertex* source() const { return m_source; }
-        vertex* source() { return m_source; }
-        const vertex* target() const { return m_target; }
-        vertex* target() { return m_target; }
-        int row() const { return m_row; }
-        edge reverse() const { return edge(m_target, m_source, m_row); }
-    };
-
-    static int other(int x, int y, int z) {
-        SASSERT(x == z || y == z);
-        return x == z ? y : x;
-    }
-    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 (m_pol.contains(v->column()))
-            out << (pol(v) == -1 ? " -" : " +");
-        else
-            out << " not in m_pol";
-        out << ')';
-        return out;
-    }
-
-    hashtable<unsigned, u_hash, u_eq> m_visited_rows;
-    hashtable<unsigned, u_hash, u_eq> m_visited_columns;
-    u_map<vertex*> m_vertices;
-    vertex* m_root = nullptr;
-    // At some point we can find a row with a single vertex non fixed vertex
-    // then we can fix the whole tree,
-    // by adjusting the vertices offsets, so they become absolute.
-    // If the tree is fixed then in addition to checking with the m_vals_to_verts
-    // we are going to check with the m_fixed_var_tables.
-    const vertex* m_fixed_vertex = nullptr;
-    explanation m_fixed_vertex_explanation;
-    // a pair (o, j) belongs to m_vals_to_verts iff x[j] = x[m_root->column()] + o
-    map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts;
-    // a pair (o, j) belongs to m_vals_to_verts_neg iff -x[j] = x[m_root->column()] + o
-    map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts_neg;
-    // x[m_root->column()] - m_pol[j].pol()*x[j] == const;
-    // to bind polarity and the vertex in the table
-    u_map<int> m_pol;
-    // if m_pos.contains(j) then  x[j] = x[m_root->column()] + o
-    uint_set m_pos;
-
+	uint_set m_visited_rows;
     // these maps map a column index to the corresponding index in ibounds
     std::unordered_map<unsigned, unsigned> m_improved_lower_bounds;
     std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
@@ -118,12 +21,14 @@ class lp_bound_propagator {
     vector<implied_bound> m_ibounds;
 
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
-
-    bool is_fixed_row(unsigned r, unsigned& x) {
+    // works for rows of the form x + y + sum of fixed = 0
+    map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_pos;
+    // works for rows of the form x - y + sum of fixed = 0    
+    map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_neg;
+    // returns true iff there is only one non-fixed column in the row
+    bool only_one_nfixed(unsigned r, unsigned& x) {
         x = UINT_MAX;
-        const auto& row = lp().get_row(r);
-        for (unsigned k = 0; k < row.size(); k++) {
-            const auto& c = row[k];
+        for (const auto& c: lp().get_row(r)) {
             if (column_is_fixed(c.var()))
                 continue;
             if (x != UINT_MAX)
@@ -134,22 +39,27 @@ class lp_bound_propagator {
     }
 
     void try_add_equation_with_internal_fixed_tables(unsigned r1) {
-        SASSERT(m_fixed_vertex);
         unsigned v1, v2;
-        if (!is_fixed_row(r1, v1))
+        if (!only_one_nfixed(r1, v1))
             return;
         unsigned r2 = UINT_MAX;
         if (!m_val2fixed_row.find(val(v1), r2) || r2 >= lp().row_count()) {
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
-        if (!is_fixed_row(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) {
+        if (!only_one_nfixed(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) {
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
         if (v1 == v2)
             return;
-
+#if Z3DEBUG
+        lp_assert(val(v1) == val(v2));
+        unsigned debv1, debv2;
+        lp_assert(only_one_nfixed(r1, debv1) && only_one_nfixed(r2, debv2));
+        lp_assert(debv1 == v1 && debv2 == v2);
+        lp_assert(ival(v1).y == ival(v2).y);
+#endif
         explanation ex;
         explain_fixed_in_row(r1, ex);
         explain_fixed_in_row(r2, ex);
@@ -157,141 +67,12 @@ class lp_bound_propagator {
         add_eq_on_columns(ex, v1, v2, true);
     }
 
-    void try_add_equation_with_lp_fixed_tables(unsigned row_index, const vertex* v) {
-        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)) {
-            try_add_equation_with_internal_fixed_tables(row_index);
-            return;
-        }
-
-        TRACE("cheap_eq",
-              tout << "v_j = ";
-              lp().print_column_info(v_j, tout) << std::endl;
-              tout << "v = "; print_vert(tout, v) << std::endl;
-              tout << "found j " << j << std::endl; lp().print_column_info(j, tout) << std::endl;
-              tout << "found j = " << j << std::endl;);
-        vector<edge> path = connect_in_tree(v, m_fixed_vertex);
-        explanation ex = get_explanation_from_path(path);
-        ex.add_expl(m_fixed_vertex_explanation);
-        explain_fixed_column(j, ex);
-        add_eq_on_columns(ex, j, v_j, true);
-    }
-
-    void try_add_equation_with_val_table(const vertex* v) {
-        SASSERT(m_fixed_vertex);
-        unsigned v_j = v->column();
-        const vertex* u = nullptr;
-        if (!m_vals_to_verts.find(val(v_j), u)) {
-            m_vals_to_verts.insert(val(v_j), v);
-            return;
-        }
-        unsigned j = u->column();
-        if (j == v_j || is_int(j) != is_int(v_j))
-            return;
-
-        TRACE("cheap_eq", tout << "found j=" << j << " for v=";
-              print_vert(tout, v) << "\n in m_vals_to_verts\n";);
-        vector<edge> path = connect_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, true);
-    }
-
-    static bool not_set(unsigned j) { return j == UINT_MAX; }
+    static bool is_not_set(unsigned j) { return j == UINT_MAX; }
     static bool is_set(unsigned j) { return j != UINT_MAX; }
 
-    void create_root(unsigned row_index) {
-        SASSERT(!m_root && !m_fixed_vertex);
-        unsigned x, y;
-        int polarity;
-        TRACE("cheap_eq_det", print_row(tout, row_index););
-        if (!is_tree_offset_row(row_index, x, y, polarity)) {
-            TRACE("cheap_eq_det", tout << "not an offset row\n";);
-            return;
-        }
-        TRACE("cheap_eq", print_row(tout, row_index););
-        m_root = alloc_v(x);
-        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);
-        } else {
-            vertex* v = add_child_with_check(row_index, y, m_root, polarity);
-            if (v)
-                explore_under(v);
-        }
-        explore_under(m_root);
-    }
-
-    void explore_under(vertex* v) {
-        check_for_eq_and_add_to_val_tables(v);
-        go_over_vertex_column(v);
-    }
-
-    // In case of only one non fixed column, and the function returns true,
-    // this column would be represened by x.
-    bool is_tree_offset_row(unsigned row_index, unsigned& x, unsigned& y, int& polarity) const {
-        x = y = UINT_MAX;
-        const row_cell<mpq>* x_cell = nullptr;
-        const row_cell<mpq>* y_cell = nullptr;
-        const auto& row = lp().get_row(row_index);
-        for (unsigned k = 0; k < row.size(); k++) {
-            const auto& c = row[k];
-            if (column_is_fixed(c.var()))
-                continue;
-            if (not_set(x)) {
-                if (c.coeff().is_one() || c.coeff().is_minus_one()) {
-                    x = c.var();
-                    x_cell = &c;
-                } else
-                    return false;
-            } else if (not_set(y)) {
-                if (c.coeff().is_one() || c.coeff().is_minus_one()) {
-                    y = c.var();
-                    y_cell = &c;
-                } else
-                    return false;
-            } else
-                return false;
-        }
-        if (is_set(x)) {
-            if (is_set(y))
-                polarity = x_cell->coeff().is_pos() == y_cell->coeff().is_pos() ? -1 : 1;
-            else
-                polarity = 1;
-            return true;
-        }
-        return false;
-    }
-
-    void go_over_vertex_column(vertex* v) {
-        lpvar j = v->column();
-        if (!check_insert(m_visited_columns, j))
-            return;
-
-        for (const auto& c : lp().get_column(j)) {
-            unsigned row_index = c.var();
-            if (!check_insert(m_visited_rows, row_index))
-                continue;
-            vertex* u = get_child_from_row(row_index, v);
-            if (u)
-                explore_under(u);
-        }
-    }
-
     void reset_cheap_eq_eh() {
-        if (!m_root)
-            return;
-        delete_tree(m_root);
-        m_root = nullptr;
-        set_fixed_vertex(nullptr);
-        m_fixed_vertex_explanation.clear();
-        m_vals_to_verts.reset();
-        m_vals_to_verts_neg.reset();
-        m_pol.reset();
-        m_vertices.reset();
+        m_row2index_pos.reset();           
+        m_row2index_neg.reset();
     }
 
     struct reset_cheap_eq {
@@ -381,175 +162,24 @@ class lp_bound_propagator {
     }
 
     const mpq& val(unsigned j) const {
-        return lp().get_column_value(j).x;
+        return lp().get_column_value(j).x; // figure out why it is safe to return .x
     }
-
-    const mpq& val(const vertex* v) const {
-        return val(v->column());
-    }
-
-    bool tree_contains_r(vertex* root, vertex* v) const {
-        if (*root == *v)
-            return true;
-        for (auto e : root->edges())
-            if (tree_contains_r(e.target(), v))
-                return true;
-        return false;
-    }
-
-    // pol for polarity
-    int pol(const vertex* v) const { return pol(v->column()); }
-    int pol(unsigned j) const { return m_pol[j]; }
-    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, p);
-    }
-
-    void check_and_set_polarity(vertex* v, int polarity, unsigned row_index, vertex* v_parent) {
-        int prev_pol;
-        if (!m_pol.find(v->column(), prev_pol)) {
-            set_polarity(v, polarity);
-            return;
-        }
-        if (prev_pol == polarity)
-            return;
-        // we have a path L between v and parent 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 = connect_in_tree(v, v_parent);
-        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: " << polarity << "\nv = ";
-              print_vert(tout, v) << "\nu = "; 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()););
-    }
-
-    bool tree_contains(vertex* v) const {
-        if (!m_root)
-            return false;
-        return tree_contains_r(m_root, v);
-    }
-
-    vertex* alloc_v(unsigned column) {
-        vertex* v = alloc(vertex, column);
-        m_vertices.insert(column, v);
-        SASSERT(!tree_contains(v));
-        return v;
+    
+    const impq& ival(unsigned j) const {
+        return lp().get_column_value(j); // figure out why it is safe to return .x
     }
 
     unsigned column(unsigned row, unsigned index) {
         return lp().get_row(row)[index].var();
     }
 
-    bool fixed_phase() const { return m_fixed_vertex; }
-
-    // Returns the vertex to start exploration from, or nullptr.
-    // It is assumed that parent->column() is present in the row
-    vertex* get_child_from_row(unsigned row_index, vertex* parent) {
-        TRACE("cheap_eq_det", print_row(tout, row_index););
-        unsigned x, y;
-        int row_polarity;
-        if (!is_tree_offset_row(row_index, x, y, row_polarity)) {
-            TRACE("cheap_eq_det", tout << "not an offset row\n";);
-            return nullptr;
-        }
-        if (not_set(y)) {  // there is only one fixed variable in the row
-            if (!fixed_phase()) {
-                set_fixed_vertex(parent);
-                explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
-            }
-            return nullptr;
-        }
-
-        SASSERT(is_set(x) && is_set(y));
-        unsigned col = other(x, y, parent->column());
-        return add_child_with_check(row_index, col, parent, row_polarity);
-    }
-
-    vertex* add_child_with_check(unsigned row_index, unsigned col, vertex* parent, int row_polarity) {
-        vertex* vy;
-        if (m_vertices.find(col, vy)) {
-            SASSERT(vy != nullptr);
-            if (!fixed_phase()) {
-                check_and_set_polarity(vy, pol(parent) * row_polarity, row_index, parent);
-            }
-            return nullptr;  // it is not a new vertex
-        }
-        vy = alloc_v(col);
-        parent->add_child(row_index, vy);
-        if (!fixed_phase())
-            check_and_set_polarity(vy, row_polarity * pol(parent), row_index, parent);
-        return vy;
-    }
 
     bool is_equal(lpvar j, lpvar k) const {
         return m_imp.is_equal(col_to_imp(j), col_to_imp(k));
     }
 
-    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_vert(tout, v) << "\n";);
-        const vertex* k;  // the other vertex
-        if (table.find(val(v), k)) {
-            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())) {
-                report_eq(k, v);
-            } else {
-                TRACE("cheap_eq", tout << "no report\n";);
-            }
-        } else {
-            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_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);
-            else
-                check_for_eq_and_add_to_val_table(v, m_vals_to_verts);
-        }
-    }
-
     void clear_for_eq() {
         m_visited_rows.reset();
-        m_visited_columns.reset();
-        m_root = nullptr;
-    }
-
-    std::ostream& print_edge(const edge& e, std::ostream& out) const {
-        out << e.source()->column() << "->" << e.target()->column() << "\n";
-        return print_row(out, e.row());
-    }
-
-    std::ostream& print_path(const vector<edge>& path, std::ostream& out) const {
-        out << "path = \n";
-        for (const edge& k : path)
-            print_edge(k, out) << "\n";
-        return out;
-    }
-
-    // we have v_i and v_j, indices of vertices at the same offsets
-    void report_eq(const vertex* v_i, const vertex* v_j) {
-        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_vert(tout, v_i) << "\nv = "; print_vert(tout, v_j) << "\n");
-
-        vector<edge> path = connect_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(), false);
     }
 
     std::ostream& print_expl(std::ostream& out, const explanation& exp) const {
@@ -560,10 +190,12 @@ class lp_bound_propagator {
     }
 
     bool add_eq_on_columns(const explanation& exp, lpvar j, lpvar k, bool is_fixed) {
-        SASSERT(j != k);
+        lp_assert(j != k && is_int(j) == is_int(k));
+        lp_assert(ival(j) == ival(k));
+
         unsigned je = lp().column_to_reported_index(j);
         unsigned ke = lp().column_to_reported_index(k);
-        TRACE("cheap_eq",
+        TRACE("eq",
               tout << "reporting eq " << j << ", " << k << "\n";
               tout << "reported idx " << je << ", " << ke << "\n";
               print_expl(tout, exp);
@@ -593,20 +225,26 @@ class lp_bound_propagator {
         return lp().column_is_int(j);
     }
 
-    explanation get_explanation_from_path(vector<edge>& path) const {
-        explanation ex;
-        for (edge& e : path)
-            explain_fixed_in_row(e.row(), ex);
-        return ex;
-    }
-
     void explain_fixed_in_row(unsigned row, explanation& ex) const {
-        TRACE("cheap_eq", tout << lp().get_row(row) << std::endl);
+        TRACE("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);
     }
 
+    unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) const {
+        unsigned base = UINT_MAX;
+        TRACE("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);
+            } else if (lp().is_base(c.var())) {
+                base = c.var();
+            }
+        }
+        return base;
+    }
+
     void explain_fixed_column(unsigned j, explanation& ex) const {
         SASSERT(column_is_fixed(j));
         constraint_index lc, uc;
@@ -615,101 +253,156 @@ class lp_bound_propagator {
         if (lc != uc)
             ex.push_back(uc);
     }
-
-    vector<edge> connect_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()) {
-            path.push_back(u->edge_from_parent().reverse());
-            u = u->parent();
-        }
-
-        while (u->level() < v->level()) {
-            v_branch.push_back(v->edge_from_parent());
-            v = v->parent();
-        }
-        SASSERT(u->level() == v->level());
-        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 {
-        std::unordered_set<int> vs;
-        return tree_is_correct(m_root, vs);
-    }
-
-    bool tree_is_correct(vertex* v, std::unordered_set<int>& visited_verts) const {
-        if (fixed_phase())
-            return true;
-        if (visited_verts.find(v->column()) != visited_verts.end())
-            return false;
-        visited_verts.insert(v->column());
-        for (auto e : v->edges())
-            if (!tree_is_correct(e.target(), visited_verts))
+#ifdef Z3DEBUG
+    bool all_fixed_in_row(unsigned row) const {
+        for (const auto& c : lp().get_row(row))
+            if (!lp().is_fixed(c.var()))
                 return false;
         return true;
     }
-    std::ostream& print_tree(std::ostream& out, vertex* v) const {
-        print_vert(out, v);
-        out << "\nchildren :\n";
-        for (auto c : v->edges()) {
-            out << "row = ";
-            print_row(out, c.row());
-            print_tree(out, c.target());
+
+    // bounded by 2
+    unsigned num_of_non_fixed_in_row(unsigned row_index) const {
+        unsigned n_of_nfixed = 0;
+        for (const auto& c : lp().get_row(row_index)) {
+            if (lp().column_is_fixed(c.var()))
+                continue;
+            n_of_nfixed++;
+            if (n_of_nfixed > 1)
+                return n_of_nfixed;
         }
-        return out;
+            
+        return n_of_nfixed;
+    }   
+#endif
+    // Let nf is the number of non-fixed columns in the row.
+    // Then the function returns min(nf, 3).
+    // if nf == 0, the row is of the form sum of fixed = 0
+    // if nf == 1, the row is of the form x + sum of fixed = 0, where x is not fixed base
+    // if nf == 2, the row is of the form x + ay + sum of fixed = 0, x is a non fixed base and y is not fixed 
+    // y_sign is set to a, if abs(a)= 1, and 0 otherwise
+
+    unsigned extract_non_fixed(unsigned row_index, unsigned& x, unsigned& y, int& y_sign) const {
+        unsigned nf = 0;  // number of non-fixed columns
+        y = UINT_MAX;
+        const auto& row = lp().get_row(row_index);
+        x = lp().get_base_column_in_row(row_index);
+        if (!column_is_fixed(x)) {
+            nf++;
+        } else {
+            lp_assert(all_fixed_in_row(row_index));
+            return 0;
+        }
+
+        for (const auto& c : row) {
+            unsigned j = c.var();
+            if (j == x) continue;
+            if (column_is_fixed(j))
+                continue;
+            if (++nf > 2)
+                return nf;
+            lp_assert(is_not_set(y));
+            y = j;
+            if (c.coeff().is_one()) {
+                y_sign = 1;
+            } else if (c.coeff().is_minus_one()) {
+                y_sign = -1;
+            } else {
+                // y has a coefficient other than 1 or -1
+                y_sign = 0;
+                return nf; // maybe be too low but we don't care
+            }
+        }
+
+        return nf;
     }
 
-    void try_add_equation_with_fixed_tables(unsigned row_index, const vertex* v) {
-        try_add_equation_with_lp_fixed_tables(row_index, v);
-        try_add_equation_with_val_table(v);
-    }
-
-    void handle_fixed_phase(unsigned row_index) {
-        if (!fixed_phase())
+    void try_add_equation_with_lp_fixed_tables(unsigned row_index, unsigned v_j) {
+        lp_assert(lp().get_base_column_in_row(row_index) == v_j);
+        lp_assert(num_of_non_fixed_in_row(row_index) == 1 || column_is_fixed(v_j));
+        if (column_is_fixed(v_j)) {
             return;
-        const vertex* v = m_root;
-        try_add_equation_with_fixed_tables(row_index, v);
-        for (auto e : v->edges())
-            try_add_equation_with_fixed_tables(row_index, e.target());
+        }
+        unsigned j = null_lpvar;
+        if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
+            try_add_equation_with_internal_fixed_tables(row_index);
+            return;
+        } 
+        TRACE("eq",
+              tout << "v_j = ";
+              lp().print_column_info(v_j, tout) << std::endl;
+              tout << "found j " << j << std::endl; lp().print_column_info(j, tout) << std::endl;
+              print_row(tout, row_index) << std::endl;
+              );
+        explanation ex;  
+        explain_fixed_in_row(row_index, ex);
+        explain_fixed_column(j, ex);
+        add_eq_on_columns(ex, j, v_j, true);
     }
 
-    void cheap_eq_tree(unsigned row_index) {
+    void cheap_eq_on_nbase(unsigned row_index) {
         reset_cheap_eq _reset(*this);
-        TRACE("cheap_eq_det", tout << "row_index = " << row_index << "\n";);
+        TRACE("eq", tout << "row_index = " << row_index << "\n";
+                    print_row(tout, row_index) << "\n";);
         if (!check_insert(m_visited_rows, row_index))
             return;
-        create_root(row_index);
-        if (!m_root)
+        unsigned x, y;
+        int y_sign;
+        unsigned nf = extract_non_fixed(row_index, x, y, y_sign);
+        if (nf == 0 || nf > 2)
             return;
+        if (nf == 1) {
+            lp_assert(is_not_set(y));
+            try_add_equation_with_lp_fixed_tables(row_index, x);
+            return;
+        }
+        if (y_sign == 0) {
+            // the coefficient before y is not 1 or -1
+            return;
+        }
+        lp_assert(y_sign == -1 || y_sign == 1);
+        lp_assert(lp().is_base(y) == false);
+        auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg;
+        table.insert(val(x), row_index);        
+        TRACE("eq", tout << "y = " << y << "\n";);    
 
-        TRACE("cheap_eq", tout << "tree = "; print_tree(tout, m_root) << "\n";);
-        SASSERT(tree_is_correct());
-        handle_fixed_phase(row_index);
+        for (const column_cell& c : lp().get_column(y)) {
+            unsigned i = c.var();  // the running index of the row
+            if (i == row_index)
+                continue;
+            if (check_insert(m_visited_rows, i) == false)
+                continue;
+            unsigned y_nb;
+            nf = extract_non_fixed(i, x, y_nb, y_sign);
+            if (nf != 2 || y_sign == 0)
+                continue;
 
-        TRACE("cheap_eq",
-              tout << "done for row_index " << row_index << "\n";
-              tout << "tree size = " << verts_size(););
+            lp_assert(y_nb == y);
+            lp_assert(y_sign == 1 || y_sign == -1);
+            auto& table = y_sign == 1 ? m_row2index_pos : m_row2index_neg;
+            const auto& v = val(x);
+            unsigned found_i;
+            if (!table.find(v, found_i)) {
+                table.insert(v, i);
+            } else {
+                explanation ex;
+                unsigned base_of_found = lp().get_base_column_in_row(found_i);
+                if (is_int(x) != is_int(base_of_found) || ival(x).y != ival(base_of_found).y)
+                    continue;
+                explain_fixed_in_row(found_i, ex);
+                explain_fixed_in_row(i, ex);
+                TRACE("eq", {
+                    print_row(tout, i);
+                    print_row(tout, found_i) << "\n";
+                    lp().print_column_info(base_of_found, tout);
+                    lp().print_column_info(x, tout) << "\n";
+                });
+                add_eq_on_columns(ex, x, base_of_found, false);
+            }
+        }
     }
 
     std::ostream& print_row(std::ostream& out, unsigned row_index) const {
-        unsigned x, y;
-        int polarity;
-        if (true || !is_tree_offset_row(row_index, x, y, polarity))
-            return lp().get_int_solver()->display_row_info(out, row_index);
-
         bool first = true;
         for (const auto& c : lp().A_r().m_rows[row_index]) {
             if (lp().column_is_fixed(c.var()))
@@ -726,29 +419,6 @@ class lp_bound_propagator {
         return out;
     }
 
-    void set_fixed_vertex(vertex* v) {
-        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;
-    }
-
-    unsigned verts_size() const {
-        return subtree_size(m_root);
-    }
-
-    unsigned subtree_size(vertex* v) const {
-        unsigned r = 1;  // 1 for v
-        for (auto e : v->edges())
-            r += subtree_size(e.target());
-        return r;
-    }
-
-    void delete_tree(vertex* v) {
-        for (auto p : v->edges())
-            delete_tree(p.target());
-        dealloc(v);
-    }
-
     template <typename C>
     bool check_insert(C& table, unsigned j) {
         if (table.contains(j))
diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp
index 28f92d8e2..b14231d09 100644
--- a/src/math/lp/lp_core_solver_base.cpp
+++ b/src/math/lp/lp_core_solver_base.cpp
@@ -65,6 +65,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivot_column_tableau(un
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_rows_tableau(unsigned int, unsigned int);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::inf_heap_is_correct() const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::inf_heap_is_correct() const;
-template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int);
+template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis_core(unsigned int, unsigned int);
 
 
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index 251199419..e7570d5dd 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -338,7 +338,7 @@ public:
         
     }
 
-    bool remove_from_basis(unsigned j);
+    bool remove_from_basis_core(unsigned entering, unsigned leaving);
     bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w);
     void init_basic_part_of_basis_heading() {
         unsigned m = m_basis.size();
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 101f9dbea..613862dde 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -403,30 +403,24 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::transpose_row
     transpose_basis(i, j);
     m_A.transpose_rows(i, j);
 }
-    
-// j is the new basic column, j_basic - the leaving column
-template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) {
-    lp_assert(m_basis_heading[j] < 0);
-    lp_assert(m_basis_heading[j_basic] >= 0);
-    unsigned row_index = m_basis_heading[j_basic];
-    // the tableau case
-    if (!pivot_column_tableau(j, row_index))
+// entering is the new base column, leaving - the column leaving the basis
+template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned entering, unsigned leaving, indexed_vector<T> & w) {
+	lp_assert(m_basis_heading[entering] < 0);
+	lp_assert(m_basis_heading[leaving] >= 0);
+	unsigned row_index = m_basis_heading[leaving];
+	  // the tableau case
+	if (pivot_column_tableau(entering, row_index))
+		change_basis(entering, leaving);
+	else 
         return false;
-    change_basis(j, j_basic);
-    return true;
+	
+	return true;
 }
 
 
-template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_basis(unsigned basic_j) {
+template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_basis_core(unsigned entering, unsigned leaving) {
     indexed_vector<T> w(m_basis.size()); // the buffer
-    unsigned i = m_basis_heading[basic_j];
-    for (auto &c : m_A.m_rows[i]) {
-        if (c.var() == basic_j)
-            continue;
-        if (pivot_column_general(c.var(), basic_j, w))
-            return true;
-    }
-    return false;
+    return pivot_column_general(entering, leaving, w);
 }