chore: fix tests

Author: leodemoura

tests/lean/run/grind_canon_bug_2.lean

@@ -4,18 +4,18 @@ set_option warn.sorry false
 
 -- The following trace should contain only one `m[k]` and `(m.insert 1 3)[k]`
 /--
-trace: [grind.cutsat.model] k := 101
-[grind.cutsat.model] (ExtHashMap.filter (fun k x => decide (101 ≤ k)) (m.insert 1 3))[k] := 4
-[grind.cutsat.model] (m.insert 1 2)[k] := 4
-[grind.cutsat.model] (m.insert 1 3)[k] := 4
-[grind.cutsat.model] m[k] := 4
-[grind.cutsat.model] (m.insert 1 2).getKey k ⋯ := 101
-[grind.cutsat.model] m.getKey k ⋯ := 101
+trace: [grind.lia.model] k := 101
+[grind.lia.model] (ExtHashMap.filter (fun k x => decide (101 ≤ k)) (m.insert 1 3))[k] := 4
+[grind.lia.model] (m.insert 1 2)[k] := 4
+[grind.lia.model] (m.insert 1 3)[k] := 4
+[grind.lia.model] m[k] := 4
+[grind.lia.model] (m.insert 1 2).getKey k ⋯ := 101
+[grind.lia.model] m.getKey k ⋯ := 101
 -/
 #guard_msgs in
 example (m : ExtHashMap Nat Nat) :
     (m.insert 1 2).filter (fun k _ => k > 1000) = (m.insert 1 3).filter fun k _ => k > 100 := by
   ext1 k
-  set_option trace.grind.cutsat.model true in
+  set_option trace.grind.lia.model true in
   fail_if_success grind (splits := 4)
   sorry

tests/lean/run/grind_cutsat_auto.lean

@@ -29,14 +29,14 @@ abbrev problem (x y z w v : Int) : Prop :=
   (y ≥ -10)
 
 /--
-trace: [grind.cutsat.model] x := 121
-[grind.cutsat.model] y := -10
-[grind.cutsat.model] z := -34
-[grind.cutsat.model] w := 0
-[grind.cutsat.model] v := 1
+trace: [grind.lia.model] x := 121
+[grind.lia.model] y := -10
+[grind.lia.model] z := -34
+[grind.lia.model] w := 0
+[grind.lia.model] v := 1
 -/
 #guard_msgs (trace) in
-set_option trace.grind.cutsat.model true in
+set_option trace.grind.lia.model true in
 example (x y z w v : Int) : problem x y z w v → False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_cooper.lean

@@ -18,11 +18,11 @@ abbrev problem₁ [∀ n, OfNat α n] [Neg α] [Mul α] [Sub α] [Add α] [LE α
   7*x - 9*y ≤ 4
 
 /--
-trace: [grind.cutsat.model] x := 241/154
-[grind.cutsat.model] y := 1
+trace: [grind.lia.model] x := 241/154
+[grind.lia.model] y := 1
 -/
 #guard_msgs (trace) in
-set_option trace.grind.cutsat.model true in
+set_option trace.grind.lia.model true in
 example (x y : Int) : problem₁ x y → False := by
   fail_if_success grind +qlia -- Rational counterexamples allowed
   sorry

tests/lean/run/grind_cutsat_diseq_1.lean

@@ -2,11 +2,11 @@ module
 set_option grind.debug true
 open Int.Linear
 
-set_option trace.grind.cutsat.assert true
+set_option trace.grind.lia.assert true
 
 /--
-trace: [grind.cutsat.assert] a + b + 1 ≤ 0
-[grind.cutsat.assert] a + -1*b ≠ 0
+trace: [grind.lia.assert] a + b + 1 ≤ 0
+[grind.lia.assert] a + -1*b ≠ 0
 -/
 #guard_msgs (trace) in
 example (a b : Int) : a + b < 0 → a ≠ b → False := by
@@ -17,62 +17,62 @@ example (a b : Int) : a ≠ b → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] a + -1*b ≠ 0
-[grind.cutsat.assert] a + b + 1 ≤ 0
+trace: [grind.lia.assert] a + -1*b ≠ 0
+[grind.lia.assert] a + b + 1 ≤ 0
 -/
 #guard_msgs (trace) in
 example (a b : Int) : a ≠ b → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] a + -1*b ≠ 0
-[grind.cutsat.assert] a + b + 1 ≤ 0
+trace: [grind.lia.assert] a + -1*b ≠ 0
+[grind.lia.assert] a + b + 1 ≤ 0
 -/
 #guard_msgs (trace) in
 example (a b c : Int) : a ≠ c → c = b → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] a + -1*b ≠ 0
