diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index bded5dc26..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);