diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9e4f544c1..e55ac16e8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -48,7 +48,7 @@ namespace lp {
         return out;
     }
 
-    class bound { 
+    class bound {
         smt::bool_var     m_bv;
         smt::theory_var  m_var;
         rational         m_value;
@@ -66,11 +66,11 @@ namespace lp {
         smt::bool_var get_bv() const { return m_bv; }
         bound_kind get_bound_kind() const { return m_bound_kind; }
         rational const& get_value() const { return m_value; }
-        inf_rational get_value(bool is_true) const { 
+        inf_rational get_value(bool is_true) const {
             if (is_true) return inf_rational(m_value);                         // v >= value or v <= value
             if (m_bound_kind == lower_t) return inf_rational(m_value, false);  // v <= value - epsilon
             return inf_rational(m_value, true);                                // v >= value + epsilon
-        } 
+        }
         virtual std::ostream& display(std::ostream& out) const {
             return out << "v" << get_var() << "  " << get_bound_kind() << " " << m_value;
         }
@@ -111,12 +111,12 @@ namespace lp {
 namespace smt {
 
     typedef ptr_vector<lp::bound> lp_bounds;
-    
-    class theory_lra::imp {        
+
+    class theory_lra::imp {
 
         struct scope {
             unsigned m_bounds_lim;
-            unsigned m_asserted_qhead;            
+            unsigned m_asserted_qhead;
             unsigned m_asserted_atoms_lim;
             unsigned m_delayed_terms_lim;
             unsigned m_delayed_equalities_lim;
@@ -150,7 +150,7 @@ namespace smt {
         vector<rational>    m_columns;
         // temporary values kept during internalization
         struct internalize_state {
-            expr_ref_vector     m_terms;                     
+            expr_ref_vector     m_terms;
             vector<rational>    m_coeffs;
             svector<theory_var> m_vars;
             rational            m_coeff;
@@ -182,21 +182,21 @@ namespace smt {
         public:
             scoped_internalize_state(imp& i): m_imp(i), m_st(push_internalize(i)) {}
             ~scoped_internalize_state() { --m_imp.m_internalize_head; }
-            expr_ref_vector&     terms() { return m_st.m_terms; }                     
+            expr_ref_vector&     terms() { return m_st.m_terms; }
             vector<rational>&    coeffs() { return m_st.m_coeffs; }
             svector<theory_var>& vars() { return m_st.m_vars; }
             rational&            coeff() { return m_st.m_coeff; }
-            ptr_vector<expr>&    terms_to_internalize() { return m_st.m_terms_to_internalize; }            
+            ptr_vector<expr>&    terms_to_internalize() { return m_st.m_terms_to_internalize; }
             void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
-            void set_back(unsigned i) { 
+            void set_back(unsigned i) {
                 if (terms().size() == i + 1) return;
-                terms()[i] = terms().back(); 
+                terms()[i] = terms().back();
                 coeffs()[i] = coeffs().back();
                 terms().pop_back();
                 coeffs().pop_back();
             }
         };
-       
+
         typedef vector<std::pair<rational, lean::var_index>> var_coeffs;
         struct delayed_def {
             vector<rational>    m_coeffs;
@@ -208,8 +208,8 @@ namespace smt {
         };
 
         svector<lean::var_index> m_theory_var2var_index;   // translate from theory variables to lar vars
-        svector<theory_var>      m_var_index2theory_var;   // reverse map from lp_solver variables to theory variables  
-        svector<theory_var>      m_term_index2theory_var;   // reverse map from lp_solver variables to theory variables  
+        svector<theory_var>      m_var_index2theory_var;   // reverse map from lp_solver variables to theory variables
+        svector<theory_var>      m_term_index2theory_var;   // reverse map from lp_solver variables to theory variables
         var_coeffs               m_left_side;              // constraint left side
         mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
 
@@ -225,8 +225,8 @@ namespace smt {
         svector<theory_var>                           m_definitions;     // asserted rows corresponding to definitions
 
         bool                   m_delay_constraints;    // configuration
-        svector<delayed_atom>  m_asserted_atoms;        
-        app_ref_vector         m_delayed_terms;        
+        svector<delayed_atom>  m_asserted_atoms;
+        app_ref_vector         m_delayed_terms;
         svector<std::pair<theory_var, theory_var>> m_delayed_equalities;
         vector<delayed_def>    m_delayed_defs;
         expr*                  m_not_handled;
@@ -243,7 +243,7 @@ namespace smt {
 
         svector<unsigned>       m_to_check;    // rows that should be checked for theory propagation
 
-        svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates; 
+        svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates;
         unsigned                                          m_assume_eq_head;
 
         unsigned               m_num_conflicts;
@@ -264,7 +264,7 @@ namespace smt {
 
         svector<scope>         m_scopes;
         lp::stats              m_stats;
-        arith_factory*         m_factory;       
+        arith_factory*         m_factory;
         scoped_ptr<lean::lar_solver> m_solver;
         resource_limit         m_resource_limit;
         lp_bounds              m_new_bounds;
@@ -276,12 +276,12 @@ namespace smt {
         bool is_int(enode* n) const { return a.is_int(n->get_owner()); }
         enode* get_enode(theory_var v) const { return th.get_enode(v); }
         enode* get_enode(expr* e) const { return ctx().get_enode(e); }
-        expr*  get_owner(theory_var v) const { return get_enode(v)->get_owner(); }        
+        expr*  get_owner(theory_var v) const { return get_enode(v)->get_owner(); }
 
         void init_solver() {
             if (m_solver) return;
             lp_params lp(ctx().get_params());
-            m_solver = alloc(lean::lar_solver); 
+            m_solver = alloc(lean::lar_solver);
             m_theory_var2var_index.reset();
             m_solver->settings().set_resource_limit(m_resource_limit);
             m_solver->settings().simplex_strategy() = static_cast<lean::simplex_strategy_enum>(lp.simplex_strategy());
@@ -315,7 +315,7 @@ namespace smt {
                 }
                 if (a.is_to_real(term, term)) {
                     continue;
-                }                
+                }
                 return false;
             }
             while (false);
@@ -325,15 +325,15 @@ namespace smt {
         void linearize_term(expr* term, scoped_internalize_state& st) {
             st.push(term, rational::one());
             linearize(st);
-        } 
-        
+        }
+
         void linearize_ineq(expr* lhs, expr* rhs, scoped_internalize_state& st) {
             st.push(lhs, rational::one());
             st.push(rhs, rational::minus_one());
             linearize(st);
         }
-        
-        void linearize(scoped_internalize_state& st) { 
+
+        void linearize(scoped_internalize_state& st) {
             expr_ref_vector & terms = st.terms();
             svector<theory_var>& vars = st.vars();
             vector<rational>& coeffs = st.coeffs();
@@ -354,7 +354,7 @@ namespace smt {
                 }
                 else if (a.is_sub(n)) {
                     unsigned sz = to_app(n)->get_num_args();
-                    terms[index] = to_app(n)->get_arg(0);                    
+                    terms[index] = to_app(n)->get_arg(0);
                     for (unsigned i = 1; i < sz; ++i) {
                         st.push(to_app(n)->get_arg(i), -coeffs[index]);
                     }
@@ -423,7 +423,7 @@ namespace smt {
                 return get_enode(n);
             }
             else {
-                return ctx().mk_enode(n, !reflect(n), false, enable_cgc_for(n));       
+                return ctx().mk_enode(n, !reflect(n), false, enable_cgc_for(n));
             }
         }
 
@@ -459,12 +459,12 @@ namespace smt {
         }
 
         bool reflect(app* n) const {
-            return m_arith_params.m_arith_reflect || is_underspecified(n);          
+            return m_arith_params.m_arith_reflect || is_underspecified(n);
         }
 
         theory_var mk_var(expr* n, bool internalize = true) {
             if (!ctx().e_internalized(n)) {
-                ctx().internalize(n, false);                
+                ctx().internalize(n, false);
             }
             enode* e = get_enode(n);
             theory_var v;
@@ -478,12 +478,12 @@ namespace smt {
                 ctx().attach_th_var(e, &th, v);
             }
             else {
-                v = e->get_th_var(get_id());                
+                v = e->get_th_var(get_id());
             }
             SASSERT(null_theory_var != v);
             return v;
         }
-        
+
         lean::var_index get_var_index(theory_var v) {
             lean::var_index result = UINT_MAX;
             if (m_theory_var2var_index.size() > static_cast<unsigned>(v)) {
@@ -497,7 +497,7 @@ namespace smt {
             }
             return result;
         }
-        
+
         void init_left_side(scoped_internalize_state& st) {
             SASSERT(all_zeros(m_columns));
             svector<theory_var> const& vars = st.vars();
@@ -510,7 +510,7 @@ namespace smt {
                 }
                 else {
                     m_columns[var] += coeff;
-                }                
+                }
             }
             m_left_side.clear();
             // reset the coefficients after they have been used.
@@ -519,12 +519,12 @@ namespace smt {
                 rational const& r = m_columns[var];
                 if (!r.is_zero()) {
                     m_left_side.push_back(std::make_pair(r, get_var_index(var)));
-                    m_columns[var].reset();                    
+                    m_columns[var].reset();
                 }
             }
             SASSERT(all_zeros(m_columns));
         }
-        
+
         bool all_zeros(vector<rational> const& v) const {
             for (unsigned i = 0; i < v.size(); ++i) {
                 if (!v[i].is_zero()) {
@@ -533,20 +533,20 @@ namespace smt {
             }
             return true;
         }
-        
+
         void add_eq_constraint(lean::constraint_index index, enode* n1, enode* n2) {
             m_constraint_sources.setx(index, equality_source, null_source);
             m_equalities.setx(index, enode_pair(n1, n2), enode_pair(0, 0));
             ++m_stats.m_add_rows;
         }
-        
+
         void add_ineq_constraint(lean::constraint_index index, literal lit) {
             m_constraint_sources.setx(index, inequality_source, null_source);
             m_inequalities.setx(index, lit, null_literal);
             ++m_stats.m_add_rows;
             TRACE("arith", m_solver->print_constraint(index, tout); tout << "\n";);
         }
-        
+
         void add_def_constraint(lean::constraint_index index, theory_var v) {
             m_constraint_sources.setx(index, definition_source, null_source);
             m_definitions.setx(index, v, null_theory_var);
@@ -556,12 +556,12 @@ namespace smt {
         void internalize_eq(delayed_def const& d) {
             scoped_internalize_state st(*this);
             st.vars().append(d.m_vars);
-            st.coeffs().append(d.m_coeffs);            
+            st.coeffs().append(d.m_coeffs);
             init_left_side(st);
             add_def_constraint(m_solver->add_constraint(m_left_side, lean::EQ, -d.m_coeff), d.m_var);
         }
-        
-        void internalize_eq(theory_var v1, theory_var v2) {                  
+
+        void internalize_eq(theory_var v1, theory_var v2) {
             enode* n1 = get_enode(v1);
             enode* n2 = get_enode(v2);
             scoped_internalize_state st(*this);
@@ -571,7 +571,7 @@ namespace smt {
             st.coeffs().push_back(rational::minus_one());
             init_left_side(st);
             add_eq_constraint(m_solver->add_constraint(m_left_side, lean::EQ, rational::zero()), n1, n2);
-            TRACE("arith", 
+            TRACE("arith",
                   tout << "v" << v1 << " = " << "v" << v2 << ": "
                   << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";);
         }
@@ -583,7 +583,7 @@ namespace smt {
                 lp::bound* b = m_bounds[v].back();
                 // del_use_lists(b);
                 dealloc(b);
-                m_bounds[v].pop_back();                        
+                m_bounds[v].pop_back();
             }
             m_bounds_trail.shrink(old_size);
         }
@@ -591,9 +591,9 @@ namespace smt {
         void updt_unassigned_bounds(theory_var v, int inc) {
             TRACE("arith", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
             ctx().push_trail(vector_value_trail<smt::context, unsigned, false>(m_unassigned_bounds, v));
-            m_unassigned_bounds[v] += inc;            
+            m_unassigned_bounds[v] += inc;
         }
-       
+
         bool is_unit_var(scoped_internalize_state& st) {
             return st.coeff().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one();
         }
@@ -644,26 +644,26 @@ namespace smt {
                 return v;
             }
         }
-        
+
 
     public:
-        imp(theory_lra& th, ast_manager& m, theory_arith_params& ap): 
-            th(th), m(m), 
-            m_arith_params(ap), 
-            a(m), 
-            m_arith_eq_adapter(th, ap, a),            
+        imp(theory_lra& th, ast_manager& m, theory_arith_params& ap):
+            th(th), m(m),
+            m_arith_params(ap),
+            a(m),
+            m_arith_eq_adapter(th, ap, a),
             m_internalize_head(0),
-            m_delay_constraints(false), 
+            m_delay_constraints(false),
             m_delayed_terms(m),
             m_not_handled(0),
-            m_asserted_qhead(0), 
+            m_asserted_qhead(0),
             m_assume_eq_head(0),
             m_num_conflicts(0),
             m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
             m_solver(0),
             m_resource_limit(*this) {
         }
-        
+
         ~imp() {
             del_bounds(0);
             std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc<internalize_state>());
@@ -672,7 +672,7 @@ namespace smt {
         void init(context* ctx) {
             init_solver();
         }
-        
+
         bool internalize_atom(app * atom, bool gate_ctx) {
             if (m_delay_constraints) {
                 return internalize_atom_lazy(atom, gate_ctx);
@@ -697,7 +697,7 @@ namespace smt {
             else if (a.is_ge(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
                 v = internalize_def(to_app(n1));
                 k = lp::lower_t;
-            }    
+            }
             else {
                 TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
                 found_not_handled(atom);
@@ -730,7 +730,7 @@ namespace smt {
             else if (a.is_ge(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
                 v = internalize_def(to_app(n1), st);
                 k = lp::lower_t;
-            }    
+            }
             else {
                 TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
                 found_not_handled(atom);
@@ -743,11 +743,11 @@ namespace smt {
             m_bool_var2bound.insert(bv, b);
             TRACE("arith", tout << "Internalized " << mk_pp(atom, m) << "\n";);
             if (!is_unit_var(st) && m_bounds[v].size() == 1) {
-                m_delayed_defs.push_back(delayed_def(st.vars(), st.coeffs(), st.coeff(), v)); 
+                m_delayed_defs.push_back(delayed_def(st.vars(), st.coeffs(), st.coeff(), v));
             }
             return true;
         }
-        
+
         bool internalize_term(app * term) {
             if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) {
                 // skip
@@ -766,7 +766,7 @@ namespace smt {
             }
             return true;
         }
-        
+
         void internalize_eq_eh(app * atom, bool_var) {
             expr* lhs = 0, *rhs = 0;
             VERIFY(m.is_eq(atom, lhs, rhs));
@@ -845,7 +845,7 @@ namespace smt {
             m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim);
             m_var_trail.shrink(m_scopes[old_size].m_var_trail_lim);
             m_not_handled = m_scopes[old_size].m_not_handled;
-            m_scopes.resize(old_size);            
+            m_scopes.resize(old_size);
             if (!m_delay_constraints) m_solver->pop(num_scopes);
             // VERIFY(l_false != make_feasible());
             m_new_bounds.reset();
@@ -860,16 +860,16 @@ namespace smt {
         void relevant_eh(app* n) {
             TRACE("arith", tout << mk_pp(n, m) << "\n";);
             expr* n1, *n2;
-            if (a.is_mod(n, n1, n2)) 
+            if (a.is_mod(n, n1, n2))
                 mk_idiv_mod_axioms(n1, n2);
             else if (a.is_rem(n, n1, n2))
                 mk_rem_axiom(n1, n2);
-            else if (a.is_div(n, n1, n2)) 
+            else if (a.is_div(n, n1, n2))
                 mk_div_axiom(n1, n2);
-            else if (a.is_to_int(n)) 
+            else if (a.is_to_int(n))
                 mk_to_int_axiom(n);
             else if (a.is_is_int(n))
-                mk_is_int_axiom(n);            
+                mk_is_int_axiom(n);
         }
 
         //  n < 0 || rem(a, n) =  mod(a, n)
@@ -881,7 +881,7 @@ namespace smt {
             expr_ref mmod(a.mk_uminus(mod), m);
             literal dgez = mk_literal(a.mk_ge(divisor, zero));
             mk_axiom(~dgez, th.mk_eq(rem, mod,  false));
-            mk_axiom( dgez, th.mk_eq(rem, mmod, false));                    
+            mk_axiom( dgez, th.mk_eq(rem, mmod, false));
         }
 
         // q = 0 or q * (p div q) = p
@@ -896,7 +896,7 @@ namespace smt {
         // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
         void mk_to_int_axiom(app* n) {
             expr* x = 0, *y = 0;
-            VERIFY (a.is_to_int(n, x));            
+            VERIFY (a.is_to_int(n, x));
             if (a.is_to_real(x, y)) {
                 mk_axiom(th.mk_eq(y, n, false));
             }
@@ -945,7 +945,7 @@ namespace smt {
             mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
             mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
             rational k;
-            if (m_arith_params.m_arith_enum_const_mod && a.is_numeral(q, k) && 
+            if (m_arith_params.m_arith_enum_const_mod && a.is_numeral(q, k) &&
                 k.is_pos() && k < rational(8)) {
                 unsigned _k = k.get_unsigned();
                 literal_buffer lits;
@@ -954,8 +954,8 @@ namespace smt {
                     lits.push_back(mod_j);
                     ctx().mark_as_relevant(mod_j);
                 }
-                ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());                
-            }            
+                ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());
+            }
         }
 
         void mk_axiom(literal l) {
@@ -1006,14 +1006,14 @@ namespace smt {
         }
 
         bool can_get_value(theory_var v) const {
-            return 
+            return
                 (v != null_theory_var) &&
-                (v < static_cast<theory_var>(m_theory_var2var_index.size())) && 
-                (UINT_MAX != m_theory_var2var_index[v]) && 
+                (v < static_cast<theory_var>(m_theory_var2var_index.size())) &&
+                (UINT_MAX != m_theory_var2var_index[v]) &&
                 (m_solver->is_term(m_theory_var2var_index[v]) || m_variable_values.count(m_theory_var2var_index[v]) > 0);
         }
 
-        
+
         bool can_get_ivalue(theory_var v) const {
             if (v == null_theory_var || (v >= static_cast<theory_var>(m_theory_var2var_index.size())))
                 return false;
@@ -1034,7 +1034,7 @@ namespace smt {
             return result;
         }
 
-        
+
         rational get_value(theory_var v) const {
             if (!can_get_value(v)) return rational::zero();
             lean::var_index vi = m_theory_var2var_index[v];
@@ -1051,7 +1051,7 @@ namespace smt {
                 return result;
             }
             UNREACHABLE();
-            return m_variable_values[vi];        
+            return m_variable_values[vi];
         }
 
         void init_variable_values() {
@@ -1064,20 +1064,20 @@ namespace smt {
             m_variable_values.clear();
         }
 
-        bool assume_eqs() {        
+        bool assume_eqs() {
             svector<lean::var_index> vars;
             theory_var sz = static_cast<theory_var>(th.get_num_vars());
             for (theory_var v = 0; v < sz; ++v) {
-                if (th.is_relevant_and_shared(get_enode(v))) { 
+                if (th.is_relevant_and_shared(get_enode(v))) {
                     vars.push_back(m_theory_var2var_index[v]);
                 }
             }
             if (vars.empty()) {
                 return false;
             }
-            TRACE("arith", 
+            TRACE("arith",
                   for (theory_var v = 0; v < sz; ++v) {
-                      if (th.is_relevant_and_shared(get_enode(v))) { 
+                      if (th.is_relevant_and_shared(get_enode(v))) {
                           tout << "v" << v << " " << m_theory_var2var_index[v] << " ";
                       }
                   }
@@ -1086,14 +1086,14 @@ namespace smt {
             m_solver->random_update(vars.size(), vars.c_ptr());
             m_model_eqs.reset();
             TRACE("arith", display(tout););
-            
+
             unsigned old_sz = m_assume_eq_candidates.size();
             bool result = false;
             int start = ctx().get_random_value();
             for (theory_var i = 0; i < sz; ++i) {
                 theory_var v = (i + start) % sz;
                 enode* n1 = get_enode(v);
-                if (!th.is_relevant_and_shared(n1)) {                    
+                if (!th.is_relevant_and_shared(n1)) {
                     continue;
                 }
                 if (!can_get_ivalue(v)) {
@@ -1112,7 +1112,7 @@ namespace smt {
                     result = true;
                 }
             }
-            
+
             if (result) {
                 ctx().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
             }
@@ -1123,7 +1123,7 @@ namespace smt {
         bool delayed_assume_eqs() {
             if (m_assume_eq_head == m_assume_eq_candidates.size())
                 return false;
-            
+
             ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head));
             while (m_assume_eq_head < m_assume_eq_candidates.size()) {
                 std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
@@ -1132,7 +1132,7 @@ namespace smt {
                 enode* n1 = get_enode(v1);
                 enode* n2 = get_enode(v2);
                 m_assume_eq_head++;
-                CTRACE("arith", 
+                CTRACE("arith",
                        get_ivalue(v1) == get_ivalue(v2) && n1->get_root() != n2->get_root(),
                        tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";);
                 if (get_ivalue(v1) == get_ivalue(v2) &&  n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) {
@@ -1177,7 +1177,7 @@ namespace smt {
                 if (assume_eqs()) {
                     return FC_CONTINUE;
                 }
-                if (m_not_handled != 0) {                    
+                if (m_not_handled != 0) {
                     return FC_GIVEUP;
                 }
                 return FC_DONE;
@@ -1201,7 +1201,7 @@ namespace smt {
            Thus, 'a' must be considered a shared var if it is the child of an underspecified operator.
 
            if merge(a / b, x + y) and a / b is root, then x + y become shared and all z + u in equivalence class of x + y.
-                      
+
 
            TBD: when the set of underspecified subterms is small, compute the shared variables below it.
                 Recompute the set if there are merges that invalidate it.
@@ -1256,7 +1256,7 @@ namespace smt {
             while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent()) {
                 bool_var bv  = m_asserted_atoms[m_asserted_qhead].m_bv;
                 bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
-                
+
 #if 1
                 m_to_check.push_back(bv);
 #else
@@ -1281,7 +1281,7 @@ namespace smt {
             }*/
 
             lbool lbl = make_feasible();
-            
+
             switch(lbl) {
             case l_false:
                 TRACE("arith", tout << "propagation conflict\n";);
@@ -1294,7 +1294,7 @@ namespace smt {
             case l_undef:
                 break;
             }
-            
+
         }
 
         void propagate_bounds_with_lp_solver() {
@@ -1351,9 +1351,9 @@ namespace smt {
             return false;
         }
 
-        struct local_bound_propagator: public lean::bound_propagator {
+        struct local_bound_propagator: public lean::lp_bound_propagator {
             imp & m_imp;
-            local_bound_propagator(imp& i) : bound_propagator(*i.m_solver), m_imp(i) {}
+            local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {}
 
             bool bound_is_interesting(unsigned j, lean::lconstraint_kind kind, const rational & v) {
                 return m_imp.bound_is_interesting(j, kind, v);
@@ -1364,7 +1364,7 @@ namespace smt {
             }
         };
 
-        
+
         void propagate_lp_solver_bound(lean::implied_bound& be) {
 
             theory_var v;
@@ -1381,7 +1381,7 @@ namespace smt {
                   // if (m_unassigned_bounds[v] == 0) m_solver->print_bound_evidence(be, tout);
                   );
 
-            
+
             if (m_unassigned_bounds[v] == 0 || m_bounds.size() <= static_cast<unsigned>(v)) {
                 TRACE("arith", tout << "return\n";);
                 return;
@@ -1447,18 +1447,18 @@ namespace smt {
                 ctx().assign(
                     lit, ctx().mk_justification(
                         ext_theory_propagation_justification(
-                            get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), 
-                            m_eqs.size(), m_eqs.c_ptr(), lit, m_params.size(), m_params.c_ptr())));            
+                            get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(),
+                            m_eqs.size(), m_eqs.c_ptr(), lit, m_params.size(), m_params.c_ptr())));
             }
         }
 
         literal is_bound_implied(lean::lconstraint_kind k, rational const& value, lp::bound const& b) const {
             if ((k == lean::LE || k == lean::LT) && b.get_bound_kind() == lp::upper_t && value <= b.get_value()) {
-                // v <= value <= b.get_value() => v <= b.get_value() 
+                // v <= value <= b.get_value() => v <= b.get_value()
                 return literal(b.get_bv(), false);
             }
             if ((k == lean::GE || k == lean::GT) && b.get_bound_kind() == lp::lower_t && b.get_value() <= value) {
-                // b.get_value() <= value <= v => b.get_value() <= v 
+                // b.get_value() <= value <= v => b.get_value() <= v
                 return literal(b.get_bv(), false);
             }
             if (k == lean::LE && b.get_bound_kind() == lp::lower_t && value < b.get_value()) {
@@ -1484,8 +1484,8 @@ namespace smt {
         void mk_bound_axioms(lp::bound& b) {
             if (!ctx().is_searching()) {
                 //
-                // NB. We make an assumption that user push calls propagation 
-                // before internal scopes are pushed. This flushes all newly 
+                // NB. We make an assumption that user push calls propagation
+                // before internal scopes are pushed. This flushes all newly
                 // asserted atoms into the right context.
                 //
                 m_new_bounds.push_back(&b);
@@ -1499,7 +1499,7 @@ namespace smt {
             lp::bound* end = 0;
             lp::bound* lo_inf = end, *lo_sup = end;
             lp::bound* hi_inf = end, *hi_sup = end;
-            
+
             for (unsigned i = 0; i < bounds.size(); ++i) {
                 lp::bound& other = *bounds[i];
                 if (&other == &b) continue;
@@ -1530,7 +1530,7 @@ namespace smt {
                 else if (hi_sup == end || k2 < hi_sup->get_value()) {
                     hi_sup = &other;
                 }
-            }        
+            }
             if (lo_inf != end) mk_bound_axiom(b, *lo_inf);
             if (lo_sup != end) mk_bound_axiom(b, *lo_sup);
             if (hi_inf != end) mk_bound_axiom(b, *hi_inf);
@@ -1550,9 +1550,9 @@ namespace smt {
             SASSERT(v == b2.get_var());
             if (k1 == k2 && kind1 == kind2) return;
             SASSERT(k1 != k2 || kind1 != kind2);
-            parameter coeffs[3] = { parameter(symbol("farkas")), 
+            parameter coeffs[3] = { parameter(symbol("farkas")),
                                     parameter(rational(1)), parameter(rational(1)) };
-            
+
             if (kind1 == lp::lower_t) {
                 if (kind2 == lp::lower_t) {
                     if (k2 <= k1) {
@@ -1582,12 +1582,12 @@ namespace smt {
                 }
                 else {
                     // k1 < k2, k2 <= x => ~(x <= k1)
-                    mk_clause(~l1, ~l2, 3, coeffs); 
+                    mk_clause(~l1, ~l2, 3, coeffs);
                     if (v_is_int && k1 == k2 - rational(1)) {
                         // x <= k1 or k1+l <= x
                         mk_clause(l1, l2, 3, coeffs);
                     }
-                    
+
                 }
             }
             else {
@@ -1600,7 +1600,7 @@ namespace smt {
                     // k1 <= hi_sup , x <= k1 =>  x <= hi_sup
                     mk_clause(~l1, l2, 3, coeffs);
                 }
-            }        
+            }
         }
 
         typedef lp_bounds::iterator iterator;
@@ -1609,7 +1609,7 @@ namespace smt {
             CTRACE("arith", !m_new_bounds.empty(), tout << "flush bound axioms\n";);
 
             while (!m_new_bounds.empty()) {
-                lp_bounds atoms;            
+                lp_bounds atoms;
                 atoms.push_back(m_new_bounds.back());
                 m_new_bounds.pop_back();
                 theory_var v = atoms.back()->get_var();
@@ -1620,22 +1620,22 @@ namespace smt {
                         m_new_bounds.pop_back();
                         --i;
                     }
-                }            
-                CTRACE("arith_verbose", !atoms.empty(),  
+                }
+                CTRACE("arith_verbose", !atoms.empty(),
                        for (unsigned i = 0; i < atoms.size(); ++i) {
                            atoms[i]->display(tout); tout << "\n";
                        });
                 lp_bounds occs(m_bounds[v]);
-                
+
                 std::sort(atoms.begin(), atoms.end(), compare_bounds());
                 std::sort(occs.begin(), occs.end(), compare_bounds());
-                
+
                 iterator begin1 = occs.begin();
                 iterator begin2 = occs.begin();
                 iterator end = occs.end();
                 begin1 = first(lp::lower_t, begin1, end);
                 begin2 = first(lp::upper_t, begin2, end);
-                
+
                 iterator lo_inf = begin1, lo_sup = begin1;
                 iterator hi_inf = begin2, hi_sup = begin2;
                 iterator lo_inf1 = begin1, lo_sup1 = begin1;
@@ -1648,10 +1648,10 @@ namespace smt {
                     hi_inf1 = next_inf(a1, lp::upper_t, hi_inf, end, fhi_inf);
                     lo_sup1 = next_sup(a1, lp::lower_t, lo_sup, end, flo_sup);
                     hi_sup1 = next_sup(a1, lp::upper_t, hi_sup, end, fhi_sup);
-                    if (lo_inf1 != end) lo_inf = lo_inf1; 
-                    if (lo_sup1 != end) lo_sup = lo_sup1; 
-                    if (hi_inf1 != end) hi_inf = hi_inf1; 
-                    if (hi_sup1 != end) hi_sup = hi_sup1; 
+                    if (lo_inf1 != end) lo_inf = lo_inf1;
+                    if (lo_sup1 != end) lo_sup = lo_sup1;
+                    if (hi_inf1 != end) hi_inf = hi_inf1;
+                    if (hi_sup1 != end) hi_sup = hi_sup1;
                     if (!flo_inf) lo_inf = end;
                     if (!fhi_inf) hi_inf = end;
                     if (!flo_sup) lo_sup = end;
@@ -1661,7 +1661,7 @@ namespace smt {
                     if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(*a1, **lo_sup);
                     if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(*a1, **hi_inf);
                     if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(*a1, **hi_sup);
-                }                            
+                }
             }
         }
 
@@ -1671,8 +1671,8 @@ namespace smt {
 
 
         lp_bounds::iterator first(
-            lp::bound_kind kind, 
-            iterator it, 
+            lp::bound_kind kind,
+            iterator it,
             iterator end) {
             for (; it != end; ++it) {
                 lp::bound* a = *it;
@@ -1682,16 +1682,16 @@ namespace smt {
         }
 
         lp_bounds::iterator next_inf(
-            lp::bound* a1, 
-            lp::bound_kind kind, 
-            iterator it, 
+            lp::bound* a1,
+            lp::bound_kind kind,
+            iterator it,
             iterator end,
             bool& found_compatible) {
             rational const & k1(a1->get_value());
             iterator result = end;
             found_compatible = false;
             for (; it != end; ++it) {
-                lp::bound * a2 = *it;            
+                lp::bound * a2 = *it;
                 if (a1 == a2) continue;
                 if (a2->get_bound_kind() != kind) continue;
                 rational const & k2(a2->get_value());
@@ -1707,15 +1707,15 @@ namespace smt {
         }
 
         lp_bounds::iterator next_sup(
-            lp::bound* a1, 
-            lp::bound_kind kind, 
-            iterator it, 
+            lp::bound* a1,
+            lp::bound_kind kind,
+            iterator it,
             iterator end,
             bool& found_compatible) {
             rational const & k1(a1->get_value());
             found_compatible = false;
             for (; it != end; ++it) {
-                lp::bound * a2 = *it;            
+                lp::bound * a2 = *it;
                 if (a1 == a2) continue;
                 if (a2->get_bound_kind() != kind) continue;
                 rational const & k2(a2->get_value());
@@ -1728,7 +1728,7 @@ namespace smt {
         }
 
         void propagate_basic_bounds() {
-            for (auto const& bv : m_to_check) {                
+            for (auto const& bv : m_to_check) {
                 lp::bound& b = *m_bool_var2bound.find(bv);
                 propagate_bound(bv, ctx().get_assignment(bv) == l_true, b);
                 if (ctx().inconsistent()) break;
@@ -1736,9 +1736,9 @@ namespace smt {
             }
             m_to_check.reset();
         }
-        
+
         // for glb lo': lo' < lo:
-        //   lo <= x -> lo' <= x 
+        //   lo <= x -> lo' <= x
         //   lo <= x -> ~(x <= lo')
         // for lub hi': hi' > hi
         //   x <= hi -> x <= hi'
@@ -1773,7 +1773,7 @@ namespace smt {
                 }
                 if (!lb) return;
                 bool sign = lb->get_bound_kind() != lp::lower_t;
-                lit2 = literal(lb->get_bv(), sign);                    
+                lit2 = literal(lb->get_bv(), sign);
             }
             else {
                 rational lub;
@@ -1791,7 +1791,7 @@ namespace smt {
                 bool sign = ub->get_bound_kind() != lp::upper_t;
                 lit2 = literal(ub->get_bv(), sign);
             }
-            TRACE("arith", 
+            TRACE("arith",
                   ctx().display_literal_verbose(tout, lit1);
                   ctx().display_literal_verbose(tout << " => ", lit2);
                   tout << "\n";);
@@ -1841,7 +1841,7 @@ namespace smt {
         // The idea is that if bounds on all variables in an inequality ax + by + cz >= k
         // have been assigned we may know the truth value of the inequality by using simple
         // bounds propagation.
-        // 
+        //
         void propagate_bound_compound(bool_var bv, bool is_true, lp::bound& b) {
             theory_var v = b.get_var();
             TRACE("arith", tout << mk_pp(get_owner(v), m) << "\n";);
@@ -1866,15 +1866,15 @@ namespace smt {
                         lit = literal(vb->get_bv(), true);
                     }
                 }
-                else {                     
+                else {
                     if (get_glb(*vb, r) && r > vb->get_value()) {         // VB <= value < val(VB)
                         lit = literal(vb->get_bv(), true);
                     }
                     else if (get_lub(*vb, r) && r <= vb->get_value()) {   // val(VB) <= value
                         lit = literal(vb->get_bv(), false);
                     }
-                }                
-                
+                }
+
                 if (lit != null_literal) {
                     TRACE("arith",
                           ctx().display_literals_verbose(tout, m_core);
@@ -1882,7 +1882,7 @@ namespace smt {
                           ctx().display_literal_verbose(tout, lit);
                           tout << "\n";
                           );
-                
+
 
                     assign(lit);
                 }
@@ -1934,9 +1934,9 @@ namespace smt {
                     if (is_strict) {
                         r += inf_rational(rational::zero(), coeff.second.is_pos());
                     }
-                }                
+                }
                 r += value * coeff.second;
-                set_evidence(ci);                    
+                set_evidence(ci);
             }
             TRACE("arith_verbose", tout << (is_lub?"lub":"glb") << " is " << r << "\n";);
             return true;
@@ -1958,7 +1958,7 @@ namespace smt {
             case lp::upper_t:
                 k = is_true ? lean::LE : lean::GT;
                 break;
-            }         
+            }
             if (k == lean::LT || k == lean::LE) {
                 ++m_stats.m_assert_lower;
             }
@@ -1978,7 +1978,7 @@ namespace smt {
         // A fixed equality is inferred if there are two variables v1, v2 whose
         // upper and lower bounds coincide.
         // Then the equality v1 == v2 is propagated to the core.
-        // 
+        //
 
         typedef std::pair<lean::constraint_index, rational> constraint_bound;
         vector<constraint_bound>        m_lower_terms;
@@ -2043,11 +2043,11 @@ namespace smt {
         bool has_upper_bound(lean::var_index vi, lean::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
 
         bool has_lower_bound(lean::var_index vi, lean::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
-       
+
         bool has_bound(lean::var_index vi, lean::constraint_index& ci, rational const& bound, bool is_lower) {
 
             if (m_solver->is_term(vi)) {
-                
+
                 lean::var_index ti = m_solver->adjust_term_index(vi);
                 theory_var v = m_term_index2theory_var.get(ti, null_theory_var);
                 rational val;
@@ -2105,7 +2105,7 @@ namespace smt {
                         set_evidence(ci4);
                         enode* x = get_enode(v1);
                         enode* y = get_enode(v2);
-                        justification* js = 
+                        justification* js =
                             ctx().mk_justification(
                                 ext_theory_eq_propagation_justification(
                                     get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, 0));
@@ -2114,10 +2114,10 @@ namespace smt {
                               for (unsigned i = 0; i <  m_core.size(); ++i) {
                                   ctx().display_detailed_literal(tout, m_core[i]);
                                   tout << "\n";
-                              } 
+                              }
                               for (unsigned i = 0; i < m_eqs.size(); ++i) {
                                   tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
-                              } 
+                              }
                               tout << " ==> ";
                               tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
                               );
@@ -2158,15 +2158,15 @@ namespace smt {
                 //                SASSERT(m_solver->all_constraints_hold());
                 return l_true;
             case lean::lp_status::TIME_EXHAUSTED:
-                
+
             default:
                 TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
-                // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, 
+                // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED,
                 // FLOATING_POINT_ERROR, TIME_EXAUSTED, ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE
                 return l_undef;
             }
         }
- 
+
         vector<std::pair<rational, lean::constraint_index>> m_explanation;
         literal_vector      m_core;
         svector<enode_pair> m_eqs;
@@ -2188,7 +2188,7 @@ namespace smt {
             case equality_source: {
                 SASSERT(m_equalities[idx].first  != nullptr);
                     SASSERT(m_equalities[idx].second != nullptr);
-                    m_eqs.push_back(m_equalities[idx]);          
+                    m_eqs.push_back(m_equalities[idx]);
                     break;
             }
             case definition_source: {
@@ -2219,7 +2219,7 @@ namespace smt {
             TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
             TRACE("arith", display(tout););
             for (auto const& ev : m_explanation) {
-                if (!ev.first.is_zero()) { 
+                if (!ev.first.is_zero()) {
                     set_evidence(ev.second);
                 }
             }
@@ -2227,8 +2227,8 @@ namespace smt {
             ctx().set_conflict(
                 ctx().mk_justification(
                     ext_theory_conflict_justification(
-                        get_id(), ctx().get_region(), 
-                        m_core.size(), m_core.c_ptr(), 
+                        get_id(), ctx().get_region(),
+                        m_core.size(), m_core.c_ptr(),
                         m_eqs.size(), m_eqs.c_ptr(), m_params.size(), m_params.c_ptr())));
         }
 
@@ -2261,7 +2261,7 @@ namespace smt {
         }
 
         bool get_value(enode* n, expr_ref& r) {
-            theory_var v = n->get_th_var(get_id());            
+            theory_var v = n->get_th_var(get_id());
             if (can_get_value(v)) {
                 r = a.mk_numeral(get_value(v), is_int(n));
                 return true;
@@ -2269,7 +2269,7 @@ namespace smt {
             else {
                 return false;
             }
-        }    
+        }
 
         bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
             SASSERT(v1 != null_theory_var);
@@ -2287,12 +2287,12 @@ namespace smt {
             add_background(nctx);
             bool result = l_true != nctx.check();
             CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
-                   display(tout););   
+                   display(tout););
             return result;
         }
 
         bool validate_assign(literal lit) {
-            if (dump_lemmas()) {                
+            if (dump_lemmas()) {
                 ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
             }
             context nctx(m, ctx().get_fparams(), ctx().get_params());
@@ -2301,7 +2301,7 @@ namespace smt {
             m_core.pop_back();
             bool result = l_true != nctx.check();
             CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
-                   display(tout););   
+                   display(tout););
             return result;
         }
 
@@ -2321,7 +2321,7 @@ namespace smt {
             for (unsigned i = 0; i < m_eqs.size(); ++i) {
                 nctx.assert_expr(m.mk_eq(m_eqs[i].first->get_owner(), m_eqs[i].second->get_owner()));
             }
-        }        
+        }
 
         theory_lra::inf_eps value(theory_var v) {
             lean::impq ival = get_ivalue(v);
@@ -2392,7 +2392,7 @@ namespace smt {
         app_ref mk_obj(theory_var v) {
             lean::var_index vi = m_theory_var2var_index[v];
             bool is_int = a.is_int(get_enode(v)->get_owner());
-            if (m_solver->is_term(vi)) {                
+            if (m_solver->is_term(vi)) {
                 expr_ref_vector args(m);
                 const lean::lar_term& term = m_solver->get_term(vi);
                 for (auto & ti : term.m_coeffs) {
@@ -2440,7 +2440,7 @@ namespace smt {
             }
             TRACE("arith", tout << b << "\n";);
             return expr_ref(b, m);
-            
+
         }
 
 
@@ -2452,9 +2452,9 @@ namespace smt {
             unsigned nv = th.get_num_vars();
             for (unsigned v = 0; v < nv; ++v) {
                 out << "v" << v;
-                if (can_get_value(v)) out << ", value: " << get_value(v);                
-                out << ", shared: " << ctx().is_shared(get_enode(v)) 
-                    << ", rel: " << ctx().is_relevant(get_enode(v)) 
+                if (can_get_value(v)) out << ", value: " << get_value(v);
+                out << ", shared: " << ctx().is_shared(get_enode(v))
+                    << ", rel: " << ctx().is_relevant(get_enode(v))
                     << ", def: "; th.display_var_flat_def(out, v) << "\n";
             }
         }
@@ -2462,8 +2462,8 @@ namespace smt {
         void display_evidence(std::ostream& out, vector<std::pair<rational, lean::constraint_index>> const& evidence) {
             for (auto const& ev : evidence) {
                 expr_ref e(m);
-                SASSERT(!ev.first.is_zero()); 
-                if (ev.first.is_zero()) { 
+                SASSERT(!ev.first.is_zero());
+                if (ev.first.is_zero()) {
                     continue;
                 }
                 unsigned idx = ev.second;
@@ -2474,23 +2474,23 @@ namespace smt {
                     out << e << " " << ctx().get_assignment(lit) << "\n";
                     break;
                 }
-                case equality_source: 
-                    out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = " 
-                        << mk_pp(m_equalities[idx].second->get_owner(), m) << "\n"; 
+                case equality_source:
+                    out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = "
+                        << mk_pp(m_equalities[idx].second->get_owner(), m) << "\n";
                     break;
                 case definition_source: {
                     theory_var v = m_definitions[idx];
                     out << "def: v" << v << " := " << mk_pp(th.get_enode(v)->get_owner(), m) << "\n";
                     break;
                 }
-                case null_source:                    
+                case null_source:
                 default:
                     UNREACHABLE();
-                    break; 
+                    break;
                 }
             }
             for (auto const& ev : evidence) {
-                m_solver->print_constraint(ev.second, out << ev.first << ": "); 
+                m_solver->print_constraint(ev.second, out << ev.first << ": ");
             }
         }
 
@@ -2512,16 +2512,16 @@ namespace smt {
             st.update("arith-make-feasible", m_stats.m_make_feasible);
             st.update("arith-max-columns", m_stats.m_max_cols);
             st.update("arith-max-rows", m_stats.m_max_rows);
-        }        
+        }
     };
-    
+
     theory_lra::theory_lra(ast_manager& m, theory_arith_params& ap):
         theory(m.get_family_id("arith")) {
         m_imp = alloc(imp, *this, m, ap);
-    }    
+    }
     theory_lra::~theory_lra() {
         dealloc(m_imp);
-    }   
+    }
     theory* theory_lra::mk_fresh(context* new_ctx) {
         return alloc(theory_lra, new_ctx->get_manager(), new_ctx->get_fparams());
     }
diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h
index add25d389..4c6c43464 100644
--- a/src/util/lp/bound_analyzer_on_row.h
+++ b/src/util/lp/bound_analyzer_on_row.h
@@ -16,9 +16,9 @@
 namespace lean {
 
 class bound_analyzer_on_row {
-    
+
     linear_combination_iterator<mpq> & m_it;
-    bound_propagator &                 m_bp;
+    lp_bound_propagator &                 m_bp;
     unsigned           m_row_or_term_index;
     int                m_column_of_u; // index of an unlimited from above monoid
                                // -1 means that such a value is not found, -2 means that at least two of such monoids were found
@@ -31,7 +31,7 @@ public :
                           linear_combination_iterator<mpq> &it,
                           const numeric_pair<mpq>& rs,
                           unsigned row_or_term_index,
-                          bound_propagator & bp
+                          lp_bound_propagator & bp
                           )
         :
         m_it(it),
@@ -45,7 +45,7 @@ public :
 
     unsigned j;
     void analyze() {
-        
+
         mpq a; unsigned j;
         while (((m_column_of_l != -2) || (m_column_of_u != -2)) && m_it.next(a, j))
             analyze_bound_on_var_on_coeff(j, a);
@@ -136,7 +136,7 @@ public :
             strict = !is_zero(ub(j).y);
             return a * ub(j).x;
         }
-        
+
         strict = !is_zero(lb(j).y);
         return a * lb(j).x;
     }
@@ -145,10 +145,10 @@ public :
         if (is_neg(a)) {
             return a * ub(j).x;
         }
-        
+
         return a * lb(j).x;
     }
-    
+
 
     void limit_all_monoids_from_above() {
         int strict = 0;
@@ -194,7 +194,7 @@ public :
             bool str;
 			bool a_is_pos = is_pos(a);
 			mpq bound = total / a + monoid_max_no_mult(a_is_pos, j, str);
-            bool astrict = strict - static_cast<int>(str) > 0; 
+            bool astrict = strict - static_cast<int>(str) > 0;
             if (a_is_pos) {
                 limit_j(j, bound, true, true, astrict);
             }
@@ -204,7 +204,7 @@ public :
         }
     }
 
-    
+
     void limit_monoid_u_from_below() {
         // we are going to limit from below the monoid m_column_of_u,
         // every other monoid is impossible to limit from below
@@ -225,7 +225,7 @@ public :
         }
 
         bound /= u_coeff;
-        
+
         if (numeric_traits<impq>::is_pos(u_coeff)) {
             limit_j(m_column_of_u, bound, true, true, strict);
         } else {
@@ -260,7 +260,7 @@ public :
             limit_j(m_column_of_l, bound, false, true, strict);
         }
     }
-    
+
     // // it is the coefficent before the bounded column
     // void provide_evidence(bool coeff_is_pos) {
     //     /*
@@ -284,27 +284,27 @@ public :
         m_bp.try_add_bound(u, j, is_low_bound, coeff_before_j_is_pos, m_row_or_term_index, strict);
     }
 
-    
+
     void advance_u(unsigned j) {
         if (m_column_of_u == -1)
             m_column_of_u = j;
         else
             m_column_of_u = -2;
     }
-    
+
     void advance_l(unsigned j) {
         if (m_column_of_l == -1)
             m_column_of_l = j;
         else
             m_column_of_l = -2;
     }
-    
+
     void analyze_bound_on_var_on_coeff(int j, const mpq &a) {
         switch (m_bp.get_column_type(j)) {
         case column_type::low_bound:
             if (numeric_traits<mpq>::is_pos(a))
                 advance_u(j);
-            else 
+            else
                 advance_l(j);
             break;
         case column_type::upper_bound:
@@ -325,7 +325,7 @@ public :
     static void analyze_row(linear_combination_iterator<mpq> &it,
                             const numeric_pair<mpq>& rs,
                             unsigned row_or_term_index,
-                            bound_propagator & bp
+                            lp_bound_propagator & bp
                             ) {
         bound_analyzer_on_row a(it, rs, row_or_term_index, bp);
         a.analyze();
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index b74515566..7c1817c26 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -51,7 +51,7 @@ class lar_solver : public column_namer {
     vector<lar_term*>                       m_terms;
     vector<lar_term*>                       m_orig_terms;
     const var_index                         m_terms_start_index;
-    indexed_vector<mpq>                     m_column_buffer;    
+    indexed_vector<mpq>                     m_column_buffer;
 public:
     lar_core_solver m_mpq_lar_core_solver;
     unsigned constraint_count() const {
@@ -66,7 +66,7 @@ public:
     static_matrix<mpq, numeric_pair<mpq>> const & A_r() const { return m_mpq_lar_core_solver.m_r_A;}
     static_matrix<double, double> & A_d() { return m_mpq_lar_core_solver.m_d_A;}
     static_matrix<double, double > const & A_d() const { return m_mpq_lar_core_solver.m_d_A;}
-    
+
     static bool valid_index(unsigned j){ return static_cast<int>(j) >= 0;}
 
 
@@ -84,7 +84,7 @@ public:
                    m_terms_start_index(1000000),
                    m_mpq_lar_core_solver(m_settings, *this)
     {}
-    
+
     void set_propagate_bounds_on_pivoted_rows_mode(bool v) {
         m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr;
     }
@@ -99,7 +99,7 @@ public:
     }
 
 #include "util/lp/init_lar_solver.h"
-    
+
     numeric_pair<mpq> const& get_value(var_index vi) const { return m_mpq_lar_core_solver.m_r_x[vi]; }
 
     bool is_term(var_index j) const {
@@ -113,7 +113,7 @@ public:
 
 
     bool use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; }
-    
+
     bool sizes_are_correct() const {
         lean_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count());
         lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size());
@@ -121,8 +121,8 @@ public:
         lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_x.size());
         return true;
     }
-    
- 
+
+
     void print_implied_bound(const implied_bound& be, std::ostream & out) const {
         out << "implied bound\n";
         unsigned v = be.m_j;
@@ -138,11 +138,11 @@ public:
         //     out << p.first << " : ";
         //     print_constraint(p.second, out);
         // }
-        
+
         // m_mpq_lar_core_solver.m_r_solver.print_column_info(be.m_j< m_terms_start_index? be.m_j : adjust_term_index(be.m_j), out);
         out << "end of implied bound" << std::endl;
     }
-    
+
     bool implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const {
         std::unordered_map<unsigned, mpq> coeff_map;
         auto rs_of_evidence = zero_of_type<mpq>();
@@ -164,7 +164,7 @@ public:
         lconstraint_kind kind = n_of_G ? GE : (n_of_L ? LE : EQ);
         if (strict)
             kind = static_cast<lconstraint_kind>((static_cast<int>(kind) / 2));
-      
+
         if (!is_term(be.m_j)) {
             if (coeff_map.size() != 1)
                 return false;
@@ -200,13 +200,13 @@ public:
         return kind == be.kind() && rs_of_evidence == be.m_bound;
     }
 
-    
+
     void analyze_new_bounds_on_row(
                                    unsigned row_index,
-                                   bound_propagator & bp) {
+                                   lp_bound_propagator & bp) {
         lean_assert(!use_tableau());
         iterator_on_pivot_row<mpq> it(m_mpq_lar_core_solver.get_pivot_row(), m_mpq_lar_core_solver.m_r_basis[row_index]);
-     
+
         bound_analyzer_on_row ra_pos(it,
                                      zero_of_type<numeric_pair<mpq>>(),
                                      row_index,
@@ -217,7 +217,7 @@ public:
 
     void analyze_new_bounds_on_row_tableau(
                                            unsigned row_index,
-                                           bound_propagator & bp
+                                           lp_bound_propagator & bp
                                            ) {
 
         if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation)
@@ -231,20 +231,20 @@ public:
                                            );
     }
 
-    
+
     void substitute_basis_var_in_terms_for_row(unsigned i) {
         // todo : create a map from term basic vars to the rows where they are used
         unsigned basis_j = m_mpq_lar_core_solver.m_r_solver.m_basis[i];
         for (unsigned k = 0; k < m_terms.size(); k++) {
             if (term_is_used_as_row(k))
                 continue;
-            if (!m_terms[k]->contains(basis_j)) 
+            if (!m_terms[k]->contains(basis_j))
                 continue;
             m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row);
         }
     }
-    
-    void calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp) {
+
+    void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator & bp) {
         if(use_tableau()) {
             analyze_new_bounds_on_row_tableau(i, bp);
         } else {
@@ -269,7 +269,7 @@ public:
       bound_evidences.push_back(fill_bound_evidence(implied_evidence));
       }
       }
-    
+
       void fill_bound_evidence_on_term(implied_bound & ie, implied_bound& be) {
       lean_assert(false);
       }
@@ -282,7 +282,7 @@ public:
       while (it.next(a, j)) {
       if (j == ie.m_j) continue;
       const ul_pair & ul = m_vars_to_ul_pairs[j];
-            
+
       if (is_neg(a)) { // so the monoid has a positive coeff on the right side
       constraint_index witness = toggle ? ul.m_low_bound_witness : ul.m_upper_bound_witness;
       lean_assert(is_valid(witness));
@@ -305,7 +305,7 @@ public:
 
       implied_bound fill_implied_bound_for_upper_bound(implied_bound& implied_evidence) {
       lean_assert(false);
-        
+
       be.m_j = implied_evidence.m_j;
       be.m_bound = implied_evidence.m_bound.x;
       be.m_kind = implied_evidence.m_bound.y.is_zero() ? LE : LT;
@@ -315,12 +315,12 @@ public:
       lean_assert(is_valid(witness));
       be.m_explanation.emplace_back(t.m_coeff, witness);
       }
-        
+
       }
     */
     /*
       void process_new_implied_evidence_for_upper_bound(
-      implied_bound& implied_evidence, 
+      implied_bound& implied_evidence,
       vector<implied_bound> & implied_bounds,
       std::unordered_map<unsigned, unsigned> & improved_upper_bounds) {
       unsigned existing_index;
@@ -336,7 +336,7 @@ public:
       }
     */
     //    implied_bound * get_existing_
-  
+
     linear_combination_iterator<mpq> * create_new_iter_from_term(unsigned term_index) const {
         lean_assert(false); // not implemented
         return nullptr;
@@ -347,13 +347,13 @@ public:
         unsigned ext_var_or_term = m_columns_to_ext_vars_or_term_indices[j];
         return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term;
     }
-    
-    void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset) {
+
+    void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset) {
         lean_assert(false); // not implemented
     }
 
 
-    void explain_implied_bound(implied_bound & ib, bound_propagator & bp) {
+    void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) {
         unsigned i = ib.m_row_or_term_index;
         int bound_sign = ib.m_is_low_bound? 1: -1;
         int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
@@ -367,7 +367,7 @@ public:
             if (j == m_j) continue;
             if (is_term(j)) {
                 j = m_ext_vars_to_columns[j];
-            } 
+            }
             int a_sign = is_pos(a)? 1: -1;
             int sign = j_sign * a_sign;
             const ul_pair & ul =  m_vars_to_ul_pairs[j];
@@ -383,8 +383,8 @@ public:
 		lean_assert(is_term(term));
 		return contains(m_ext_vars_to_columns, term);
     }
-    
-    void propagate_bounds_on_terms(bound_propagator & bp) {
+
+    void propagate_bounds_on_terms(lp_bound_propagator & bp) {
         for (unsigned i = 0; i < m_terms.size(); i++) {
             if (term_is_used_as_row(i + m_terms_start_index))
                 continue; // this term is used a left side of a constraint,
@@ -395,7 +395,7 @@ public:
 
 
     // goes over touched rows and tries to induce bounds
-    void propagate_bounds_for_touched_rows(bound_propagator & bp) {
+    void propagate_bounds_for_touched_rows(lp_bound_propagator & bp) {
         if (!use_tableau())
             return;  // ! todo : enable bound propagaion here. The current bug is that after the pop
         // the changed terms become incorrect!
@@ -420,7 +420,7 @@ public:
         m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true;
         return solve();
     }
-    
+
     lp_status solve() {
         if (m_status == INFEASIBLE) {
             return m_status;
@@ -430,7 +430,7 @@ public:
             if (m_settings.bound_propagation())
                 detect_rows_with_changed_bounds();
         }
-       
+
         m_columns_with_changed_bound.clear();
         return m_status;
     }
@@ -443,7 +443,7 @@ public:
         evidence.push_back(std::make_pair(-numeric_traits<mpq>::one(), ul.low_bound_witness()));
     }
 
-    
+
     unsigned get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); }
     // see http://research.microsoft.com/projects/z3/smt07.pdf
     // This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find
@@ -481,7 +481,7 @@ public:
         set.resize(n);
     }
 
-    
+
     void pop(unsigned k) {
         int n_was = static_cast<int>(m_ext_vars_to_columns.size());
 		m_status.pop(k);
@@ -502,14 +502,14 @@ public:
         clean_inf_set_of_r_solver_after_pop();
         lean_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
 			(!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
-        
-        
+
+
         lean_assert(ax_is_correct());
         lean_assert(m_mpq_lar_core_solver.m_r_solver.inf_set_is_correct());
         m_constraint_count.pop(k);
         for (unsigned i = m_constraint_count; i < m_constraints.size(); i++)
             delete m_constraints[i];
-        
+
         m_constraints.resize(m_constraint_count);
         m_term_count.pop(k);
         for (unsigned i = m_term_count; i < m_terms.size(); i++) {
@@ -523,7 +523,7 @@ public:
 		lean_assert(sizes_are_correct());
         lean_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
     }
-    
+
     vector<constraint_index> get_all_constraint_indices() const {
         vector<constraint_index> ret;
         constraint_index i = 0;
@@ -536,7 +536,7 @@ public:
                                   impq &term_max) {
         if (settings().simplex_strategy() == simplex_strategy_enum::undecided)
             decide_on_strategy_and_adjust_initial_state();
- 
+
         m_mpq_lar_core_solver.solve();
         if (m_mpq_lar_core_solver.m_r_solver.get_status() == UNBOUNDED)
             return false;
@@ -560,12 +560,12 @@ public:
         }
         return true;
     }
-    
+
     void set_costs_to_zero(const vector<std::pair<mpq, var_index>> & term) {
         auto & rslv = m_mpq_lar_core_solver.m_r_solver;
         auto & jset = m_mpq_lar_core_solver.m_r_solver.m_inf_set; // hijack this set that should be empty right now
         lean_assert(jset.m_index.size()==0);
-        
+
         for (auto & p : term) {
             unsigned j = p.second;
             rslv.m_costs[j] = zero_of_type<mpq>();
@@ -582,13 +582,13 @@ public:
             rslv.m_d[j] = zero_of_type<mpq>();
 
         jset.clear();
-        
+
         lean_assert(reduced_costs_are_zeroes_for_r_solver());
         lean_assert(costs_are_zeros_for_r_solver());
     }
 
     void prepare_costs_for_r_solver(const vector<std::pair<mpq, var_index>> & term) {
-        
+
         auto & rslv = m_mpq_lar_core_solver.m_r_solver;
         rslv.m_using_infeas_costs = false;
         lean_assert(costs_are_zeros_for_r_solver());
@@ -604,7 +604,7 @@ public:
         }
         lean_assert(rslv.reduced_costs_are_correct_tableau());
     }
-    
+
     bool maximize_term_on_corrected_r_solver(const vector<std::pair<mpq, var_index>> & term,
                                              impq &term_max) {
         settings().backup_costs = false;
@@ -627,7 +627,7 @@ public:
                 m_mpq_lar_core_solver.m_r_solver.set_status(OPTIMAL);
                 return ret;
             }
-            
+
         case simplex_strategy_enum::lu:
             lean_assert(false); // not implemented
             return false;
@@ -635,7 +635,7 @@ public:
             lean_unreachable(); // wrong mode
         }
         return false;
-    }    
+    }
     // starting from a given feasible state look for the maximum of the term
     // return true if found and false if unbounded
     bool maximize_term(const vector<std::pair<mpq, var_index>> & term,
@@ -644,9 +644,9 @@ public:
         m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = false;
         return maximize_term_on_corrected_r_solver(term, term_max);
     }
-    
 
-    
+
+
     const lar_term &  get_term(unsigned j) const {
         lean_assert(j >= m_terms_start_index);
         return *m_terms[j - m_terms_start_index];
@@ -697,14 +697,14 @@ public:
         else
             m_column_buffer.clear();
         lean_assert(m_column_buffer.size() == 0 && m_column_buffer.is_OK());
-        
+
         m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer);
         for (unsigned i : m_column_buffer.m_index)
             m_rows_with_changed_bounds.insert(i);
     }
 
 
-    
+
     void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) {
         for (auto & rc : m_mpq_lar_core_solver.m_r_A.m_columns[j])
             m_rows_with_changed_bounds.insert(rc.m_i);
@@ -715,7 +715,7 @@ public:
     bool use_tableau_costs() const {
         return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
     }
-    
+
     void detect_rows_of_column_with_bound_change(unsigned j) {
         if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { // it is a basic column
             // just mark the row at touched and exit
@@ -739,7 +739,7 @@ public:
             r += c.m_value * m_mpq_lar_core_solver.m_r_x[c.m_j];
         return is_zero(r);
     }
-    
+
     bool ax_is_correct() const {
         for (unsigned i = 0; i < A_r().row_count(); i++) {
             if (!row_is_correct(i))
@@ -755,7 +755,7 @@ public:
     bool costs_are_used() const {
         return m_settings.simplex_strategy() != simplex_strategy_enum::tableau_rows;
     }
-    
+
     void change_basic_x_by_delta_on_column(unsigned j, const numeric_pair<mpq> & delta) {
         if (use_tableau()) {
             for (const auto & c : A_r().m_columns[j]) {
@@ -795,7 +795,7 @@ public:
         }
     }
 
-    
+
     void detect_rows_with_changed_bounds_for_column(unsigned j) {
         if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) {
             m_rows_with_changed_bounds.insert(m_mpq_lar_core_solver.m_r_heading[j]);
@@ -804,10 +804,10 @@ public:
 
         if (use_tableau())
             detect_rows_of_bound_change_column_for_nbasic_column_tableau(j);
-        else 
+        else
             detect_rows_of_bound_change_column_for_nbasic_column(j);
     }
-    
+
     void detect_rows_with_changed_bounds() {
         for (auto j : m_columns_with_changed_bound.m_index)
             detect_rows_with_changed_bounds_for_column(j);
@@ -830,7 +830,7 @@ public:
         }
     }
 
-    
+
     void solve_with_core_solver() {
         if (!use_tableau())
             add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver);
@@ -844,34 +844,34 @@ public:
         }
         if (use_tableau())
             update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
-        else 
+        else
             update_x_and_inf_costs_for_columns_with_changed_bounds();
         m_mpq_lar_core_solver.solve();
         set_status(m_mpq_lar_core_solver.m_r_solver.get_status());
         lean_assert(m_status != OPTIMAL || all_constraints_hold());
     }
 
-    
+
     numeric_pair<mpq> get_basic_var_value_from_row_directly(unsigned i) {
         numeric_pair<mpq> r = zero_of_type<numeric_pair<mpq>>();
-        
+
         unsigned bj = m_mpq_lar_core_solver.m_r_solver.m_basis[i];
         for (const auto & c: A_r().m_rows[i]) {
             if (c.m_j == bj) continue;
             const auto & x = m_mpq_lar_core_solver.m_r_x[c.m_j];
-            if (!is_zero(x)) 
+            if (!is_zero(x))
                 r -= c.m_value * x;
         }
         return r;
     }
-    
-    
-    
+
+
+
     numeric_pair<mpq> get_basic_var_value_from_row(unsigned i) {
         if (settings().use_tableau()) {
             return get_basic_var_value_from_row_directly(i);
         }
-        
+
         numeric_pair<mpq> r = zero_of_type<numeric_pair<mpq>>();
         m_mpq_lar_core_solver.calculate_pivot_row(i);
         for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_pivot_row.m_index) {
@@ -900,9 +900,9 @@ public:
                 f = nullptr;
             }
         }
-        
+
     }
-    
+
     bool x_is_correct() const {
         if (m_mpq_lar_core_solver.m_r_x.size() != A_r().column_count()) {
             //            std::cout << "the size is off " << m_r_solver.m_x.size() << ", " << A().column_count() << std::endl;
@@ -921,7 +921,7 @@ public:
             }
         }
         return true;;
-    
+
     }
 
     bool var_is_registered(var_index vj) const {
@@ -938,7 +938,7 @@ public:
         return m_constraint_count.stack_size();
     }
 
-    void fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A, const lar_term * ls) {    
+    void fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A, const lar_term * ls) {
         lean_assert(A.row_count() > 0);
         lean_assert(A.column_count() > 0);
         unsigned last_row = A.row_count() - 1;
@@ -995,7 +995,7 @@ public:
     }
 
     std::string get_column_name(unsigned j) const {
-        if (j >= m_terms_start_index) 
+        if (j >= m_terms_start_index)
             return std::string("_t") + T_to_string(j);
         if (j >= m_columns_to_ext_vars_or_term_indices.size())
             return std::string("_s") + T_to_string(j);
@@ -1039,7 +1039,7 @@ public:
             return true;
         std::unordered_map<var_index, mpq> var_map;
         get_model(var_map);
-    
+
         for (unsigned i = 0; i < m_constraints.size(); i++) {
             if (!constraint_holds(*m_constraints[i], var_map)) {
                 print_constraint(i, std::cout);
@@ -1201,7 +1201,7 @@ public:
             return false;
         }
     }
-    
+
     bool has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) {
 
         if (var >= m_vars_to_ul_pairs.size()) {
@@ -1253,7 +1253,7 @@ public:
             constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.low_bound_witness();
             lean_assert(bound_constr_i < m_constraints.size());
             explanation.push_back(std::make_pair(coeff, bound_constr_i));
-        } 
+        }
     }
 
 
@@ -1263,9 +1263,9 @@ public:
         lean_assert(m_status == OPTIMAL);
         unsigned i;
         do {
-            
+
             // different pairs have to produce different singleton values
-            std::unordered_set<impq> set_of_different_pairs; 
+            std::unordered_set<impq> set_of_different_pairs;
             std::unordered_set<mpq> set_of_different_singles;
             delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
             for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
@@ -1278,7 +1278,7 @@ public:
                     delta /= mpq(2);
                     break;
                 }
-                    
+
                 variable_values[i] = x;
             }
         } while (i != m_mpq_lar_core_solver.m_r_x.size());
@@ -1318,7 +1318,7 @@ public:
         mpq free_coeff = c->get_free_coeff_of_left_side();
         if (!is_zero(free_coeff))
             out << " + " << free_coeff;
-        
+
     }
 
     void print_term(lar_term const& term, std::ostream & out) const {
@@ -1345,7 +1345,7 @@ public:
     }
 
     void fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector<unsigned>& column_list) {
-        for (unsigned i = 0; i < sz; i++) {        
+        for (unsigned i = 0; i < sz; i++) {
             var_index var = vars[i];
             if (var >= m_terms_start_index) { // handle the term
                 for (auto & it : m_terms[var - m_terms_start_index]->m_coeffs) {
@@ -1412,7 +1412,7 @@ public:
             if (cost_is_nz) {
                 m_mpq_lar_core_solver.m_r_solver.m_d[rc.m_j] += cost_j*rc.get_val();
             }
-            
+
             A_r().remove_element(last_row, rc);
         }
         lean_assert(last_row.size() == 0);
@@ -1484,7 +1484,7 @@ public:
 
         lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count());
         lean_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct());
-        // We remove last variables starting from m_column_names.size() to m_vec_of_canonic_left_sides.size().    
+        // We remove last variables starting from m_column_names.size() to m_vec_of_canonic_left_sides.size().
         // At this moment m_column_names is already popped
         for (unsigned j = A_r().column_count(); j-- > m_columns_to_ext_vars_or_term_indices.size();)
             remove_column_from_tableau(j);
@@ -1526,8 +1526,8 @@ public:
         }
         for (unsigned j : became_feas)
             m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j);
-    
-    
+
+
         if (use_tableau_costs()) {
             for (unsigned j : became_feas)
                 m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j);
@@ -1544,6 +1544,6 @@ public:
         lean_assert(this->explanation_is_correct(explanation));
     }
 
-    
+
 };
 }
diff --git a/src/util/lp/lp_bound_propagator.cpp b/src/util/lp/lp_bound_propagator.cpp
index 0d58ec2be..cbd4f28f2 100644
--- a/src/util/lp/lp_bound_propagator.cpp
+++ b/src/util/lp/lp_bound_propagator.cpp
@@ -4,23 +4,23 @@
 */
 #include "util/lp/lar_solver.h"
 namespace lean {
-bound_propagator::bound_propagator(lar_solver & ls):
+    lp_bound_propagator::lp_bound_propagator(lar_solver & ls):
     m_lar_solver(ls) {}
-column_type bound_propagator::get_column_type(unsigned j) const {
+column_type lp_bound_propagator::get_column_type(unsigned j) const {
     return m_lar_solver.m_mpq_lar_core_solver.m_column_types()[j];
 }
-const impq & bound_propagator::get_low_bound(unsigned j) const {
+const impq & lp_bound_propagator::get_low_bound(unsigned j) const {
     return m_lar_solver.m_mpq_lar_core_solver.m_r_low_bounds()[j];
 }
-const impq & bound_propagator::get_upper_bound(unsigned j) const {
+const impq & lp_bound_propagator::get_upper_bound(unsigned j) const {
     return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
 }
-void bound_propagator::try_add_bound(const mpq & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
+void lp_bound_propagator::try_add_bound(const mpq & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
     j = m_lar_solver.adjust_column_index_to_term_index(j);
     lconstraint_kind kind = is_low? GE : LE;
     if (strict)
         kind = static_cast<lconstraint_kind>(kind / 2);
-    
+
     if (!bound_is_interesting(j, kind, v))
         return;
      unsigned k; // index to ibounds
diff --git a/src/util/lp/lp_bound_propagator.h b/src/util/lp/lp_bound_propagator.h
index 92523d75f..f1e0d486e 100644
--- a/src/util/lp/lp_bound_propagator.h
+++ b/src/util/lp/lp_bound_propagator.h
@@ -6,14 +6,14 @@
 #include "util/lp/lp_settings.h"
 namespace lean {
 class lar_solver;
-class bound_propagator {
+class lp_bound_propagator {
     std::unordered_map<unsigned, unsigned> m_improved_low_bounds; // these maps map a column index to the corresponding index in ibounds
     std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
     lar_solver & m_lar_solver;
 public:
     vector<implied_bound> m_ibounds;
 public:
-    bound_propagator(lar_solver & ls);
+    lp_bound_propagator(lar_solver & ls);
     column_type get_column_type(unsigned) const;
     const impq & get_low_bound(unsigned) const;
     const impq & get_upper_bound(unsigned) const;