-[grind.cutsat.assert] a + b + 1 ≤ 0
+trace: [grind.lia.assert] a + -1*b ≠ 0
+[grind.lia.assert] a + b + 1 ≤ 0
 -/
 #guard_msgs (trace) in
 example (a b c d : Int) : d ≠ c → c = b → a = d → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] a + b + 1 ≤ 0
-[grind.cutsat.assert] a + -1*b ≠ 0
+trace: [grind.lia.assert] a + b + 1 ≤ 0
+[grind.lia.assert] a + -1*b ≠ 0
 -/
 #guard_msgs (trace) in
 example (a b c d : Int) : d ≠ c → a = d → a + b < 0 → c = b → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] a + b + 1 ≤ 0
-[grind.cutsat.assert] a + -1*b ≠ 0
-[grind.cutsat.assert] e + -1*b = 0
-[grind.cutsat.assert] -1*e + 1 ≤ 0
+trace: [grind.lia.assert] a + b + 1 ≤ 0
+[grind.lia.assert] a + -1*b ≠ 0
+[grind.lia.assert] e + -1*b = 0
+[grind.lia.assert] -1*e + 1 ≤ 0
 -/
 #guard_msgs (trace) in
 example (a b c d e : Int) : d ≠ c → a = d → a + b < 0 → c = b → c = e → e > 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] -1*e + 1 ≤ 0
-[grind.cutsat.assert] b + -1*e = 0
-[grind.cutsat.assert] a + -1*e ≠ 0
-[grind.cutsat.assert] a + b + 1 ≤ 0
+trace: [grind.lia.assert] -1*e + 1 ≤ 0
+[grind.lia.assert] b + -1*e = 0
+[grind.lia.assert] a + -1*e ≠ 0
+[grind.lia.assert] a + b + 1 ≤ 0
 -/
 #guard_msgs (trace) in
 example (a b c d e : Int) : d ≠ c → a = d → c = b → c = e → e > 0 → a + b < 0 → False := by
   (fail_if_success grind); sorry
 
 /--
-trace: [grind.cutsat.assert] -1*e + 1 ≤ 0
-[grind.cutsat.assert] b + -1*e = 0
-[grind.cutsat.assert] a + b + 1 ≤ 0
-[grind.cutsat.assert] a + -1*e ≠ 0
+trace: [grind.lia.assert] -1*e + 1 ≤ 0
+[grind.lia.assert] b + -1*e = 0
+[grind.lia.assert] a + b + 1 ≤ 0
+[grind.lia.assert] a + -1*e ≠ 0
 -/
 #guard_msgs (trace) in
 example (a b c d e : Int) : a = d → c = b → c = e → e > 0 → a + b < 0 → d ≠ c → False := by

tests/lean/run/grind_cutsat_diseq_2.lean

@@ -12,16 +12,16 @@ theorem ex₃ (a b c : Int) : a + b + c = 0 → a = c → b = 4 → c = -2 := by
   grind
 
 /--
