diff --git a/Lean/Egg/Tests/BVar Index Correction.lean b/Lean/Egg/Tests/BVar Index Correction.lean
index f5cc2910c9..4eb3d6ea19 100644
--- a/Lean/Egg/Tests/BVar Index Correction.lean	
+++ b/Lean/Egg/Tests/BVar Index Correction.lean	
@@ -23,7 +23,7 @@ example : False := by
   contradiction
 
 set_option egg.shiftCapturedBVars true in
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example : (fun x => (x, 5).fst) = (fun _ : Nat => (fun x => x) 1) := by
   egg [thm₁]
diff --git a/Lean/Egg/Tests/Block Invalid Matches.lean b/Lean/Egg/Tests/Block Invalid Matches.lean
index 3da40b6adb..de6d0869a0 100644
--- a/Lean/Egg/Tests/Block Invalid Matches.lean	
+++ b/Lean/Egg/Tests/Block Invalid Matches.lean	
@@ -35,7 +35,7 @@ theorem thm₂ : ∀ x y : Nat, x = (fun _ => x) y :=
 
 -- This test covers Condition (1) of valid matches.
 set_option egg.blockInvalidMatches true in
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example : (fun x => x) = (fun _ : Nat => (fun x => x) 1) := by
   egg [thm₂]
diff --git a/Lean/Egg/Tests/Builtins.lean b/Lean/Egg/Tests/Builtins.lean
index 463c39801b..03d59e2c24 100644
--- a/Lean/Egg/Tests/Builtins.lean
+++ b/Lean/Egg/Tests/Builtins.lean
@@ -1,6 +1,6 @@
 import Egg
 
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 set_option egg.builtins false in
 example : Nat.succ a = a + 1 := by
@@ -10,7 +10,7 @@ set_option egg.builtins true in
 example : Nat.succ a = a + 1 := by
   egg
 
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 set_option egg.builtins false in
 example (a : Nat) (h₁ : a < b → 1 = 2) (h₂ : b > a) : 1 = 2 := by
@@ -21,7 +21,7 @@ example (a : Nat) (h₁ : a < b → 1 = 2) (h₂ : b > a) : 1 = 2 := by
 -- example (a : Nat) (h₁ : a < b → 1 = 2) (h₂ : b > a) : 1 = 2 := by
 --   egg [h₁; h₂]
 
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 set_option egg.builtins false in
 example (a : Nat) (h₁ : a ≤ b → 1 = 2) (h₂ : b ≥ a) : 1 = 2 := by
diff --git a/Lean/Egg/Tests/Conditional.lean b/Lean/Egg/Tests/Conditional.lean
index fef8537f0b..d9f9e85962 100644
--- a/Lean/Egg/Tests/Conditional.lean
+++ b/Lean/Egg/Tests/Conditional.lean
@@ -1,6 +1,6 @@
 import Egg
 
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example (h : x ∧ y → 1 = 2) : 1 = 2 := by
   egg [h]
@@ -36,7 +36,7 @@ example (h₁ : ∀ n, n > 2 → n > 3 → n = x) (h₃ : 4 > 3) (h₂ : 4 > 2)
 example {a : Nat} (h : a < b) : a % b = a := by
   egg [Nat.mod_eq_of_lt; h]
 
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example {x : Nat} (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by
   egg [h₁, h₂]
diff --git a/Lean/Egg/Tests/Crash 2.lean b/Lean/Egg/Tests/Crash 2.lean
index c83bc30293..34920b614a 100644
--- a/Lean/Egg/Tests/Crash 2.lean	
+++ b/Lean/Egg/Tests/Crash 2.lean	
@@ -2,7 +2,7 @@ import Egg
 
 -- This used to crash, before we changed proof erasure to encode the type of propositions.
 
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size)
     (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
diff --git a/Lean/Egg/Tests/Eta.lean b/Lean/Egg/Tests/Eta.lean
index 433a9e6304..f8fe56a7be 100644
--- a/Lean/Egg/Tests/Eta.lean
+++ b/Lean/Egg/Tests/Eta.lean
@@ -5,7 +5,7 @@ set_option egg.genEtaRw true
 set_option egg.genBetaRw false
 
 set_option egg.genEtaRw false in
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example : (fun x => Nat.succ x) = Nat.succ := by
   egg
@@ -45,7 +45,7 @@ example : (eta 50 Nat.succ Nat) = Nat.succ := by
   egg
 
 set_option egg.genEtaRw false in
-/-- error: egg failed to prove the goal (reached time limit) -/
+/-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ x).add a = 0 := by
   egg [h]
diff --git a/Lean/Egg/Tests/Rudi.lean b/Lean/Egg/Tests/Rudi.lean
index a4f1cebf1b..56de0af747 100644
--- a/Lean/Egg/Tests/Rudi.lean
+++ b/Lean/Egg/Tests/Rudi.lean
@@ -2,9 +2,3 @@ import Egg
 
 example : (fun x => (fun t _y => t) (fun z => x z)) = (fun (x : α → α) (_y : α) => x) := by
   egg
-
-variable (m : Type → Type) (map : {α β : Type _} → (α → β) → m α → m β)
-
-example (f : α → β → β) (g : β → β) (arg : m β) (ω : α) :
-    map (f ω) (map g arg) = map (fun x => (f ω) (g x)) arg := by
-  sorry -- Which rewrites should prove this?
diff --git a/Lean/Egg/Tests/Equational.lean b/Lean/Egg/Tests/ZZ Equational.lean
similarity index 100%
rename from Lean/Egg/Tests/Equational.lean
rename to Lean/Egg/Tests/ZZ Equational.lean