diff --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h b/mlir/include/mlir/Analysis/Presburger/Simplex.h
--- a/mlir/include/mlir/Analysis/Presburger/Simplex.h
+++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h
@@ -705,7 +705,28 @@
   /// the set of solutions does not change if these constraints are removed.
   /// Marks these constraints as redundant. Whether a specific constraint has
   /// been marked redundant can be queried using isMarkedRedundant.
-  void detectRedundant();
+  ///
+  /// The first overload only tries to find redundant constraints with indices
+  /// in the range [offset, offset + count), by scanning constraints from left
+  /// to right in this range. If `count` is not provided, all constraints
+  /// starting at `offset` are scanned, and if neither are provided, all
+  /// constraints are scanned, starting from 0 and going to the last constraint.
+  ///
+  /// As an example, in the set (x) : (x >= 0, x >= 0, x >= 0), calling
+  /// `detectRedundant` with no parameters will result in the first two
+  /// constraints being marked redundant. All copies cannot be marked redundant
+  /// because removing all the constraints changes the set. The first two are
+  /// the ones marked redundant because we scan from left to right. Thus, when
+  /// there is some preference among the constraints as to which should be
+  /// marked redundant with priority when there are multiple possibilities, this
+  /// could be accomplished by succesive calls to detectRedundant(offset,
+  /// count).
+  void detectRedundant(unsigned offset, unsigned count);
+  void detectRedundant(unsigned offset) {
+    assert(offset <= con.size() && "invalid offset!");
+    detectRedundant(offset, con.size() - offset);
+  }
+  void detectRedundant() { detectRedundant(0, con.size()); }
 
   /// Returns a (min, max) pair denoting the minimum and maximum integer values
   /// of the given expression. If no integer value exists, both results will be
diff --git a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
--- a/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
@@ -291,11 +291,19 @@
         continue;
       }
 
-      simplex.detectRedundant();
-
       // Equalities are added to simplex as a pair of inequalities.
       unsigned totalNewSimplexInequalities =
           2 * sI.getNumEqualities() + sI.getNumInequalities();
+      // Look for redundant constraints among the constraints of sI. We don't
+      // care about redundant constraints in `b` at this point.
+      //
+      // When there are two copies of a constraint in `simplex`, i.e., among the
+      // constraints of `b` and `sI`, only one of them can be marked redundant.
+      // (Assuming no other constraint makes these redundant.)
+      //
+      // In a case where there is one copy in `b` and one in `sI`, we want the
+      // one in `sI` to be marked, not the one in `b`.
+      simplex.detectRedundant(offset, totalNewSimplexInequalities);
       for (unsigned j = 0; j < totalNewSimplexInequalities; j++)
         canIgnoreIneq[j] = simplex.isMarkedRedundant(offset + j);
       simplex.rollback(snapshotBeforeIntersect);
diff --git a/mlir/lib/Analysis/Presburger/Simplex.cpp b/mlir/lib/Analysis/Presburger/Simplex.cpp
--- a/mlir/lib/Analysis/Presburger/Simplex.cpp
+++ b/mlir/lib/Analysis/Presburger/Simplex.cpp
@@ -1387,7 +1387,8 @@
 }
 
 /// Find a subset of constraints that is redundant and mark them redundant.
-void Simplex::detectRedundant() {
+void Simplex::detectRedundant(unsigned offset, unsigned count) {
+  assert(offset + count <= con.size() && "invalid range!");
   // It is not meaningful to talk about redundancy for empty sets.
   if (empty)
     return;
@@ -1401,7 +1402,8 @@
   // two identical constraints both being marked redundant since each is
   // redundant given the other one. In this example, only the first of the
   // constraints that is processed will get marked redundant, as it should be.
-  for (Unknown &u : con) {
+  for (unsigned i = 0; i < count; ++i) {
+    Unknown &u = con[offset + i];
     if (u.orientation == Orientation::Column) {
       unsigned column = u.pos;
       Optional<unsigned> pivotRow = findPivotRow({}, Direction::Down, column);
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
@@ -763,4 +763,10 @@
   // Previously, the subtraction result was producing an extra empty set, which
   // is correct, but bad for output size.
   EXPECT_EQ(result.getNumDisjuncts(), 1u);
+
+  PresburgerSet subtractSelf = set1.subtract(set1);
+  EXPECT_TRUE(subtractSelf.isIntegerEmpty());
+  // Previously, the subtraction result was producing several unnecessary empty
+  // sets, which is correct, but bad for output size.
+  EXPECT_EQ(subtractSelf.getNumDisjuncts(), 0u);
 }