diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 573a9be41..c1a44ca63 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -299,7 +299,7 @@ public:
     inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; }
     inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
     template <typename T>
-    void explain_implied_bound(implied_bound & ib, lp_bound_propagator<T> & bp) {
+    void explain_implied_bound(const implied_bound & ib, lp_bound_propagator<T> & bp) {
         unsigned i = ib.m_row_or_term_index;
         int bound_sign = ib.m_is_lower_bound? 1: -1;
         int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index c9018bfd4..f7a165854 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -67,8 +67,14 @@ class lp_bound_propagator {
     std::unordered_map<unsigned, unsigned>    m_improved_upper_bounds;
     T&                                        m_imp;
     impq                                      m_zero;
-public:
     vector<implied_bound> m_ibounds;
+public:
+    const vector<implied_bound>& ibounds() const { return m_ibounds; }
+    void init() {
+        m_improved_upper_bounds.clear();
+        m_improved_lower_bounds.clear();
+        m_ibounds.reset();
+    }
     lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {}
     const lar_solver& lp() const { return m_imp.lp(); }
     column_type get_column_type(unsigned j) const {
@@ -178,9 +184,8 @@ public:
         }
             
     }
-
+        
     void clear_for_eq() {
-        //        m_reported_pairs.reset();
         m_visited_rows.reset();
         m_visited_columns.reset();
         m_offset_to_verts.reset();
@@ -251,8 +256,9 @@ public:
     void find_path_on_tree(ptr_vector<vertex> & path, vertex* u, vertex* v) const {
         vertex* up; // u parent
         vertex* vp; // v parent
+        ptr_vector<vertex> v_branch;
         path.push_back(u);
-        path.push_back(v);
+        v_branch.push_back(v);
          // equalize the levels
         while (u->level() > v->level()) {
             up = u->parent();
@@ -264,7 +270,7 @@ public:
         while (u->level() < v->level()) {            
             vp = v->parent();
             if (v->row() == vp->row())
-                path.push_back(vp);
+                v_branch.push_back(vp);
             v = vp;
         }
         SASSERT(u->level() == v->level());
@@ -278,9 +284,13 @@ public:
             if (up->row() == u->row())
                 path.push_back(up);
             if (vp->row() == v->row())
-                path.push_back(vp);
+                v_branch.push_back(vp);
             u = up; v = vp;
         }
+        
+        for (unsigned i = v_branch.size(); i--; ) {
+            path.push_back(v_branch[i]);
+        }
     }
     
     bool tree_is_correct() const {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 62ab6bec0..b403ed489 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -165,11 +165,11 @@ class theory_lra::imp {
     };
 
 
-    theory_lra&          th;
-    ast_manager&         m;
-    arith_util           a;
-    arith_eq_adapter     m_arith_eq_adapter;
-    vector<rational>     m_columns;
+    theory_lra&                  th;
+    ast_manager&                 m;
+    arith_util                   a;
+    arith_eq_adapter             m_arith_eq_adapter;
+    vector<rational>             m_columns;
       
 
     // temporary values kept during internalization
@@ -309,13 +309,14 @@ class theory_lra::imp {
     int_hashtable<var_value_hash, var_value_eq>   m_model_eqs;
 
 
-    svector<scope>         m_scopes;
-    lp_api::stats          m_stats;
-    arith_factory*         m_factory;       
-    scoped_ptr<lp::lar_solver> m_solver;
-    resource_limit         m_resource_limit;
-    lp_bounds              m_new_bounds;
-    symbol                 m_farkas;
+    svector<scope>               m_scopes;
+    lp_api::stats                m_stats;
+    arith_factory*               m_factory;       
+    scoped_ptr<lp::lar_solver>   m_solver;
+    resource_limit               m_resource_limit;
+    lp_bounds                    m_new_bounds;
+    symbol                       m_farkas;
+    lp::lp_bound_propagator<imp> m_bp;
 
     context& ctx() const { return th.get_context(); }
     theory_id get_id() const { return th.get_id(); }
@@ -958,7 +959,9 @@ public:
         m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
         m_solver(nullptr),
         m_resource_limit(*this),
-        m_farkas("farkas") {
+        m_farkas("farkas"),
+        m_bp(*this)
+    {
     }
         
     ~imp() {
@@ -2351,10 +2354,9 @@ public:
     void propagate_bounds_with_lp_solver() {
         if (!should_propagate()) 
             return;
-        
-        lp::lp_bound_propagator<imp>  bp(*this);
 
-        lp().propagate_bounds_for_touched_rows(bp);
+        m_bp.init();
+        lp().propagate_bounds_for_touched_rows(m_bp);
 
         if (!m.inc()) {
             return;
@@ -2364,8 +2366,11 @@ public:
             get_infeasibility_explanation_and_set_conflict();
         }
         else {
-            for (unsigned i = 0; m.inc() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) {
-                propagate_lp_solver_bound(bp.m_ibounds[i]);
+            for (auto& ib : m_bp.ibounds()) {
+                m.inc();
+                if (ctx().inconsistent())
+                    break;
+                propagate_lp_solver_bound(ib);
             }
         }
     }
@@ -2386,7 +2391,7 @@ public:
         }
         return false;
     }
-    void propagate_lp_solver_bound(lp::implied_bound& be) {
+    void propagate_lp_solver_bound(const lp::implied_bound& be) {
         lpvar vi = be.m_j;
         theory_var v = lp().local_to_external(vi);
 
@@ -2418,8 +2423,7 @@ public:
                 first = false;
                 reset_evidence();
                 m_explanation.clear();
-                lp::lp_bound_propagator<imp> bp(*this);
-                lp().explain_implied_bound(be, bp);
+                lp().explain_implied_bound(be, m_bp);
             }
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
             updt_unassigned_bounds(v, -1);
@@ -4045,5 +4049,5 @@ expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_ration
 }
 template  class lp::lp_bound_propagator<smt::theory_lra::imp>;
 template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);
-template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&);
+template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(const lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&);
 template void lp::lar_solver::calculate_implied_bounds_for_row<smt::theory_lra::imp>(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>&);