chore: fix test

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean

@@ -94,6 +94,6 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
   for (e, v) in model do
     unless isInterpretedTerm e do
       r := r.push (e, v)
-  return r
+  return r.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
 
 end Lean.Meta.Grind.Arith.Cutsat

tests/lean/run/grind_cutsat_cooper.lean

@@ -1,3 +1,4 @@
+import Std.Internal.Rat
 set_option grind.warning false
 
 example (x y : Int) :
@@ -10,3 +11,47 @@ example (x y : Int) :
 
 example (x : Int) : 100 ≤ x → x ≤ 10000 → 20000 ∣ 3*x → False := by
   grind
+
+abbrev problem₁ [∀ n, OfNat α n] [Neg α] [Mul α] [Sub α] [Add α] [LE α] (x y : α) : Prop :=
+  27 ≤ 11*x + 13*y ∧
+  11*x + 13*y ≤ 45 ∧
+  -10 ≤ 7*x - 9*y ∧
+  7*x - 9*y ≤ 4
+
+/--
+info: [grind.cutsat.model] x := 241/154
+[grind.cutsat.model] y := 1
+-/
+#guard_msgs (info) in
+set_option trace.grind.cutsat.model true in
+example (x y : Int) : problem₁ x y → False := by
+  fail_if_success grind +qlia -- Rational counterexamples allowed
+  sorry
+
+/-- info: true -/
+#guard_msgs (info) in
+open Std.Internal in
+#eval problem₁ (241/154 : Rat) (1 : Rat)
+
+theorem ex₁ (x y : Int) :
+    27 ≤ 13*x + 11*y → 13*x + 11*y ≤ 30 →
+    -10 ≤ 9*x - 7*y → 9*x - 7*y ≤ 4 → False := by
+  grind
+
+theorem ex₂ (x y : Int) :
+    27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 →
+    -10 ≤ 7*x - 9*y → 7*x - 9*y ≤ 4 → False := by
+  grind
+
+theorem ex₃ (x y : Int) :
+    5 ≤ x + y → x + 2*y ≤ 14 → 7 ∣ x → 4 ∣ y → y ≥ 4 → False := by
+  grind
+
+theorem ex₄ (x y : Int) :
+    5 ≤ 2*x + y → 3*x + 2*y ≤ 14 → 7 ∣ x → 4 ∣ y → y ≥ 4 → False := by
+  grind
+
+#print ex₁
+#print ex₂
+#print ex₃
+#print ex₄

tests/lean/run/grind_cutsat_le_2.lean

@@ -11,9 +11,9 @@ example (a b c d e : Int) :
 set_option trace.grind.cutsat.model true
 
 /--
-info: [grind.cutsat.model] c := 3
-[grind.cutsat.model] a := 7
+info: [grind.cutsat.model] a := 7
 [grind.cutsat.model] b := 0
+[grind.cutsat.model] c := 3
 [grind.cutsat.model] d := 2
 -/
 #guard_msgs (info) in
@@ -25,9 +25,9 @@ example (a b c d e : Int) :
   (fail_if_success grind); sorry
 
 /--
-info: [grind.cutsat.model] c := -9
-[grind.cutsat.model] a := 17
+info: [grind.cutsat.model] a := 17
 [grind.cutsat.model] b := -9
+[grind.cutsat.model] c := -9
 -/
 #guard_msgs (info) in
 example (a b c : Int) :