diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
index fbedf9f46a..fa30307cec 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
@@ -211,7 +211,7 @@ def toLinearExpr (e : Expr) : MetaM (Int.Linear.Expr × Array Expr) := do
   if atoms.size == 1 then
     return (e, atoms)
   else
-    let (atoms, perm) := sortExprs atoms
+    let (atoms, perm) := sortExprs atoms (lt := false)
     let e := e.applyPerm perm
     return (e, atoms)
 
diff --git a/tests/lean/run/grind_cutsat_nat_dvd.lean b/tests/lean/run/grind_cutsat_nat_dvd.lean
index 2d85e95f4b..f9741ed9ea 100644
--- a/tests/lean/run/grind_cutsat_nat_dvd.lean
+++ b/tests/lean/run/grind_cutsat_nat_dvd.lean
@@ -30,3 +30,15 @@ example (x y : Nat) :
 
 example (i : Nat) : i < 330 → 7 ∣ (660 + i) * (1319 - i) → 1319 - i < 1979 := by
   grind
+
+example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
+    4 ≤ (x + y) % 8 ∧ (x + y) % 8 ≤ 6 := by
+  grind
+
+example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
+    4 ≤ (y + x) % 8 ∧ (x + y) % 8 ≤ 6 := by
+  grind
+
+example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
+    4 ≤ (y + x) % 8 ∧ (y + x) % 8 ≤ 6 := by
+  grind