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
@@ -376,8 +376,9 @@
 /// where we take a modulo of the whole symbolic expression on the right to
 /// bring it into the range [0, d - 1]. Therefore, as in LexSimplex::addCut,
 /// k is the quotient on dividing the LHS by d, and since LHS >= 0, we have
-/// k >= 0 as well. We realize the modulo of the symbolic expression by adding a
-/// division variable
+/// k >= 0 as well. If all the a_i are divisible by d, then we can add the
+/// constraint directly.  Otherwise, we realize the modulo of the symbolic
+/// expression by adding a division variable
 ///
 /// q = ((-c%d) + sum_i (-a_i%d)s_i)/d
 ///
@@ -392,16 +393,23 @@
 LogicalResult SymbolicLexSimplex::addSymbolicCut(unsigned row) {
   int64_t d = tableau(row, 0);
 
-  // Add the division variable `q` described above to the symbol domain.
-  // q = ((-c%d) + sum_i (-a_i%d)s_i)/d.
+  // Make the division variable `q = ((-c%d) + sum_i (-a_i%d)s_i)/d`.
   SmallVector<int64_t, 8> divCoeffs;
   divCoeffs.reserve(nSymbol + 1);
   int64_t divDenom = d;
   for (unsigned col = 3; col < 3 + nSymbol; ++col)
     divCoeffs.push_back(mod(-tableau(row, col), divDenom)); // (-a_i%d)s_i
   divCoeffs.push_back(mod(-tableau(row, 1), divDenom));     // -c%d.
-
   normalizeDiv(divCoeffs, divDenom);
+
+  if (divDenom == 1) {
+    // The symbolic sample numerator is divisible by 1, so the division isn't
+    // a division at all: it has denominator 1. We add the constraint directly,
+    // which is equivalent to adding ignoring the symbols and adding a regular
+    // cut as in LexSimplexBase::addCut.
+    return LexSimplexBase::addCut(row);
+  }
+
   domainSimplex.addDivisionVariable(divCoeffs, divDenom);
   domainPoly.addLocalFloorDiv(divCoeffs, divDenom);