diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index a1d86e6f3..409dda96d 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -55,6 +55,17 @@ public :
         m_rs(rs)
     {}
 
+    static void analyze_row(const C & row,
+                            unsigned bj, // basis column for the row
+                            const numeric_pair<mpq>& rs,
+                            unsigned row_or_term_index,
+                            lp_bound_propagator & bp) {
+        bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
+        a.analyze();
+        // TBD: a.analyze_eq();
+    }
+
+private:
 
     void analyze() {
         for (const auto & c : m_row) {
@@ -73,6 +84,37 @@ public :
             limit_all_monoids_from_above();
     }
 
+
+    void analyze_eq() {
+        lpvar x = null_lpvar, y = null_lpvar;
+        for (const auto & c : m_row) {
+            if (m_bp.get_column_type(c.var()) == column_type::fixed)
+                continue;
+            if (x == null_lpvar && c.coeff().is_one())
+                x = c.var();
+            else if (y == null_lpvar && c.coeff().is_minus_one())
+                y = c.var();
+            else 
+                return;
+        }        
+        if (x == null_lpvar || y == null_lpvar)
+            return;
+        impq value;
+        for (const auto & c : m_row) {
+            if (m_bp.get_column_type(c.var()) == column_type::fixed)
+                value += c.coeff() * lb(c.var());
+        }
+        if (!value.is_zero()) {
+            // insert / check offset table to infer equalities
+            // of the form y = z from offset table collision:
+            // value = (x - y)
+            // value = (x - z)
+        } 
+        else {
+            // m_bp.try_add_fixed(x, y, m_row_or_term_index);
+        }
+    }
+
     bool bound_is_available(unsigned j, bool lower_bound) {
         return (lower_bound && lower_bound_is_available(j)) ||
             (!lower_bound && upper_bound_is_available(j));
@@ -319,14 +361,6 @@ public :
         }
     }
 
-    static void analyze_row(const C & row,
-                            unsigned bj, // basis column for the row
-                            const numeric_pair<mpq>& rs,
-                            unsigned row_or_term_index,
-                            lp_bound_propagator & bp) {
-        bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
-        a.analyze();
-    }
 
 };
 }
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
index aff4d8b99..5a46159c4 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -631,7 +631,7 @@ public:
         for (unsigned i = 0; i < m_r_A.row_count(); i++) {
             auto & row = m_r_A.m_rows[i];
             for (row_cell<mpq> & c : row) {
-                A.add_new_element(i, c.var(), c.get_val().get_double());
+                A.add_new_element(i, c.var(), c.coeff().get_double());
             }
         }
     }
diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h
index abd9922ab..77e5177de 100644
--- a/src/math/lp/lar_core_solver_def.h
+++ b/src/math/lp/lar_core_solver_def.h
@@ -227,7 +227,7 @@ void lar_core_solver::fill_not_improvable_zero_sum_from_inf_row() {
     m_infeasible_sum_sign =  m_r_solver.inf_sign_of_column(bj);
     m_infeasible_linear_combination.clear();
     for (auto & rc : m_r_solver.m_A.m_rows[m_r_solver.m_inf_row_index_for_tableau]) {
-        m_infeasible_linear_combination.push_back(std::make_pair( rc.get_val(), rc.var()));
+        m_infeasible_linear_combination.push_back(std::make_pair(rc.coeff(), rc.var()));
     }
 }
 
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 0306261cc..fc0e2be4a 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -141,14 +141,16 @@ void lar_solver::analyze_new_bounds_on_row(
     lp_bound_propagator & bp) {
     lp_assert(!use_tableau());
     unsigned j =  m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row
-    bound_analyzer_on_row<indexed_vector<mpq>>
-        ra_pos(m_mpq_lar_core_solver.get_pivot_row(),
-                                 j,
-                                 zero_of_type<numeric_pair<mpq>>(),
-                                 row_index,
-                                 bp
-                                 );
-    ra_pos.analyze();
+
+    
+    bound_analyzer_on_row<indexed_vector<mpq>>::analyze_row(
+        m_mpq_lar_core_solver.get_pivot_row(),
+        j,
+        zero_of_type<numeric_pair<mpq>>(),
+        row_index,
+        bp
+                                                            );
+//    ra_pos.analyze();
 }
 
 bool lar_solver::row_has_a_big_num(unsigned i) const {
@@ -167,6 +169,7 @@ void lar_solver::analyze_new_bounds_on_row_tableau(
         || row_has_a_big_num(row_index))
         return;
     lp_assert(use_tableau());
+
     bound_analyzer_on_row<row_strip<mpq>>::analyze_row(A_r().m_rows[row_index],
                                        null_ci,
                                        zero_of_type<numeric_pair<mpq>>(),
@@ -227,7 +230,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
     for (auto const& r : A_r().m_rows[i]) {
         unsigned j = r.var();
         if (j == bound_j) continue;
-        mpq const& a = r.get_val();
+        mpq const& a = r.coeff();
         int a_sign = is_pos(a)? 1: -1;
         int sign = j_sign * a_sign;
         const ul_pair & ul =  m_columns_to_ul_pairs[j];
@@ -948,7 +951,7 @@ void lar_solver::copy_from_mpq_matrix(static_matrix<U, V> & matr) {
     matr.m_columns.resize(A_r().column_count());
     for (unsigned i = 0; i < matr.row_count(); i++) {
         for (auto & it : A_r().m_rows[i]) {
-            matr.set(i, it.var(),  convert_struct<U, mpq>::convert(it.get_val()));
+            matr.set(i, it.var(),  convert_struct<U, mpq>::convert(it.coeff()));
         }
     }
 }
@@ -1399,7 +1402,7 @@ void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) {
     for (unsigned k = last_row.size(); k-- > 0;) {
         auto &rc = last_row[k];
         if (cost_is_nz) {
-            m_mpq_lar_core_solver.m_r_solver.m_d[rc.var()] += cost_j*rc.get_val();
+            m_mpq_lar_core_solver.m_r_solver.m_d[rc.var()] += cost_j * rc.coeff();
         }
         A_r().remove_element(last_row, rc);
     }
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index cae9f1ae8..9b67162a9 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -18,6 +18,7 @@ public:
     const impq & get_lower_bound(unsigned) const;
     const impq & get_upper_bound(unsigned) const;
     void try_add_bound(mpq const & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict);
+    void try_add_eq(lpvar x, lpvar y, unsigned row_or_term_index) {} // TBD
     virtual bool bound_is_interesting(unsigned vi,
                                       lp::lconstraint_kind kind,
                                       const rational & bval) {return true;}
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 0880c69c2..46fb0be76 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -95,7 +95,7 @@ pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
         return;
     for (const row_cell<T> & r: m_A.m_rows[i]){
         if (r.var() != j)
-            m_d[r.var()] -= a * r.get_val();
+            m_d[r.var()] -= a * r.coeff();
     }
     a = zero_of_type<T>(); // zero the pivot column's m_d finally
 }
@@ -304,7 +304,7 @@ calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) {
         for (auto & c : m_A.m_rows[i]) {
             unsigned j = c.var();
             if (m_basis_heading[j] < 0) {
-                m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.get_val() * pi_1);
+                m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.coeff() * pi_1);
             }
         }
     }
@@ -444,7 +444,7 @@ rs_minus_Anx(vector<X> & rs) {
         for (auto & it : m_A.m_rows[row]) {
             unsigned j = it.var();
             if (m_basis_heading[j] < 0) {
-                rsv -= m_x[j] * it.get_val();
+                rsv -= m_x[j] * it.coeff();
             }
         }
     }
@@ -630,8 +630,8 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
         column[0]  = column[pivot_col_cell_index];
         column[pivot_col_cell_index] = c;
 
