chore: fix test

This PR fixes bugs in `Std.Internal.Rat.floor` and `Std.Internal.Rat.ceil`.

src/Std/Internal/Rat.lean

@@ -7,6 +7,7 @@ prelude
 import Init.NotationExtra
 import Init.Data.ToString.Macro
 import Init.Data.Int.DivMod.Basic
+import Init.Data.Int.Linear
 import Init.Data.Nat.Gcd
 namespace Std
 namespace Internal
@@ -101,15 +102,13 @@ protected def floor (a : Rat) : Int :=
   if a.den == 1 then
     a.num
   else
-    let r := a.num.tmod a.den
-    if a.num < 0 then r - 1 else r
+    a.num / a.den
 
 protected def ceil (a : Rat) : Int :=
   if a.den == 1 then
     a.num
   else
-    let r := a.num.tmod a.den
-    if a.num > 0 then r + 1 else r
+    Int.Linear.cdiv a.num a.den
 
 instance : LT Rat where
   lt a b := (Rat.lt a b) = true

tests/lean/run/Rat.lean

@@ -0,0 +1,27 @@
+import Std.Internal.Rat
+
+open Std.Internal
+
+/-- info: 1 -/
+#guard_msgs in
+#eval ((14:Rat)/11).floor
+
+/-- info: -2 -/
+#guard_msgs in
+#eval ((-14:Rat)/11).floor
+
+/-- info: 2 -/
+#guard_msgs in
+#eval ((14:Rat)/11).ceil
+
+/-- info: -1 -/
+#guard_msgs in
+#eval ((-14:Rat)/11).ceil
+
+/-- info: (5 : Rat)/2 -/
+#guard_msgs in
+#eval (1/6 : Rat) + 2 + 1/3
+
+/-- info: true -/
+#guard_msgs in
+#eval (1/6 : Rat) ≤ 1/3

tests/lean/run/grind_cutsat_le_2.lean

@@ -11,10 +11,10 @@ example (a b c d e : Int) :
 set_option trace.grind.cutsat.model true
 
 /--
-info: [grind.cutsat.model] c := 6
-[grind.cutsat.model] a := 13
+info: [grind.cutsat.model] c := 3
+[grind.cutsat.model] a := 7
 [grind.cutsat.model] b := 0
-[grind.cutsat.model] d := 4
+[grind.cutsat.model] d := 2
 -/
 #guard_msgs (info) in
 example (a b c d e : Int) :