diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 68916e411a..c3d4549832 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -15,7 +15,7 @@ import Lean.Util.Profile
 namespace Lean.Meta
 
 register_builtin_option synthInstance.maxHeartbeats : Nat := {
-  defValue := 300
+  defValue := 500
   descr := "maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }