diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc
index af04fa7e3..14cb9f96a 100644
--- a/src/tsolvers/lasolver/LASolver.cc
+++ b/src/tsolvers/lasolver/LASolver.cc
@@ -1034,14 +1034,15 @@ vec<PTRef> LASolver::collectEqualitiesFor(vec<PTRef> const & vars, std::unordere
         }
         for (auto const & val : valuesWithDelta) {
             for (auto const & entry : eqClasses) {
-                // check if entry.first - val could be 0 for some value of delta, with 0 < delta <= 1
+                // check if entry.first - val could be 0 for some value of delta, with 0 < delta <= maxDelta
                 auto diff = entry.first - val;
                 if (not diff.hasDelta()) { continue; } // MB: This takes care also of the case where val == entry.first
                 if (isNonNegative(diff.R()) and isPositive(diff.D())) { continue; }
                 if (isNonPositive(diff.R()) and isNegative(diff.D())) { continue; }
                 auto ratio = diff.R() / diff.D();
                 assert(isNegative(ratio));
-                if (ratio < FastRational(-1)) { continue; } // MB: ratio is -delta; hence -1 <= ratio < 0
+                ratio.negate(); // MB: delta is the negated ratio
+                if (ratio > Simplex::maxDelta) { continue; } // No chance of collision
 
                 // They could be equal for the right value of delta, add equalities for cross-product
                 vec<PTRef> const & varsOfFirstVal = eqClasses.at(val);
diff --git a/src/tsolvers/lasolver/Simplex.cc b/src/tsolvers/lasolver/Simplex.cc
index d73914b04..e1f2a01f1 100644
--- a/src/tsolvers/lasolver/Simplex.cc
+++ b/src/tsolvers/lasolver/Simplex.cc
@@ -409,10 +409,13 @@ Delta Simplex::getValuation(LVRef v) const {
     return val;
 }
 
+// Definition of static member: maxDelta = 1/2;
+const opensmt::Real Simplex::maxDelta {1,2};
+
 opensmt::Real Simplex::computeDelta() const {
 
     /*
-     Delta computation according to the Technical Report accompanying the Simple paper
+     Delta computation according to the Technical Report accompanying the Simplex paper
      https://yices.csl.sri.com/papers/sri-csl-06-01.pdf
      For a pair (c,k) \in Q_\delta representing Real value c + k * \delta if the inequality (c_1, k_1) <= (c_2, k_2) holds
      then there exists \delta_0 such that \forall 0 < \epsilon < \delta_0 the inequality c_1 + k_1 * \epsilon <= c_2 + k_2 * \epsilon holds.
@@ -427,15 +430,14 @@ opensmt::Real Simplex::computeDelta() const {
     Delta delta_abst;
     bool deltaNotSet = true;
 
-    const LAVarStore& laVarStore = boundStore.getVarStore();
-    for (LVRef v : laVarStore)
-    {
-        assert( !isModelOutOfBounds(v) );
+    LAVarStore const & laVarStore = boundStore.getVarStore();
+    for (LVRef v : laVarStore) {
+        assert(not isModelOutOfBounds(v));
 
-        if (model->read(v).D() == 0)
+        auto const & val = model->read(v);
+        if (val.D().isZero())
             continue; // If values are exact we do not need to consider them for delta computation
 
-        auto const & val = model->read(v);
         // Computing delta to satisfy lower bound
         if (model->hasLBound(v)) {
             auto const & lb = model->Lb(v);
@@ -443,7 +445,7 @@ opensmt::Real Simplex::computeDelta() const {
             if (lb.R() < val.R() && lb.D() > val.D()) {
                 Real valOfDelta = (val.R() - lb.R()) / (lb.D() - val.D());
                 assert(valOfDelta > 0);
-                if (deltaNotSet || delta_abst > valOfDelta) {
+                if (deltaNotSet or delta_abst > valOfDelta) {
                     deltaNotSet = false;
                     delta_abst = valOfDelta;
                 }
@@ -456,7 +458,7 @@ opensmt::Real Simplex::computeDelta() const {
             if (val.R() < ub.R() && val.D() > ub.D()) {
                 Real valOfDelta = (ub.R() - val.R()) / (val.D() - ub.D());
                 assert(valOfDelta > 0);
-                if (deltaNotSet || delta_abst > valOfDelta) {
+                if (deltaNotSet or delta_abst > valOfDelta) {
                     deltaNotSet = false;
                     delta_abst = valOfDelta;
                 }
@@ -464,8 +466,8 @@ opensmt::Real Simplex::computeDelta() const {
         }
     }
 
-    if (deltaNotSet || delta_abst > 1) {
-        return 1;
+    if (deltaNotSet or delta_abst > maxDelta) {
+        return maxDelta;
     }
     return delta_abst.R()/2;
 }
diff --git a/src/tsolvers/lasolver/Simplex.h b/src/tsolvers/lasolver/Simplex.h
index 03d6ded58..f51b1e721 100644
--- a/src/tsolvers/lasolver/Simplex.h
+++ b/src/tsolvers/lasolver/Simplex.h
@@ -100,6 +100,7 @@ class Simplex {
     bool checkValueConsistency() const;
     bool invariantHolds() const;
 
+    static const opensmt::Real maxDelta;
     opensmt::Real computeDelta() const;
     Delta getValuation(LVRef) const;                     // Understands also variables deleted by gaussian elimination
 //    Delta read(LVRef v) const { assert(!tableau.isQuasiBasic(v)); return model->read(v); } // ignores unsafely variables deleted by gaussian elimination