diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 965e9acc7..d83aded9c 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1729,7 +1729,7 @@ constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, c
 }
 
 void lar_solver::remove_non_fixed_from_fixed_var_table() {
-    vector<value_sort_pair> to_remove;
+    vector<mpq> to_remove;
     for (const auto& p : m_fixed_var_table) {
         unsigned j = p.m_value;
         if (j >= column_count() || !column_is_fixed(j))
@@ -1746,7 +1746,7 @@ void lar_solver::register_in_fixed_var_table(unsigned j, unsigned & equal_to_j)
     if (!bound.y.is_zero())
         return;
 
-    value_sort_pair key(bound.x, column_is_int(j));
+    const mpq& key = bound.x;
     unsigned k;
     if (!m_fixed_var_table.find(key, k)) {
         m_fixed_var_table.insert(key, j);
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 727a0ca7f..05d828c43 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -49,8 +49,6 @@ namespace lp {
 class int_branch;
 class int_solver;
 class lar_solver : public column_namer {
-    typedef std::pair<mpq, bool> value_sort_pair;
-    typedef pair_hash<obj_hash<mpq>, bool_hash> value_sort_pair_hash;
     struct term_hasher {
         std::size_t operator()(const lar_term &t) const
         {            
@@ -105,10 +103,7 @@ class lar_solver : public column_namer {
     vector<impq>                                        m_backup_x;
     stacked_vector<unsigned>                            m_usage_in_terms;
     // ((x[j], is_int(j))->j)  for fixed j, used in equalities propagation
-    map<value_sort_pair,
-        unsigned,
-        value_sort_pair_hash,
-        default_eq<value_sort_pair>>                    m_fixed_var_table;
+    map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>  m_fixed_var_table;
     // end of fields
 
     ////////////////// methods ////////////////////////////////
@@ -290,16 +285,10 @@ class lar_solver : public column_namer {
     void register_normalized_term(const lar_term&, lpvar);
     void deregister_normalized_term(const lar_term&);
 public:
-    const map<value_sort_pair,
-        unsigned,
-        value_sort_pair_hash,
-                  default_eq<value_sort_pair>>& fixed_var_table() const {
+    const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table() const {
         return m_fixed_var_table;
     }
-    map<value_sort_pair,
-        unsigned,
-        value_sort_pair_hash,
-                  default_eq<value_sort_pair>>& fixed_var_table() {
+    map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table() {
         return m_fixed_var_table;
     }
     unsigned external_to_column_index(unsigned) const;
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index a2a5efbdf..bb376dfe4 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -324,9 +324,8 @@ public:
         if (is_offset_row(rid, x, y, k)) {
             if (y == null_lpvar) {
                 // x is an implied fixed var at k.
-                value_sort_pair key(k, is_int(x));
                 unsigned x2;
-                if (lp().fixed_var_table().find(key, x2) && !is_equal(x, x2)) {
+                if (lp().fixed_var_table().find(k, x2) && !is_equal(x, x2)) {
                     SASSERT(lp().column_is_fixed(x2) && get_lower_bound_rational(x2) == k && is_int(x) == is_int(x2)); 
                     explanation ex;
                     constraint_index lc, uc;