diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean
index a3ce37dbae..b72ecd4582 100644
--- a/tests/lean/run/typeclass_coerce.lean
+++ b/tests/lean/run/typeclass_coerce.lean
@@ -71,7 +71,7 @@ axiom Top (α : Type) (n : Nat) : Type
 #print "-----"
 
 set_option synthInstance.maxSize 256
-set_option synthInstance.maxHeartbeats 5000
+set_option synthInstance.maxHeartbeats 500000
 
 #synth HasCoerce (Top Unit Nat.zero)
                  (Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ)
diff --git a/tests/lean/run/typeclass_diamond.lean b/tests/lean/run/typeclass_diamond.lean
index 403a06a2a5..99a184edce 100644
--- a/tests/lean/run/typeclass_diamond.lean
+++ b/tests/lean/run/typeclass_diamond.lean
@@ -27,7 +27,7 @@ class Top (n : Nat) : Type := (u : Unit := ())
 instance Top₁ToTop (n : Nat) [Top₁ n] : Top n := {}
 instance Top₂ToTop (n : Nat) [Top₂ n] : Top n := {}
 
-set_option synthInstance.maxHeartbeats 500
+set_option synthInstance.maxHeartbeats 5000
 
 #synth Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