diff --git a/src/util/lp/column_namer.h b/src/util/lp/column_namer.h
index 1a10a5a23..a3fe05dd0 100644
--- a/src/util/lp/column_namer.h
+++ b/src/util/lp/column_namer.h
@@ -15,7 +15,7 @@ public:
         T a;
         unsigned i;
         while (it->next(a, i)) {
-            coeff.emplace_back(a, i);
+            coeff.push_back(std::make_pair(a, i));
         }
         print_linear_combination_of_column_indices(coeff, out);
     }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 7c1817c26..c8048a550 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -1259,7 +1259,7 @@ public:
 
 
     void get_model(std::unordered_map<var_index, mpq> & variable_values) const {
-        mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
+        mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes
         lean_assert(m_status == OPTIMAL);
         unsigned i;
         do {
@@ -1267,7 +1267,6 @@ public:
             // different pairs have to produce different singleton values
             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++ ) {
                 const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
                 set_of_different_pairs.insert(rp);
@@ -1543,7 +1542,5 @@ public:
         quick_xplain::run(explanation, *this);
         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 cbd4f28f2..8b42f24a0 100644
--- a/src/util/lp/lp_bound_propagator.cpp
+++ b/src/util/lp/lp_bound_propagator.cpp
@@ -16,31 +16,36 @@ 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 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);
+    unsigned term_j = m_lar_solver.adjust_column_index_to_term_index(j);
+	mpq w = v;
+	if (term_j != j) {
+		j = term_j;
+		w += m_lar_solver.get_term(term_j).m_v; // when terms are turned into the columns they "lose" the right side, at this moment they aquire it back
+	}
     lconstraint_kind kind = is_low? GE : LE;
     if (strict)
         kind = static_cast<lconstraint_kind>(kind / 2);
 
-    if (!bound_is_interesting(j, kind, v))
+    if (!bound_is_interesting(j, kind, w))
         return;
      unsigned k; // index to ibounds
      if (is_low) {
          if (try_get_val(m_improved_low_bounds, j, k)) {
              auto & found_bound = m_ibounds[k];
-             if (v > found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict))
-                 found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
+             if (w > found_bound.m_bound || (w == found_bound.m_bound && found_bound.m_strict == false && strict))
+                 found_bound = implied_bound(w, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
          } else {
              m_improved_low_bounds[j] = m_ibounds.size();
-             m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
+             m_ibounds.push_back(implied_bound(w, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
          }
      } else { // the upper bound case
          if (try_get_val(m_improved_upper_bounds, j, k)) {
              auto & found_bound = m_ibounds[k];
-             if (v < found_bound.m_bound || (v == found_bound.m_bound && found_bound.m_strict == false && strict))
-                 found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
+             if (w < found_bound.m_bound || (w == found_bound.m_bound && found_bound.m_strict == false && strict))
+                 found_bound = implied_bound(w, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
          } else {
              m_improved_upper_bounds[j] = m_ibounds.size();
-             m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
+             m_ibounds.push_back(implied_bound(w, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
         }
      }
 }