-        m_A.m_rows[piv_row_index][column[0].m_offset].m_offset = 0;
-        m_A.m_rows[c.var()][c.m_offset].m_offset = pivot_col_cell_index;
+        m_A.m_rows[piv_row_index][column[0].offset()].offset() = 0;
+        m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
     }
     while (column.size() > 1) {
         auto & c = column.back();
@@ -761,7 +761,7 @@ fill_reduced_costs_from_m_y_by_rows() {
         for (row_cell<T> & c : m_A.m_rows[i]) {
             j = c.var();
             if (m_basis_heading[j] < 0) {
-                m_d[j] -= y * c.get_val();
+                m_d[j] -= y * c.coeff();
             }
         }
     }
@@ -804,7 +804,7 @@ find_error_in_BxB(vector<X>& rs){
         for (auto & it : m_A.m_rows[row]) {
             unsigned j = it.var();
             if (m_basis_heading[j] >= 0) {
-                rsv -= m_x[j] * it.get_val();
+                rsv -= m_x[j] * it.coeff();
             }
         }
     }
@@ -1046,7 +1046,7 @@ void lp_core_solver_base<T, X>::calculate_pivot_row(unsigned i) {
         unsigned basic_j = m_basis[i];
         for (auto & c : m_A.m_rows[i]) {
             if (c.var() != basic_j)
-                m_pivot_row.set_value(c.get_val(), c.var());
+                m_pivot_row.set_value(c.coeff(), c.var());
         }
         return;
     }
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 806ad1932..3abf9dbc0 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -180,19 +180,19 @@ public:
         case column_type::fixed:
             return false;
         case column_type::lower_bound:
-            if (is_pos(rc.get_val())) {
+            if (is_pos(rc.coeff())) {
                 return this->x_above_lower_bound(j);
             }
 
             return true;
         case column_type::upper_bound:
-            if (is_pos(rc.get_val())) {
+            if (is_pos(rc.coeff())) {
                 return true;
             }
 
             return this->x_below_upper_bound(j);
         case column_type::boxed:
-            if (is_pos(rc.get_val())) {
+            if (is_pos(rc.coeff())) {
                 return this->x_above_lower_bound(j);
             }
 
@@ -213,19 +213,19 @@ public:
         case column_type::fixed:
             return false;
         case column_type::lower_bound:
-            if (is_neg(rc.get_val())) {
+            if (is_neg(rc.coeff())) {
                 return this->x_above_lower_bound(j);
             }
 
             return true;
         case column_type::upper_bound:
-            if (is_neg(rc.get_val())) {
+            if (is_neg(rc.coeff())) {
                 return true;
             }
 
             return this->x_below_upper_bound(j);
         case column_type::boxed:
-            if (is_neg(rc.get_val())) {
+            if (is_neg(rc.coeff())) {
                 return this->x_above_lower_bound(j);
             }
 
@@ -923,7 +923,7 @@ public:
             unsigned k = rc.var();
             if (k == j)
                 continue;
-            this->m_d[k] += delta * rc.get_val();
+            this->m_d[k] += delta * rc.coeff();
         }
     }
     
diff --git a/src/math/lp/lu_def.h b/src/math/lp/lu_def.h
index 0dcb2ba1b..df0f53730 100644
--- a/src/math/lp/lu_def.h
+++ b/src/math/lp/lu_def.h
@@ -391,7 +391,7 @@ void lu< M>::find_error_of_yB_indexed(const indexed_vector<T>& y, const vector<i
             if (hj < 0) continue;
             if (m_ii.m_data[hj] == 0)
                 m_ii.set_value(1, hj);
-            m_y_copy.m_data[hj] -= c.get_val() * y_k;
+            m_y_copy.m_data[hj] -= c.coeff() * y_k;
         }
     }
     // add the index of m_y_copy to m_ii
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 039de80ef..9f362443c 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -1,21 +1,10 @@
 /*++
 Copyright (c) 2017 Microsoft Corporation
 
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
 Author:
 
     Lev Nachmanson (levnach)
 
-Revision History:
-
-
 --*/
 
 #pragma once
@@ -30,27 +19,26 @@ Revision History:
 namespace lp {
 
 template <typename T>
-struct row_cell {
-    unsigned m_j; // points to the column
-    unsigned m_offset; // offset in column
-    T        m_value;
-    row_cell(unsigned j, unsigned offset, T const & val) : m_j(j), m_offset(offset), m_value(val) {
+class row_cell {
+    unsigned m_j;         // points to the column
+    unsigned m_offset;    // offset in column
+    T        m_coeff;     // coefficient
+public:
+    row_cell(unsigned j, unsigned offset, T const & val) : m_j(j), m_offset(offset), m_coeff(val) {
     }
     row_cell(unsigned j, unsigned offset) : m_j(j), m_offset(offset) {
     }
-    const T & get_val() const { return m_value;}
-    T & get_val() { return m_value;}
-    const T & coeff() const { return m_value;}
-    T & coeff() { return m_value;}
-    unsigned var() const { return m_j;}
-    unsigned & var() { return m_j;}
-    unsigned offset() const { return m_offset;}
-    unsigned & offset() { return m_offset;}
-            
+    inline const T & coeff() const { return m_coeff; }
+    inline T & coeff() { return m_coeff; }
+    inline unsigned var() const { return m_j; }
+    inline unsigned & var() { return m_j; }
+    inline unsigned offset() const { return m_offset; }
+    inline unsigned & offset() { return m_offset; }            
 };
+
 template <typename T>
 std::ostream& operator<<(std::ostream& out, const row_cell<T>& rc) {
-    return out << "(m_j=" << rc.m_j << ", m_offset= " << rc.m_offset << ", m_value=" << rc.m_value << ")";   
+    return out << "(j=" << rc.var() << ", offset= " << rc.offset() << ", coeff=" << rc.coeff() << ")";   
 }
 struct empty_struct {};
 typedef row_cell<empty_struct> column_cell;
@@ -102,11 +90,11 @@ public:
 public:
 
     const T & get_val(const column_cell & c) const {
-        return m_rows[c.var()][c.m_offset].get_val();
+        return m_rows[c.var()][c.offset()].coeff();
     }
 
     column_cell & get_column_cell(const row_cell<T> &rc) {
-        return m_columns[rc.m_j][rc.m_offset];
+        return m_columns[rc.var()][rc.offset()];
     }
     
     void init_row_columns(unsigned m, unsigned n);
@@ -243,7 +231,7 @@ public:
 
     void pop_row_columns(const vector<row_cell<T>> & row) {
         for (auto & c : row) {
-            unsigned j = c.m_j;
+            unsigned j = c.var();
             auto & col = m_columns[j];
             lp_assert(col[col.size() - 1].var() == m_rows.size() -1 ); // todo : start here!!!!
             col.pop_back();
@@ -277,13 +265,13 @@ public:
 
     void multiply_row(unsigned row, T const & alpha) {
         for (auto & t : m_rows[row]) {
-            t.m_value *= alpha;
+            t.coeff() *= alpha;
         }
     }
 
     void divide_row(unsigned row, T const & alpha) {
         for (auto & t : m_rows[row]) {
-            t.m_value /= alpha;
+            t.coeff() /= alpha;
         }
     }
     
@@ -306,12 +294,12 @@ public:
         m_rows[ii] = t;
         // now fix the columns
         for (auto & rc : m_rows[i]) {
-            column_cell & cc = m_columns[rc.m_j][rc.m_offset];
+            column_cell & cc = m_columns[rc.var()][rc.offset()];
             lp_assert(cc.var() == ii);
             cc.var() = i;
         }
         for (auto & rc : m_rows[ii]) {
-            column_cell & cc = m_columns[rc.m_j][rc.m_offset];
+            column_cell & cc = m_columns[rc.var()][rc.offset()];
             lp_assert(cc.var() == i);
             cc.var() = ii;
         }
@@ -326,17 +314,17 @@ public:
             return;
         
         for (const auto & c : m_rows[row_index]) {
-            if (c.m_j == j) {
+            if (c.var() == j) {
                 continue;
             }
-            T & wv = m_work_vector.m_data[c.m_j];
+            T & wv = m_work_vector.m_data[c.var()];
             bool was_zero = is_zero(wv);
-            wv -= alpha * c.m_value;
+            wv -= alpha * c.coeff();
             if (was_zero)
-                m_work_vector.m_index.push_back(c.m_j);
+                m_work_vector.m_index.push_back(c.var());
             else {
                 if (is_zero(wv)) {
-                    m_work_vector.erase_from_index(c.m_j);
+                    m_work_vector.erase_from_index(c.var());
                 }
             }
         }
@@ -390,7 +378,7 @@ public:
         L ret = zero_of_type<L>();
         lp_assert(row < m_rows.size());
         for (auto & it : m_rows[row]) {
-            ret += w[it.m_j] * it.get_val();
+            ret += w[it.var()] * it.coeff();
         }
         return ret;
     }
@@ -402,7 +390,7 @@ public:
         column_cell_plus(const column_cell & c, const static_matrix& A) :
             m_c(c), m_A(A) {}
         unsigned var() const { return m_c.var(); }
-        const T & coeff() const { return m_A.m_rows[var()][m_c.m_offset].get_val(); }
+        const T & coeff() const { return m_A.m_rows[var()][m_c.offset()].coeff(); }
         
     };
     
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index 405ca18e8..b48e24388 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -47,21 +47,21 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
     T alpha = -get_val(c);
     lp_assert(!is_zero(alpha));
     auto & rowii = m_rows[ii];
-    remove_element(rowii, rowii[c.m_offset]);
+    remove_element(rowii, rowii[c.offset()]);
     scan_row_ii_to_offset_vector(rowii);
     unsigned prev_size_ii = rowii.size();
     // run over the pivot row and update row ii
     for (const auto & iv : m_rows[i]) {
         unsigned j = iv.var();
         if (j == pivot_col) continue;
-        T alv = alpha * iv.m_value;
-        lp_assert(!is_zero(iv.m_value));
+        T alv = alpha * iv.coeff();
+        lp_assert(!is_zero(iv.coeff()));
         int j_offs = m_vector_of_row_offsets[j];
         if (j_offs == -1) { // it is a new element
             add_new_element(ii, j, alv);
         }
         else {
-            rowii[j_offs].m_value += alv;
+            rowii[j_offs].coeff() += alv;
         }
     }
     // clean the work vector
@@ -71,7 +71,7 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
 
     // remove zeroes
     for (unsigned k = rowii.size(); k-- > 0;  ) {
-        if (is_zero(rowii[k].m_value)) 
+        if (is_zero(rowii[k].coeff()))
             remove_element(rowii, rowii[k]);
     }
     return !rowii.empty();
@@ -188,7 +188,7 @@ template <typename T, typename X>    void static_matrix<T, X>::copy_column_to_in
 template <typename T, typename X>    T static_matrix<T, X>::get_max_abs_in_row(unsigned row) const {
     T ret = numeric_traits<T>::zero();
     for (auto & t : m_rows[row]) {
-        T a = abs(t.get_val());
+        T a = abs(t.coeff());
         if (a  > ret) {
             ret = a;
         }
@@ -200,7 +200,7 @@ template <typename T, typename X>    T static_matrix<T, X>::get_min_abs_in_row(u
     bool first_time = true;
     T ret = numeric_traits<T>::zero();
     for (auto & t : m_rows[row]) {
-        T a = abs(t.get_val());
+        T a = abs(t.coeff());
         if (first_time) {
             ret = a;
             first_time = false;
@@ -245,7 +245,7 @@ template <typename T, typename X>    void static_matrix<T, X>::check_consistency
         for (auto & t : m_rows[i]) {
             std::pair<unsigned, unsigned> p(i, t.var());
             lp_assert(by_rows.find(p) == by_rows.end());
-            by_rows[p] = t.get_val();
+            by_rows[p] = t.coeff();
         }
     }
     std::unordered_map<std::pair<unsigned, unsigned>, T> by_cols;
@@ -311,7 +311,7 @@ template <typename T, typename X>    void static_matrix<T, X>::cross_out_row_fro
 template <typename T, typename X>    T static_matrix<T, X>::get_elem(unsigned i, unsigned j) const { // should not be used in efficient code !!!!
     for (auto & t : m_rows[i]) {
         if (t.var() == j) {
-            return t.get_val();
+            return t.coeff();
         }
     }
     return numeric_traits<T>::zero();
@@ -329,8 +329,8 @@ template <typename T, typename X>    T static_matrix<T, X>::get_balance() const
 template <typename T, typename X>    T static_matrix<T, X>::get_row_balance(unsigned row) const {
     T ret = zero_of_type<T>();
     for (auto & t : m_rows[row]) {
-        if (numeric_traits<T>::is_zero(t.get_val())) continue;
-        T a = abs(t.get_val());
+        if (numeric_traits<T>::is_zero(t.coeff())) continue;
+        T a = abs(t.coeff());
         numeric_traits<T>::log(a);
         ret += a * a;
     }
@@ -348,11 +348,11 @@ template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
             s.insert(rc.var());
             if (rc.var() >= m_columns.size())
                 return false;
-            if (rc.m_offset >= m_columns[rc.var()].size())
+            if (rc.offset() >= m_columns[rc.var()].size())
                 return false;
-            if (rc.get_val() != get_val(m_columns[rc.var()][rc.m_offset]))
+            if (rc.coeff() != get_val(m_columns[rc.var()][rc.offset()]))
                 return false;
-            if (is_zero(rc.get_val())) {
+            if (is_zero(rc.coeff())) {
                 return false;
             }
             
@@ -369,24 +369,21 @@ template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
             s.insert(cc.var());
             if (cc.var() >= m_rows.size())
                 return false;
-            if (cc.m_offset >= m_rows[cc.var()].size())
+            if (cc.offset() >= m_rows[cc.var()].size())
                 return false;
-            if (get_val(cc) != m_rows[cc.var()][cc.m_offset].get_val())
+            if (get_val(cc) != m_rows[cc.var()][cc.offset()].coeff())
                 return false;
         }
-    }
-
-   
-    
+    }    
     return true;
 }
 
 template <typename T, typename X>
 void static_matrix<T, X>::remove_element(vector<row_cell<T>> & row_vals, row_cell<T> & row_el_iv) {
-    unsigned column_offset = row_el_iv.m_offset;
+    unsigned column_offset = row_el_iv.offset();
     auto & column_vals = m_columns[row_el_iv.var()];
     column_cell& cs = m_columns[row_el_iv.var()][column_offset];
-    unsigned row_offset = cs.m_offset;
+    unsigned row_offset = cs.offset();
     if (column_offset != column_vals.size() - 1) {
         auto & cc = column_vals[column_offset] = column_vals.back(); // copy from the tail
         m_rows[cc.var()][cc.offset()].offset() = column_offset;
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index d30580497..30d7b66c3 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -64,22 +64,21 @@ namespace smt {
         expr* s = nullptr, *r = nullptr;
         expr* e = ctx.bool_var2expr(lit.var());
         expr_ref id(a().mk_int(e->get_id()), m);
-        unsigned idx = 0;
         VERIFY(str().is_in_re(e, s, r));
         sort* seq_sort = m.get_sort(s);
         vector<expr_ref_vector> patterns;
-        auto mk_cont = [&](unsigned idx) {
+        auto mk_cont = [&](unsigned idx) { 
             return sk().mk("seq.cont", id, a().mk_int(idx), seq_sort);
         };
+        unsigned idx = 0;
         if (seq_rw().is_re_contains_pattern(r, patterns)) {
-            expr_ref t(m);
             expr_ref_vector ts(m);
             ts.push_back(mk_cont(idx));
             for (auto const& p : patterns) {
                 ts.append(p);
                 ts.push_back(mk_cont(++idx));
             }
-            t = th.mk_concat(ts, seq_sort);
+            expr_ref t = th.mk_concat(ts, seq_sort);
             th.propagate_eq(lit, s, t, true);
             return true;
         }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2336a4670..e9b284017 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1012,6 +1012,7 @@ public:
     }
 
     bool internalize_atom(app * atom, bool gate_ctx) {
+        TRACE("arith", tout << mk_pp(atom, m) << "\n";);
         SASSERT(!ctx().b_internalized(atom));
         expr* n1, *n2;
         rational r;
@@ -1722,7 +1723,9 @@ public:
         final_check_status st = FC_DONE;
         switch (is_sat) {
         case l_true:
-            TRACE("arith", display(tout););
+            TRACE("arith", /*display(tout);*/
+                  ctx().display(tout);
+                  );
             switch (check_lia()) {
             case l_true:
                 break;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 71797fe2f..d2c4d93e6 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1173,6 +1173,8 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
     expr_ref lenl = mk_len(l);
     expr_ref lenr = mk_len(r);
     literal lit = mk_eq(lenl, lenr, false);
+    ctx.mark_as_relevant(lit);
+
     if (ctx.get_assignment(lit) == l_true) {
         expr_ref_vector lhs(m), rhs(m);
         lhs.append(l2, ls2);
@@ -2753,7 +2755,6 @@ bool theory_seq::lower_bound(expr* e, rational& lo) const {
     VERIFY(m_autil.is_int(e));
     bool is_strict = true;
     return m_arith_value.get_lo(e, lo, is_strict) && !is_strict && lo.is_int();
-
 }
 
 bool theory_seq::upper_bound(expr* e, rational& hi) const {