diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 4d4ac4975..51e2f533e 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -76,7 +76,7 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
 template <typename T> 
 bool horner::lemmas_on_row(const T& row) {
     SASSERT (row_is_interesting(row));
-    c().clear_and_resize_active_var_set();
+    c().clear_active_var_set();
     u_dependency* dep = nullptr;
     create_sum_from_row(row, m_nex_creator, m_row_sum, dep);
     c().set_active_vars_weights(m_nex_creator); // without this call the comparisons will be incorrect
@@ -110,7 +110,7 @@ bool horner::horner_lemmas() {
         for (auto & s : matrix.m_columns[j])
             rows_to_check.insert(s.var());
     }
-    c().clear_and_resize_active_var_set();
+    c().clear_active_var_set();
     svector<unsigned> rows;
     for (unsigned i : rows_to_check) {
         if (row_is_interesting(matrix.m_rows[i]))
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index 2b6fc3cd8..9d530acee 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -23,7 +23,7 @@
 #include "math/lp/nla_intervals.h"
 #include "math/lp/nex.h"
 #include "math/lp/cross_nested.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 
 namespace nla {
 class core;
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index 4c9f43ffe..b9d09081a 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -20,7 +20,7 @@ Revision History:
 #pragma once
 #include "math/lp/lp_settings.h"
 #include "math/lp/static_matrix.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 #include "math/lp/lar_term.h"
 #include "math/lp/lar_constraints.h"
 #include "math/lp/hnf_cutter.h"
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 4aecbf2cc..d5d2825bf 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -234,13 +234,13 @@ namespace lp {
         m_usage_in_terms.push();
     }
     
-    void lar_solver::clean_popped_elements(unsigned n, u_set& set) {
+    void lar_solver::clean_popped_elements(unsigned n, indexed_uint_set& set) {
         vector<int> to_remove;
         for (unsigned j : set)
             if (j >= n)
                 to_remove.push_back(j);
         for (unsigned j : to_remove)
-            set.erase(j);
+            set.remove(j);
     }
 
     void lar_solver::clean_popped_elements_for_heap(unsigned n, lpvar_heap& heap) {
@@ -361,7 +361,6 @@ namespace lp {
 
     void lar_solver::prepare_costs_for_r_solver(const lar_term& term) {
         TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
-        m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
         move_non_basic_columns_to_bounds(false);
         auto& rslv = m_mpq_lar_core_solver.m_r_solver;
         lp_assert(costs_are_zeros_for_r_solver());
@@ -619,7 +618,7 @@ namespace lp {
     }
 
     void lar_solver::add_touched_row(unsigned rid) {
-        if (m_settings.bound_propagation())
+        if (m_settings.bound_propagation()) 
             m_touched_rows.insert(rid);
     }
 
@@ -710,9 +709,6 @@ namespace lp {
 
     void lar_solver::solve_with_core_solver() {
         m_mpq_lar_core_solver.prefix_r();
-        if (costs_are_used()) {
-            m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
-        }
         update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
         m_mpq_lar_core_solver.solve();
         set_status(m_mpq_lar_core_solver.m_r_solver.get_status());
@@ -1431,7 +1427,6 @@ namespace lp {
     void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) {
         register_new_ext_var_index(ext_j, is_int);
         m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
-        increase_by_one_columns_with_changed_bounds();
         add_new_var_to_core_fields_for_mpq(false); // false for not adding a row        
     }
     
@@ -1585,11 +1580,7 @@ namespace lp {
 
     void lar_solver::add_basic_var_to_core_fields() {
         m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
-        increase_by_one_columns_with_changed_bounds();
-        m_incorrect_columns.increase_size_by_one();
-        m_touched_rows.increase_size_by_one();
         add_new_var_to_core_fields_for_mpq(true);
-        
     }
 
     bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq& right_side) const {
@@ -1739,8 +1730,8 @@ namespace lp {
         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) {
-        m_columns_with_changed_bounds.insert(j);
-        TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
+         m_columns_with_changed_bounds.insert(j);
+         TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
     }
     void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
                                                                  lconstraint_kind kind,
@@ -2063,7 +2054,6 @@ namespace lp {
 
 
     void lar_solver::round_to_integer_solution() {
-        m_incorrect_columns.resize(column_count());
         for (unsigned j = 0; j < column_count(); j++) {
             if (!column_is_int(j)) continue;
             if (column_corresponds_to_term(j)) continue;
@@ -2085,7 +2075,7 @@ namespace lp {
         }
         if (!m_incorrect_columns.empty()) {
             fix_terms_with_rounded_columns();
-            m_incorrect_columns.clear();
+            m_incorrect_columns.reset();
         }
     }
 
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index fc58d0a70..54abba579 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -85,14 +85,14 @@ class lar_solver : public column_namer {
     stacked_vector<ul_pair> m_columns_to_ul_pairs;
     constraint_set m_constraints;
     // the set of column indices j such that bounds have changed for j
-    u_set m_columns_with_changed_bounds;
-    u_set m_touched_rows;
+    indexed_uint_set m_columns_with_changed_bounds;
+    indexed_uint_set m_touched_rows;
     unsigned_vector m_row_bounds_to_replay;
 
-    u_set m_basic_columns_with_changed_cost;
+    indexed_uint_set m_basic_columns_with_changed_cost;
     // these are basic columns with the value changed, so the corresponding row in the tableau
     // does not sum to zero anymore
-    u_set m_incorrect_columns;
+    indexed_uint_set m_incorrect_columns;
     // copy of m_r_solver.inf_heap()
     unsigned_vector m_inf_index_copy;
     stacked_value<unsigned> m_term_count;
@@ -132,8 +132,7 @@ class lar_solver : public column_namer {
     void add_basic_var_to_core_fields();
     bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs);
 
-    inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.clear(); }
-    inline void increase_by_one_columns_with_changed_bounds() { m_columns_with_changed_bounds.increase_size_by_one(); }
+    inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
     void insert_to_columns_with_changed_bounds(unsigned j);
     void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index, unsigned&);
     void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index);
@@ -175,7 +174,7 @@ class lar_solver : public column_namer {
     }
 
     static void clean_popped_elements_for_heap(unsigned n, lpvar_heap& set);
-    static void clean_popped_elements(unsigned n, u_set& set);
+    static void clean_popped_elements(unsigned n, indexed_uint_set& set);
     bool maximize_term_on_tableau(const lar_term& term,
                                   impq& term_max);
     bool costs_are_zeros_for_r_solver() const;
@@ -349,7 +348,7 @@ class lar_solver : public column_namer {
                     m_row_bounds_to_replay.push_back(i);
             }
         }
-        m_touched_rows.clear();
+        m_touched_rows.reset();
     }
 
     template <typename T>
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index 6db4776db..251199419 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -27,7 +27,7 @@ Revision History:
 #include "math/lp/static_matrix.h"
 #include "math/lp/permutation_matrix.h"
 #include "math/lp/column_namer.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 #include "util/heap.h"
 
 namespace lp {
@@ -92,7 +92,7 @@ public:
     vector<unsigned>      m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
     bool                  m_tracing_basis_changes;
     // these rows are changed by adding to them a multiple of the pivot row
-    u_set*                m_touched_rows;
+    indexed_uint_set*     m_touched_rows = nullptr;
     bool                  m_look_for_feasible_solution_only;
 
     void start_tracing_basis_changes() {
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index d4130faae..c074da16a 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -21,7 +21,7 @@ Revision History:
 #include "math/lp/core_solver_pretty_printer.h"
 #include "math/lp/lp_core_solver_base.h"
 #include "math/lp/static_matrix.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 #include "util/vector.h"
 #include <algorithm>
 #include <cstdlib>
@@ -46,7 +46,7 @@ namespace lp {
         vector<T> m_costs_backup;
         unsigned m_inf_row_index_for_tableau;
         bool m_bland_mode_tableau;
-        u_set m_left_basis_tableau;
+        indexed_uint_set m_left_basis_tableau;
         unsigned m_bland_mode_threshold;
         unsigned m_left_basis_repeated;
         vector<unsigned> m_leaving_candidates;
@@ -627,8 +627,7 @@ namespace lp {
     void init_reduced_costs_tableau();
     void init_tableau_rows() {
         m_bland_mode_tableau = false;
-        m_left_basis_tableau.clear();
-        m_left_basis_tableau.resize(this->m_A.column_count());
+        m_left_basis_tableau.reset();
         m_left_basis_repeated = 0;
     }
     // stage1 constructor
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index 236f29bc0..d82c4bebb 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -10,7 +10,7 @@
 
 #include "math/lp/nla_common.h"
 #include "math/lp/nla_intervals.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 
 namespace nla {
     class core;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 3c1f9da57..86ddb05b7 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -828,14 +828,14 @@ void core::insert_to_refine(lpvar j) {
 
 void core::erase_from_to_refine(lpvar j) {
     TRACE("lar_solver", tout << "j=" << j << '\n';);
-    m_to_refine.erase(j);
+    if (m_to_refine.contains(j))
+        m_to_refine.remove(j);
 }
 
 
 void core::init_to_refine() {
     TRACE("nla_solver_details", tout << "emons:" << pp_emons(*this, m_emons););
-    m_to_refine.clear();
-    m_to_refine.resize(m_lar_solver.number_of_vars());
+    m_to_refine.reset();
     unsigned r = random(), sz = m_emons.number_of_monics();
     for (unsigned k = 0; k < sz; k++) {
         auto const & m = *(m_emons.begin() + (k + r)% sz);
@@ -1407,8 +1407,12 @@ void core::patch_monomial(lpvar j) {
 }
 
 void core::patch_monomials_on_to_refine() {
-    auto to_refine = m_to_refine.index();
     // the rest of the function might change m_to_refine, so have to copy
+    unsigned_vector to_refine;
+    for (unsigned j :m_to_refine) {
+        to_refine.push_back(j);
+    }
+    
     unsigned sz = to_refine.size();
 
     unsigned start = random();
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 938bcbe83..51628b937 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -84,7 +84,7 @@ class core {
     reslimit&                m_reslim;
     std::function<bool(lpvar)> m_relevant;
     vector<lemma> *          m_lemma_vec;
-    lp::u_set                m_to_refine;
+    indexed_uint_set                m_to_refine;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
@@ -99,7 +99,7 @@ class core {
     grobner                  m_grobner;
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
-    mutable lp::u_set        m_active_var_set;
+    mutable indexed_uint_set m_active_var_set;
 
     reslimit                 m_nra_lim;
 
@@ -118,18 +118,15 @@ public:
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
     
-    const lp::u_set&  active_var_set () const { return m_active_var_set;}
+    const indexed_uint_set&  active_var_set () const { return m_active_var_set;}
     bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
 
-    void insert_to_active_var_set(unsigned j) const { m_active_var_set.insert(j); }    
+    void insert_to_active_var_set(unsigned j) const { 
+        m_active_var_set.insert(j); 
+    }    
 
-    void clear_active_var_set() const { m_active_var_set.clear(); }
+    void clear_active_var_set() const { m_active_var_set.reset(); }
 
-    void clear_and_resize_active_var_set() const {
-        m_active_var_set.clear();
-        m_active_var_set.resize(m_lar_solver.number_of_vars());
-    }
-    
     unsigned get_var_weight(lpvar) const;
 
     reslimit& reslim() { return m_reslim; }  
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 974c48d14..4c2f879cf 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -498,9 +498,8 @@ namespace nla {
     }
 
     void grobner::prepare_rows_and_active_vars() {
-        m_rows.clear();
-        m_rows.resize(m_lar_solver.row_count());
-        c().clear_and_resize_active_var_set();
+        m_rows.reset();
+        c().clear_active_var_set();
     }
 
 
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 902ad3a46..ed3aa77db 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -12,7 +12,7 @@
 #include "math/lp/nla_intervals.h"
 #include "math/lp/nex.h"
 #include "math/lp/cross_nested.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 #include "math/grobner/pdd_solver.h"
 
 namespace nla {
@@ -22,7 +22,7 @@ namespace nla {
         dd::pdd_manager          m_pdd_manager;
         dd::solver               m_solver;
         lp::lar_solver&          m_lar_solver;
-        lp::u_set                m_rows;
+        indexed_uint_set                m_rows;
 
         lp::lp_settings& lp_settings();
 
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 1f4e0b76a..377b318dd 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -9,7 +9,7 @@
 #include "math/polynomial/polynomial.h"
 #include "math/polynomial/algebraic_numbers.h"
 #include "util/map.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 #include "math/lp/nla_core.h"
 
 
@@ -23,7 +23,7 @@ struct solver::imp {
     reslimit&                 m_limit;  
     params_ref                m_params; 
     u_map<polynomial::var>    m_lp2nl;  // map from lar_solver variables to nlsat::solver variables        
-    lp::u_set                 m_term_set;
+    indexed_uint_set                 m_term_set;
     scoped_ptr<nlsat::solver> m_nlsat;
     scoped_ptr<scoped_anum>   m_zero;
     mutable variable_map_type m_variable_values; // current model        
@@ -55,7 +55,7 @@ struct solver::imp {
         m_zero = nullptr;
         m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
         m_zero = alloc(scoped_anum, am());
-        m_term_set.clear();
+        m_term_set.reset();
         m_lp2nl.reset();
         vector<nlsat::assumption, false> core;
 
@@ -182,7 +182,7 @@ struct solver::imp {
         m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
         m_zero = alloc(scoped_anum, am());
         m_lp2nl.reset();
-        m_term_set.clear();
+        m_term_set.reset();
         for (auto const& eq : eqs)
             add_eq(eq);
         for (auto const& [v, w] : m_lp2nl) {
@@ -283,8 +283,6 @@ struct solver::imp {
             r = m_nlsat->mk_var(is_int(v));
             m_lp2nl.insert(v, r);
             if (!m_term_set.contains(v) && s.column_corresponds_to_term(v)) {
-                if (v >= m_term_set.data_size())
-                    m_term_set.resize(v + 1);
                 m_term_set.insert(v);
             }
         }
diff --git a/src/math/lp/random_updater.h b/src/math/lp/random_updater.h
index d5cd4928c..f0f767750 100644
--- a/src/math/lp/random_updater.h
+++ b/src/math/lp/random_updater.h
@@ -25,14 +25,14 @@ Revision History:
 #include <string>
 #include <algorithm>
 #include "math/lp/lp_settings.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 // see http://research.microsoft.com/projects/z3/smt07.pdf
 // The class searches for a feasible solution with as many different values of variables as it can find
 namespace lp {
 template <typename T> struct numeric_pair; // forward definition
 class lar_solver; // forward definition
 class random_updater {
-    u_set           m_var_set;
+    indexed_uint_set           m_var_set;
     lar_solver &    m_lar_solver;
     unsigned        m_range;
     bool shift_var(unsigned j);
diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h
index 7d167a4a0..861068106 100644
--- a/src/math/lp/random_updater_def.h
+++ b/src/math/lp/random_updater_def.h
@@ -32,7 +32,6 @@ random_updater::random_updater(
                                const vector<unsigned> & column_indices) :
     m_lar_solver(lar_solver),
     m_range(100000) {
-    m_var_set.resize(m_lar_solver.number_of_vars());
     for (unsigned j : column_indices)
         m_var_set.insert(j);
     TRACE("lar_solver_rand", tout << "size = " << m_var_set.size() << "\n";);
@@ -45,7 +44,9 @@ bool random_updater::shift_var(unsigned j) {
     if (ret) {
         const auto & A = m_lar_solver.A_r();
         for (const auto& c : A.m_columns[j]) {
-            m_var_set.erase(m_lar_solver.r_basis()[c.var()]);
+            unsigned k = m_lar_solver.r_basis()[c.var()];
+            if (m_var_set.contains(k))
+                m_var_set.remove(k);
         }
     }
     return ret;
@@ -54,7 +55,11 @@ bool random_updater::shift_var(unsigned j) {
 
 void random_updater::update() {
     // VERIFY(m_lar_solver.check_feasible());
-    auto columns = m_var_set.index();  // m_var_set is going to change during the loop
+    unsigned_vector columns;
+    // m_var_set is going to change during the loop, make a copy
+    for (unsigned j :  m_var_set) {
+        columns.push_back(j);
+    }
     for (auto j : columns) {
         if (!m_var_set.contains(j)) {
             TRACE("lar_solver_rand", tout << "skipped " << j << "\n";);
diff --git a/src/math/lp/u_set.h b/src/math/lp/u_set.h
deleted file mode 100644
index ce59dccb7..000000000
--- a/src/math/lp/u_set.h
+++ /dev/null
@@ -1,114 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-TBD use indexed_uint_set from src/util/uint_set.h, 
-
---*/
-#pragma once
-#include "util/vector.h"
-#include <ostream>
-namespace lp {
-// serves at a set of non-negative integers smaller than the set size
-class u_set {
-    svector<int> m_data;
-    unsigned_vector m_index;
-
-public:
-    u_set(unsigned size): m_data(size, -1) {}
-    u_set() {}
-    u_set(u_set const& other):
-        m_data(other.m_data),
-        m_index(other.m_index) {}
-
-    bool contains(unsigned j) const {
-        if (j >= m_data.size())
-            return false;
-        return m_data[j] >= 0;
-    }
-    void insert(unsigned j) {
-        lp_assert(j < m_data.size());
-        if (contains(j)) return;
-        m_data[j] = m_index.size();
-        m_index.push_back(j);
-    }
-    void erase(unsigned j) {
-        if (!contains(j)) return;
-        unsigned pos_j = m_data[j];
-        unsigned last_pos = m_index.size() - 1;
-        int last_j = m_index[last_pos];
-        if (last_pos != pos_j) {
-            // move last to j spot
-            m_data[last_j] = pos_j;
-            m_index[pos_j] = last_j;
-        }
-        m_index.pop_back();
-        m_data[j] = -1;
-    }
-
-    int operator[](unsigned j) const { return m_index[j]; }
-    
-    void resize(unsigned size) {
-        if (size < data_size()) {
-            bool copy = false;
-            unsigned i = 0;
-            for (unsigned j : m_index) {
-                if (j < size) {
-                    if (copy) {
-                        m_data[j] = i;
-                        m_index[i] = j;
-                    }
-                    i++;
-                } else {
-                    copy = true;
-                }
-            }
-            m_index.shrink(i);
-        }
-        m_data.resize(size, -1);
-    }
-
-    void increase_size_by_one() {
-        resize(m_data.size() + 1);
-    }
-   
-    unsigned data_size() const {  return m_data.size(); }
-    unsigned size() const { return m_index.size();}
-    bool empty() const { return size() == 0; }
-    void clear() {
-        for (unsigned j : m_index)
-            m_data[j] = -1;
-        m_index.resize(0);
-    }
-
-    std::ostream& display(std::ostream& out) const {
-        for (unsigned j : m_index) {
-            out << j << " ";
-        }
-        out << std::endl;
-        return out;
-    }
-    const unsigned * begin() const { return m_index.begin(); }
-    const unsigned * end() const { return m_index.end(); }
-    const unsigned_vector& index() { return m_index; }
-};
-
-
-}
-
-inline std::ostream& operator<<(std::ostream& out, lp::u_set const& s) {
-    return s.display(out);
-}
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 5784962a5..0e97c3503 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -847,8 +847,7 @@ namespace arith {
         if (m_nla)
             return;
         TRACE("arith", tout << s().scope_lvl() << "\n"; tout.flush(););
-        m_tmp_var_set.clear();
-        m_tmp_var_set.resize(get_num_vars());
+        m_tmp_var_set.reset();
         m_model_eqs.reset();
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(get_num_vars());
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index e5ba06ae6..20252ede9 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -225,7 +225,7 @@ namespace arith {
 
         svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates;
         unsigned                                          m_assume_eq_head = 0;
-        lp::u_set                                         m_tmp_var_set;
+        indexed_uint_set                                         m_tmp_var_set;
 
         unsigned                                          m_num_conflicts = 0;
         lp_api::stats                                     m_stats;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 99faa437d..79b6f79c1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -168,7 +168,7 @@ class theory_lra::imp {
     
     svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates; 
     unsigned                                          m_assume_eq_head;
-    lp::u_set                                         m_tmp_var_set;
+    indexed_uint_set                                         m_tmp_var_set;
     
     unsigned                                          m_num_conflicts;
 
@@ -1493,8 +1493,7 @@ public:
     void random_update() {
         if (m_nla && m_nla->need_check())
             return;
-        m_tmp_var_set.clear();
-        m_tmp_var_set.resize(th.get_num_vars());
+        m_tmp_var_set.reset();
         m_model_eqs.reset();
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index a61b9339e..088a7dac0 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -50,7 +50,7 @@
 #include "math/lp/nla_solver.h"
 #include "math/lp/numeric_pair.h"
 #include "math/lp/static_matrix.h"
-#include "math/lp/u_set.h"
+#include "util/uint_set.h"
 #include "test/lp/argument_parser.h"
 #include "test/lp/gomory_test.h"
 #include "test/lp/smt_reader.h"
@@ -1072,20 +1072,18 @@ void test_bound_propagation() {
 }
 
 void test_int_set() {
-    u_set s(4);
-    s.insert(2);
+    indexed_uint_set s;
     s.insert(1);
     s.insert(2);
     lp_assert(s.contains(2));
     lp_assert(s.size() == 2);
-    s.erase(2);
-    lp_assert(s.size() == 1);
-    s.erase(2);
+    s.remove(2);
     lp_assert(s.size() == 1);
     s.insert(3);
     s.insert(2);
-    s.clear();
+    s.reset();
     lp_assert(s.size() == 0);
+    std::cout << "done test_int_set\n";
 }
 
 void test_rationals_no_numeric_pairs() {
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index b04c67a07..2106d7af8 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -350,6 +350,10 @@ public:
         SASSERT(index < m_size);
         return m_elems[index];
     }
+    unsigned operator[](unsigned index) const {
+        SASSERT(index < m_size);
+        return m_elems[index];
+    }
 
     bool contains(unsigned x) const { return x < m_index.size() && m_index[x] < m_size && m_elems[m_index[x]] == x; }
     void reset() { m_size = 0; }