diff --git a/mlir/lib/Analysis/Presburger/PresburgerSet.cpp b/mlir/lib/Analysis/Presburger/PresburgerSet.cpp
--- a/mlir/lib/Analysis/Presburger/PresburgerSet.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerSet.cpp
@@ -401,6 +401,90 @@
   return result;
 }
 
+/// Given an IntegerPolyhedron `p` and one of its inequalities `ineq`, check
+/// that all inequalities of `cut` are redundant for the facet of `p` where
+/// `ineq` holds as an equality.
+LogicalResult containedFacet(ArrayRef<int64_t> ineq, IntegerPolyhedron &p,
+                             ArrayRef<ArrayRef<int64_t>> cut) {
+  Simplex simp(p);
+  simp.addEquality(ineq);
+  for (ArrayRef<int64_t> curr : cut) {
+    if (simp.findIneqType(curr) != Simplex::IneqType::Redundant) {
+      return failure();
+    }
+  }
+  return success();
+}
+
+/// Adds `poly` to `polyhedrons` and removes the polyhedrons at position `i` and
+/// `j`. Updates `simplices` to reflect the changes. `i` and `j` cannot be
+/// equal.
+void addCoalescedPolyhedron(SmallVectorImpl<IntegerPolyhedron> &polyhedrons,
+                            unsigned i, unsigned j, IntegerPolyhedron &poly,
+                            SmallVectorImpl<Simplex> &simplices) {
+  assert(i != j && "The indices must refer to different polyhedra");
+  IntegerPolyhedron newSet = poly;
+
+  unsigned n = polyhedrons.size();
+  polyhedrons[i] = polyhedrons[n - 1];
+  polyhedrons[j] = polyhedrons[n - 2];
+  polyhedrons.pop_back();
+  polyhedrons[n - 2] = newSet;
+
+  simplices[i] = simplices[n - 1];
+  simplices[j] = simplices[n - 2];
+  simplices.pop_back();
+  simplices[n - 2] = Simplex(newSet);
+}
+
+/// Given two polyhedra `a` and `b` at positions `i` and `j` in `polyhedrons`
+/// and `redundantIneqsA` being the inequalities of `a` that are redundant for
+/// `b` (similarly for `cuttingIneqsA`, `redundantIneqsB`, and `cuttingIneqsB`),
+/// checks whether the facets of all cutting inequalites of `a` are contained in
+/// `b`. If so, a new polyhedron consisting of all redundant inequalites of `a`
+/// and `b` and all equalities of both is created.
+///
+/// An example of this case:
+///    ___________        ___________
+///   /   /  |   /       /          /
+///   \   \  |  /   ==>  \         /
+///    \   \ | /          \       /
+///     \___\|/            \_____/
+///
+///
+LogicalResult cutCase(SmallVectorImpl<IntegerPolyhedron> &polyhedrons,
+                      SmallVectorImpl<Simplex> &simplices, unsigned i,
+                      unsigned j, ArrayRef<ArrayRef<int64_t>> redundantIneqsA,
+                      ArrayRef<ArrayRef<int64_t>> cuttingIneqsA,
+                      ArrayRef<ArrayRef<int64_t>> redundantIneqsB,
+                      ArrayRef<ArrayRef<int64_t>> cuttingIneqsB) {
+  for (ArrayRef<int64_t> curr : cuttingIneqsA) {
+    /// All inequalities of b need to be redundant. We already know that the
+    /// redundant ones are, so only the cutting ones remain to be checked.
+    if (containedFacet(curr, polyhedrons[i], cuttingIneqsB).failed()) {
+      return failure();
+    }
+  }
+  IntegerPolyhedron newSet(polyhedrons[i].getNumDimIds(),
+                           polyhedrons[i].getNumSymbolIds(),
+                           polyhedrons[i].getNumLocalIds());
+
+  for (ArrayRef<int64_t> curr : redundantIneqsA)
+    newSet.addInequality(curr);
+
+  for (ArrayRef<int64_t> curr : redundantIneqsB)
+    newSet.addInequality(curr);
+
+  for (unsigned k = 0, e = polyhedrons[i].getNumEqualities(); k < e; k++)
+    newSet.addEquality(polyhedrons[i].getEquality(k));
+
+  for (unsigned k = 0, e = polyhedrons[j].getNumEqualities(); k < e; k++)
+    newSet.addEquality(polyhedrons[j].getEquality(k));
+
+  addCoalescedPolyhedron(polyhedrons, i, j, newSet, simplices);
+  return success();
+}
+
 /// Types the inequalities of `p` according to their `IneqType` for `simp` into
 /// `redundantIneqs` and `cuttingIneqs`. Returns success, if no separate
 /// inequalities were encountered. Otherwise, returns failure.
@@ -495,6 +579,20 @@
     return success();
   }
 
+  // Try to apply the cut case if all equalities of `a` are redundant (and b
+  // respectively).
+  if (onlyRedundantEqsA &&
+      cutCase(polyhedrons, simplices, i, j, redundantIneqsA, cuttingIneqsA,
+              redundantIneqsB, cuttingIneqsB)
+          .succeeded())
+    return success();
+
+  if (onlyRedundantEqsB &&
+      cutCase(polyhedrons, simplices, j, i, redundantIneqsB, cuttingIneqsB,
+              redundantIneqsA, cuttingIneqsA)
+          .succeeded())
+    return success();
+
   return failure();
 }
 
diff --git a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
--- a/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/PresburgerSetTest.cpp
@@ -528,7 +528,7 @@
              "(x) : ( x >= 0, -x + 3 >= 0)",
              "(x) : ( x - 2 >= 0, -x + 4 >= 0)",
          });
-  expectCoalesce(2, set);
+  expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceSeparateOneDim) {
@@ -552,7 +552,7 @@
              "(x,y) : (x >= 0, -x + 3 >= 0, y >= 0, -y + 2 >= 0)",
              "(x,y) : (x >= 0, -x + 3 >= 0, y - 1 >= 0, -y + 3 >= 0)",
          });
-  expectCoalesce(2, set);
+  expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceSeparateTwoDim) {
@@ -579,7 +579,7 @@
              "(x,y) : (x - 1 >= 0, -x + 3 >= 0, x - y == 0)",
              "(x,y) : (x >= 0, -x + 2 >= 0, x - y == 0)",
          });
-  expectCoalesce(2, set);
+  expectCoalesce(1, set);
 }
 
 TEST(SetTest, coalesceSeparateEq) {