diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 883ee2202..f02a63fc6 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -21,6 +21,7 @@ Author:
 #include <limits>
 #include "math/simplex/sparse_matrix.h"
 #include "util/heap.h"
+#include "util/map.h"
 #include "util/lbool.h"
 #include "util/uint_set.h"
 
@@ -80,13 +81,20 @@ namespace polysat {
             numeral m_base_coeff;            
         };
 
-        struct offset_eq {
+        struct var_eq {
             var_t x, y;
             row r1, r2;
-            offset_eq(var_t x, var_t y, row const& r1, row const& r2):
+            var_eq(var_t x, var_t y, row const& r1, row const& r2):
                 x(x), y(y), r1(r1), r2(r2) {}
         };
 
+        struct fix_entry {
+            var_t x;
+            row r;
+            fix_entry(var_t x, row const& r): x(x), r(r) {}
+            fix_entry():x(null_var), r(0) {}
+        };
+
         static const var_t null_var = UINT_MAX;
         reslimit&                   m_limit;
         mutable manager             m;
@@ -96,7 +104,7 @@ namespace polysat {
         var_heap                    m_to_patch;
         vector<var_info>            m_vars;
         vector<row_info>            m_rows;
-        vector<offset_eq>           m_offset_eqs;
+        vector<var_eq>              m_var_eqs;
         bool                        m_bland { false };
         unsigned                    m_blands_rule_threshold { 1000 };
         random_gen                  m_random;
@@ -104,6 +112,7 @@ namespace polysat {
         unsigned                    m_infeasible_var { null_var };
         unsigned_vector             m_base_vars;
         stats                       m_stats;
+        map<numeral, fix_entry, typename manager::hash, typename manager::eq> m_value2fixed_var;
 
     public:
         fixplex(reslimit& lim):
@@ -153,6 +162,7 @@ namespace polysat {
         bool is_offset_row(row const& r, numeral& cx, var_t& x, numeral& cy, var_t & y) const;
         void lookahead_eq(row const& r1, numeral const& cx, var_t x, numeral const& cy, var_t y);
         void get_offset_eqs(row const& r);
+        void fixed_var_eh(row const& r, var_t x);
         void eq_eh(var_t x, var_t y, row const& r1, row const& r2);
         void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
         numeral value2delta(var_t v, numeral const& new_value) const;
@@ -166,6 +176,7 @@ namespace polysat {
         bool is_free(var_t v) const { return lo(v) == hi(v); }
         bool is_non_free(var_t v) const { return !is_free(v); }
         bool is_fixed(var_t v) const { return lo(v) + 1 == hi(v); }
+        bool is_valid_variable(var_t v) const { return v < m_vars.size(); }
         bool is_base(var_t x) const { return m_vars[x].m_is_base; }
         unsigned base2row(var_t x) const { return m_vars[x].m_base2row; }
         numeral const& row2value(row const& r) const { return m_rows[r.id()].m_value; }
@@ -206,6 +217,16 @@ namespace polysat {
         static const uint64_t max_numeral = 0; // std::limits<uint64_t>::max();
         struct manager {
             typedef uint64_t numeral;
+            struct hash {
+                unsigned operator()(numeral const& n) const { 
+                    return static_cast<unsigned>(n); 
+                }
+            };
+            struct eq {
+                bool operator()(numeral const& a, numeral const& b) const {
+                    return a == b;
+                }
+            };
             void reset() {}
             void reset(numeral& n) { n = 0; }
             void del(numeral const& n) {}
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index ba97a7850..ffad0dcd7 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -96,13 +96,13 @@ namespace polysat {
         numeral base_coeff = 0;
         numeral value = 0;
         for (auto const& e : M.row_entries(r)) {
-            var_t v = e.m_var;
+            var_t v = e.var();
             if (v == base_var) 
-                base_coeff = e.m_coeff;
+                base_coeff = e.coeff();
             else {
                 if (is_base(v))
                     m_base_vars.push_back(v);
-                value += e.m_coeff * m_vars[v].m_value;
+                value += e.coeff() * m_vars[v].m_value;
             }
         }
         SASSERT(base_coeff != 0);
@@ -147,7 +147,7 @@ namespace polysat {
             row r = c.get_row();
             row_info& ri = m_rows[r.id()];
             var_t s = ri.m_base;
-            ri.m_value += delta * c.get_row_entry().m_coeff;
+            ri.m_value += delta * c.get_row_entry().coeff();
             set_base_value(s);
             add_patch(s);
         }            
@@ -219,7 +219,7 @@ namespace polysat {
         
         pivot(x, y, b, new_value);
 
-        get_offset_eqs(row(base2row(y)));
+        // get_offset_eqs(row(base2row(y)));
 
         return l_true;
     }
@@ -249,8 +249,8 @@ namespace polysat {
         bool best_in_bounds = false;
 
         for (auto const& r : M.row_entries(r)) {
-            var_t y = r.m_var;          
-            numeral const & b = r.m_coeff;  
+            var_t y = r.var();          
+            numeral const & b = r.coeff();  
             if (x == y) 
                 continue;
             if (!has_minimal_trailing_zeros(y, b))
@@ -353,7 +353,7 @@ namespace polysat {
         if (tz1 == 0)
             return true;
         for (auto col : M.col_entries(y)) {
-            numeral c = col.get_row_entry().m_coeff;
+            numeral c = col.get_row_entry().coeff();
             unsigned tz2 = m.trailing_zeros(c);
             if (tz1 > tz2)
                 return false;
@@ -385,8 +385,8 @@ namespace polysat {
         auto r = base2row(x);
         numeral lo_sum = 0, hi_sum = 0, diff = 0;
         for (auto const& e : M.row_entries(row(r))) {
-            var_t v = e.m_var;
-            numeral const& c = e.m_coeff;
+            var_t v = e.var();
+            numeral const& c = e.coeff();
             if (lo(v) == hi(v))
                 return false;
             lo_sum += lo(v) * c;
@@ -419,8 +419,8 @@ namespace polysat {
         numeral fixed = 0;
         unsigned parity = UINT_MAX;
         for (auto const& e : M.row_entries(row(r))) {
-            var_t v = e.m_var;
-            auto c = e.m_coeff;
+            var_t v = e.var();
+            auto c = e.coeff();
             if (is_fixed(v))
                 fixed += value(v)*c;
             else 
@@ -498,7 +498,7 @@ namespace polysat {
             auto z = row2base(r_z);
             auto& row_z = m_rows[rz];
             var_info& zI = m_vars[z];
-            numeral c = col.get_row_entry().m_coeff;
+            numeral c = col.get_row_entry().coeff();
             unsigned tz2 = m.trailing_zeros(c);
             SASSERT(tz1 <= tz2);
             numeral b1 = b >> tz1;
@@ -551,10 +551,7 @@ namespace polysat {
     void fixplex<Ext>::add_patch(var_t v) {
         SASSERT(is_base(v));
         CTRACE("polysat", !in_bounds(v), tout << "Add patch: v" << v << "\n";);
-        if (in_bounds(v)) {
-            
-        }
-        else 
+        if (!in_bounds(v)) 
             m_to_patch.insert(v);
     }
 
@@ -649,6 +646,8 @@ namespace polysat {
      *
      * Fixed variable equalities
      * -------------------------
+     * Use persistent hash-table of variables that are fixed at values.
+     * Update table when a variable gets fixed and check for collisions.
      * 
      */
 
@@ -669,10 +668,10 @@ namespace polysat {
         if (!row2integral(r))
             return false;
         for (auto const& e : M.row_entries(r)) {
-            var_t v = e.m_var;
+            var_t v = e.var();
             if (is_fixed(v))
                 continue;
-            numeral const& c = e.m_coeff;
+            numeral const& c = e.coeff();
             if (x == null_var) {
                 cx = c;
                 x = v;
@@ -709,11 +708,23 @@ namespace polysat {
         }
     }
 
+    /**
+     * Accumulate equalities between variables fixed to the same values.
+     */
+    template<typename Ext>
+    void fixplex<Ext>::fixed_var_eh(row const& r, var_t x) {
+        numeral val = value(x);
+        fix_entry e;
+        if (m_value2fixed_var.find(val, e) && is_valid_variable(e.x) && is_fixed(e.x) && value(e.x) == val && e.x != x) 
+            eq_eh(x, y, e.r, r);
+        else 
+            m_value2fixed_var.insert(val, fix_entry(x, r));
+    }
+
     template<typename Ext>
     void fixplex<Ext>::eq_eh(var_t x, var_t y, row const& r1, row const& r2) {
-        m_offset_eqs.push_back(offset_eq(x, y, r1, r2));
-    }
-    
+        m_var_eqs.push_back(var_eq(x, y, r1, r2));
+    }    
 
     template<typename Ext>    
     std::ostream& fixplex<Ext>::display(std::ostream& out) const {
@@ -730,9 +741,9 @@ namespace polysat {
     template<typename Ext>    
     std::ostream& fixplex<Ext>::display_row(std::ostream& out, row const& r, bool values) {
         for (auto const& e : M.row_entries(r)) {
-            var_t v = e.m_var;
-            if (e.m_coeff != 1)
-                out << e.m_coeff << " * ";
+            var_t v = e.var();
+            if (e.coeff() != 1)
+                out << e.coeff() << " * ";
             out << "v" << v << " ";
             if (values) 
                 out << value(v) << " [" << lo(v) << ", " << hi(v) << "[ ";            
@@ -766,8 +777,8 @@ namespace polysat {
         numeral sum = 0;
         numeral base_coeff = m_rows[r.id()].m_base_coeff;
         for (auto const& e : M.row_entries(r)) {
-            sum += value(e.m_var) * e.m_coeff;
-            SASSERT(s != e.m_var || base_coeff == e.m_coeff);
+            sum += value(e.var()) * e.coeff();
+            SASSERT(s != e.var() || base_coeff == e.coeff());
         }
         if (sum >= base_coeff) {
             IF_VERBOSE(0, M.display_row(verbose_stream(), r););
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index bc02ce5ef..1d9ed1819 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -76,13 +76,13 @@ namespace simplex {
         scoped_eps_numeral value(em), tmp(em);
         row_iterator it = M.row_begin(r), end = M.row_end(r);
         for (; it != end; ++it) {
-            var_t v = it->m_var;
+            var_t v = it->var();
             if (v == base_var) {
-                m.set(base_coeff, it->m_coeff);
+                m.set(base_coeff, it->coeff());
             }
             else {
                 SASSERT(!is_base(v));
-                em.mul(m_vars[v].m_value, it->m_coeff, tmp);
+                em.mul(m_vars[v].m_value, it->coeff(), tmp);
                 em.add(value, tmp, value);
             }
         }
@@ -97,8 +97,8 @@ namespace simplex {
               bool first = true;
               for (; it2 != end; ++it2) {
                   if (!first) tout << " + ";
-                  tout << "v" << it2->m_var << " * ";
-                  m.display(tout, it2->m_coeff); tout << " ";                  
+                  tout << "v" << it2->var() << " * ";
+                  m.display(tout, it2->coeff()); tout << " ";                  
                   first = false;
               }
               tout << "\n";
@@ -176,7 +176,7 @@ namespace simplex {
                 new_value = vi.m_value;
             }
             // need to move var such that old_base comes in bound.
-            update_and_pivot(old_base, var, re.m_coeff, new_value);   
+            update_and_pivot(old_base, var, re.coeff(), new_value);   
             SASSERT(is_base(var));
             SASSERT(m_vars[var].m_base2row == r.id());            
             SASSERT(!below_lower(old_base) && !above_upper(old_base));
@@ -285,10 +285,10 @@ namespace simplex {
     void simplex<Ext>::display_row(std::ostream& out, row const& r, bool values) {
         row_iterator it = M.row_begin(r), end = M.row_end(r);        
         for (; it != end; ++it) {
-            m.display(out, it->m_coeff);
-            out << "*v" << it->m_var << " ";
+            m.display(out, it->coeff());
+            out << "*v" << it->var() << " ";
             if (values) {
-                var_info const& vi = m_vars[it->m_var];
+                var_info const& vi = m_vars[it->var()];
                 out << em.to_string(vi.m_value);
                 out << " [";
                 if (vi.m_lower_valid) out << em.to_string(vi.m_lower); else out << "-oo";
@@ -405,7 +405,7 @@ namespace simplex {
         for (; it != end; ++it) {
             row r_k = it.get_row();
             if (r_k.id() != r_i) {
-                a_kj = it.get_row_entry().m_coeff;
+                a_kj = it.get_row_entry().coeff();
                 a_kj.neg();
                 M.mul(r_k, a_ij);
                 M.add(r_k, a_kj, row(r_i));
@@ -439,7 +439,7 @@ namespace simplex {
             var_t s = m_row2base[r.id()];
             var_info& si = m_vars[s];
             scoped_eps_numeral delta2(em);
-            numeral const& coeff = it.get_row_entry().m_coeff;
+            numeral const& coeff = it.get_row_entry().coeff();
             em.mul(delta,  coeff, delta2);
             em.div(delta2, si.m_base_coeff, delta2);
             delta2.neg();
@@ -555,9 +555,9 @@ namespace simplex {
         row_iterator it = M.row_begin(r), end = M.row_end(r);
     
         for (; it != end; ++it) {
-            var_t x_j       = it->m_var;          
+            var_t x_j       = it->var();          
             if (x_i == x_j) continue;
-            numeral const & a_ij = it->m_coeff;  
+            numeral const & a_ij = it->coeff();  
                                                                
             bool is_neg = is_below ? m.is_neg(a_ij) : m.is_pos(a_ij);
             bool is_pos = !is_neg;                                   
@@ -618,8 +618,8 @@ namespace simplex {
         row r(m_vars[x_i].m_base2row);
         row_iterator it = M.row_begin(r), end = M.row_end(r);
         for (; it != end; ++it) {
-            var_t x_j = it->m_var;    
-            numeral const & a_ij = it->m_coeff;                
+            var_t x_j = it->var();    
+            numeral const & a_ij = it->coeff();                
             bool is_neg = is_below ? m.is_neg(a_ij) : m.is_pos(a_ij);
             if (x_i != x_j && ((!is_neg && above_lower(x_j)) || (is_neg && below_upper(x_j)))) {
                 SASSERT(!is_base(x_j));
@@ -749,7 +749,7 @@ namespace simplex {
             //
             var_t s = m_row2base[it.get_row().id()];
             var_info& vs = m_vars[s];
-            numeral const& coeff = it.get_row_entry().m_coeff;
+            numeral const& coeff = it.get_row_entry().coeff();
             numeral const& base_coeff = vs.m_base_coeff;
             SASSERT(!m.is_zero(coeff));
             bool base_to_lower = (m.is_pos(coeff) != m.is_pos(base_coeff)) == to_lower;
@@ -801,9 +801,9 @@ namespace simplex {
         bool inc_y = false;
 
         for (; it != end; ++it) {
-            var_t x = it->m_var;          
+            var_t x = it->var();          
             if (x == v) continue; 
-            bool inc_x = m.is_pos(it->m_coeff) == m.is_pos(m_vars[v].m_base_coeff);
+            bool inc_x = m.is_pos(it->coeff()) == m.is_pos(m_vars[v].m_base_coeff);
             if ((inc_x && at_upper(x)) || (!inc_x && at_lower(x))) {
                 TRACE("simplex", tout << "v" << x << " pos: " << inc_x 
                       << " at upper: " << at_upper(x) 
@@ -867,7 +867,7 @@ namespace simplex {
             row r = it.get_row();
             var_t s = m_row2base[r.id()];
             var_info& vi = m_vars[s];
-            numeral const& a_ij = it.get_row_entry().m_coeff;
+            numeral const& a_ij = it.get_row_entry().coeff();
             numeral const& a_ii = vi.m_base_coeff;
             bool sign_eq = (m.is_pos(a_ii) == m.is_pos(a_ij));
             bool inc_s =  sign_eq != inc_x_j;
@@ -1013,9 +1013,9 @@ namespace simplex {
         row_iterator it = M.row_begin(r), end = M.row_end(r);
         scoped_eps_numeral sum(em), tmp(em);
         for (; it != end; ++it) {
-            em.mul(m_vars[it->m_var].m_value, it->m_coeff, tmp);
+            em.mul(m_vars[it->var()].m_value, it->coeff(), tmp);
             sum += tmp;
-            SASSERT(s != it->m_var || m.eq(m_vars[s].m_base_coeff, it->m_coeff));
+            SASSERT(s != it->var() || m.eq(m_vars[s].m_base_coeff, it->coeff()));
         }
         if (!em.is_zero(sum)) {
             IF_VERBOSE(0, M.display_row(verbose_stream(), r););
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index 7cc2ee564..f724d816d 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -32,10 +32,14 @@ namespace simplex {
         typedef typename Ext::manager manager;
         typedef unsigned var_t;
 
-        struct row_entry {
+        class row_entry {
+            friend class sparse_matrix;
             numeral         m_coeff;
             var_t           m_var;
+        public:
             row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {}
+            inline numeral const& coeff() const { return m_coeff; }
+            inline var_t var() const { return m_var; }
         };
 
     private:
@@ -63,7 +67,7 @@ namespace simplex {
             };            
             _row_entry(numeral && c, var_t v) : row_entry(std::move(c), v), m_col_idx(0) {}
             _row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {}
-            bool is_dead() const { return row_entry::m_var == dead_id; }
+            bool is_dead() const { return row_entry::var() == dead_id; }
         };
 
         /**
diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index 5f16f5f04..9c53cccbe 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/src/math/simplex/sparse_matrix_def.h
@@ -99,10 +99,10 @@ namespace simplex {
                 if (i != j) {
                     _row_entry & t2 = m_entries[j];
                     m.swap(t2.m_coeff, t1.m_coeff);
-                    t2.m_var = t1.m_var;
+                    t2.m_var = t1.var();
                     t2.m_col_idx = t1.m_col_idx;
                     SASSERT(!t2.is_dead());
-                    column & col = cols[t2.m_var];
+                    column & col = cols[t2.var()];
                     col.m_entries[t2.m_col_idx].m_row_idx = j;
                 }
                 j++;
@@ -138,8 +138,8 @@ namespace simplex {
         unsigned idx = 0;
         for (auto const& e : m_entries) {
             if (!e.is_dead()) {
-                result_map[e.m_var] = idx;
-                idxs.push_back(e.m_var);
+                result_map[e.var()] = idx;
+                idxs.push_back(e.var());
             }
             ++idx;
         }
@@ -150,7 +150,7 @@ namespace simplex {
     int sparse_matrix<Ext>::_row::get_idx_of(var_t v) const {
         unsigned idx = 0; 
         for (auto const& e : m_entries) {
-            if (!e.is_dead() && e.m_var == v)
+            if (!e.is_dead() && e.var() == v)
                 return idx;
             ++idx;
         }
@@ -350,7 +350,7 @@ namespace simplex {
             else {                                                      \
                 /* variable v is in row1 */                             \
                 _row_entry & r_entry   = r1.m_entries[pos];             \
-                SASSERT(r_entry.m_var == v);                            \
+                SASSERT(r_entry.var() == v);                            \
                 _ADD_COEFF_;                                            \
                 if (m.is_zero(r_entry.m_coeff)) {                       \
                     del_row_entry(r1, pos);                             \
@@ -386,7 +386,7 @@ namespace simplex {
     template<typename Ext>
     void sparse_matrix<Ext>::del_row_entry(_row& r, unsigned pos) {
         _row_entry & r_entry   = r.m_entries[pos];     
-        var_t v = r_entry.m_var;
+        var_t v = r_entry.var();
         int col_idx = r_entry.m_col_idx;                                
         r.del_row_entry(pos);                              
         column & c  = m_columns[v];                   
@@ -452,12 +452,12 @@ namespace simplex {
         g.reset();
         row_iterator it = row_begin(r), end = row_end(r); 
         for (; it != end && !m.is_one(g); ++it) {
-            if (!m.is_int(it->m_coeff)) {
+            if (!m.is_int(it->coeff())) {
                 g = numeral(1);  
                 break;
             }
             if (m.is_zero(g)) g = it->m_coeff;
-            else m.gcd(g, it->m_coeff, g);
+            else m.gcd(g, it->coeff(), g);
         }   
         if (m.is_zero(g)) {
             g = numeral(1);
@@ -498,13 +498,13 @@ namespace simplex {
                 continue;
             }
             DEBUG_CODE(
-                SASSERT(!vars.contains(e.m_var));
+                SASSERT(!vars.contains(e.var()));
                 SASSERT(!m.is_zero(e.m_coeff));            
-                SASSERT(e.m_var != dead_id);
-                col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx];
+                SASSERT(e.var() != dead_id);
+                col_entry const& c = m_columns[e.var()].m_entries[e.m_col_idx];
                 SASSERT((unsigned)c.m_row_id == row_id);
                 SASSERT((unsigned)c.m_row_idx == i););
-            vars.insert(e.m_var);
+            vars.insert(e.var());
         }                  
         int idx = r.m_first_free_idx;
         while (idx != -1) {
@@ -533,7 +533,7 @@ namespace simplex {
             DEBUG_CODE(
                 _row const& row = m_rows[c.m_row_id];
                 _row_entry const& r = row.m_entries[c.m_row_idx];
-                SASSERT(r.m_var == v); 
+                SASSERT(r.var() == v); 
                 SASSERT((unsigned)r.m_col_idx == i););
             rows.insert(c.m_row_id);
         }                           
@@ -571,8 +571,8 @@ namespace simplex {
     void sparse_matrix<Ext>::display_row(std::ostream& out, row const& r) {
         row_iterator it = row_begin(r), end = row_end(r); 
         for (; it != end; ++it) {
-            m.display(out, it->m_coeff);
-            out << "*v" << it->m_var << " ";
+            m.display(out, it->coeff());
+            out << "*v" << it->var() << " ";
         }
         out << "\n";
     }
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 3a19b1c19..b5abc7a2a 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -1011,7 +1011,7 @@ namespace smt {
             expr_ref tmp(m);
             core.reset();
             for (; it != end; ++it) {
-                unsigned v = it->m_var;
+                unsigned v = it->var();
                 if (num_nodes <= v && v < num_nodes + num_edges) {
                     unsigned edge_id = v - num_nodes;
                     literal lit = m_edges[edge_id].m_justification;
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index e9747c4ae..80fbe4022 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1283,7 +1283,7 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
         expr_ref tmp(m);
         core.reset();
         for (; it != end; ++it) {
-            unsigned v = it->m_var;
+            unsigned v = it->var();
             if (is_simplex_edge(v)) {
                 unsigned edge_id = simplex2edge(v);
                 literal lit = m_graph.get_explanation(edge_id);