-trace: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
-[grind.cutsat.assert] -1*「0」 = 0
-[grind.cutsat.assert] 「a + -2 * b + -2 * c」 = 0
-[grind.cutsat.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0
-[grind.cutsat.assert] 「a + -2 * b + -2 * d」 ≠ 0
-[grind.cutsat.assert] -1*d + c = 0
-[grind.cutsat.assert] 0 ≠ 0
+trace: [grind.lia.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
+[grind.lia.assert] -1*「0」 = 0
+[grind.lia.assert] 「a + -2 * b + -2 * c」 = 0
+[grind.lia.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0
+[grind.lia.assert] 「a + -2 * b + -2 * d」 ≠ 0
+[grind.lia.assert] -1*d + c = 0
+[grind.lia.assert] 0 ≠ 0
 -/
 #guard_msgs (trace) in
-set_option trace.grind.cutsat.assert true in
+set_option trace.grind.lia.assert true in
 theorem ex₄ (a b c d : Int) : a = 2*b + 2*c → a - 2*b - 2*d ≠ 0 → c ≠ d := by
   grind
 

tests/lean/run/grind_cutsat_div_1.lean

@@ -21,56 +21,56 @@ theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3 
 #print ex₄
 
 /--
-trace: [grind.debug.cutsat.search.assign] a := 1
-[grind.debug.cutsat.search.assign] b := 0
+trace: [grind.debug.lia.search.assign] a := 1
+[grind.debug.lia.search.assign] b := 0
 -/
 #guard_msgs (trace) in -- finds the model without any backtracking
-set_option trace.grind.debug.cutsat.search.assign true in
+set_option trace.grind.debug.lia.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by
   fail_if_success grind
   sorry
 
 /--
-trace: [grind.cutsat.assert] 2 ∣ a + 3
-[grind.cutsat.assert] 3 ∣ a + 3*b + -4
-[grind.debug.cutsat.search.assign] a := 1
-[grind.debug.cutsat.search.assign] b := 0
+trace: [grind.lia.assert] 2 ∣ a + 3
+[grind.lia.assert] 3 ∣ a + 3*b + -4
+[grind.debug.lia.search.assign] a := 1
+[grind.debug.lia.search.assign] b := 0
 -/
 #guard_msgs (trace) in
-set_option trace.grind.cutsat.assert true in
-set_option trace.grind.debug.cutsat.search.assign true in
+set_option trace.grind.lia.assert true in
+set_option trace.grind.debug.lia.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by
   fail_if_success grind
   sorry
 
 /--
-trace: [grind.debug.cutsat.search.assign] a := 1
-[grind.debug.cutsat.search.assign] b := 15
+trace: [grind.debug.lia.search.assign] a := 1
+[grind.debug.lia.search.assign] b := 15
 -/
 #guard_msgs (trace) in
-set_option trace.grind.debug.cutsat.search.assign true in
+set_option trace.grind.debug.lia.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b < 18): False := by
   fail_if_success grind
   sorry
 
 /--
-trace: [grind.debug.cutsat.search.assign] a := 1
-[grind.debug.cutsat.search.assign] b := 12
+trace: [grind.debug.lia.search.assign] a := 1
+[grind.debug.lia.search.assign] b := 12
 -/
 #guard_msgs (trace) in
-set_option trace.grind.debug.cutsat.search.assign true in
+set_option trace.grind.debug.lia.search.assign true in
 example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): False := by
   fail_if_success grind
   sorry
 
 /--
-trace: [grind.debug.cutsat.search.assign] f 0 := 11
-[grind.debug.cutsat.search.assign] f 1 := 2
-[grind.debug.cutsat.search.assign] 「1」 := 1
-[grind.debug.cutsat.search.assign] 「0」 := 0
+trace: [grind.debug.lia.search.assign] f 0 := 11
+[grind.debug.lia.search.assign] f 1 := 2
+[grind.debug.lia.search.assign] 「1」 := 1
+[grind.debug.lia.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
-set_option trace.grind.debug.cutsat.search.assign true in
+set_option trace.grind.debug.lia.search.assign true in
 example (f : Int → Int) (_ : 2 ∣ f 0 + 3) (_ : 3 ∣ f 0 + f 1 - 4) (_ : f 0 ≥ 11): False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_div_mod.lean

@@ -12,11 +12,11 @@ example (x y : Int) : x % 2 + y = 3 → x = 5 → y = 2 := by
   grind
 
 /--
-trace: [grind.cutsat.model] x := 5
-[grind.cutsat.model] y := 2
+trace: [grind.lia.model] x := 5
+[grind.lia.model] y := 2
 -/
 #guard_msgs (trace) in
-set_option trace.grind.cutsat.model true in
+set_option trace.grind.lia.model true in
 example (x y : Int) : x % 2 + y = 3 → x ≤ 5 → x > 4 → y = 1 := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_eq_1.lean

@@ -3,12 +3,12 @@ set_option grind.debug true
 open Int.Linear
 
 /--
-trace: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
-[grind.cutsat.assert] -1*「0」 = 0
-[grind.cutsat.assert] 「b + f a + 1」 = 0
+trace: [grind.lia.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
+[grind.lia.assert] -1*「0」 = 0
+[grind.lia.assert] 「b + f a + 1」 = 0
 -/
 #guard_msgs (trace) in
-set_option trace.grind.cutsat.assert true in
+set_option trace.grind.lia.assert true in
 example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2)  : False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_le_1.lean

@@ -2,11 +2,11 @@ module
 set_option grind.debug true
 
 /--
-trace: [grind.debug.cutsat.search.assign] b := -1
-[grind.debug.cutsat.search.assign] a := 3
+trace: [grind.debug.lia.search.assign] b := -1
+[grind.debug.lia.search.assign] a := 3
 -/
 #guard_msgs (trace) in
-set_option trace.grind.debug.cutsat.search.assign true in
+set_option trace.grind.debug.lia.search.assign true in
 example (a b : Int) (h₁ : a ≤ 3) (h₂ : a > 2) (h₃ : a + b < 3) : False := by
   fail_if_success grind
   sorry

tests/lean/run/grind_cutsat_le_2.lean

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