Debugging infinite loop

Stream: lean4

[Jannis Limperg]

I have an example where Aesop loops infinitely (reported by @Adomas Baliuka):

import Mathlib.Data.Complex.Exponential

open Real (cos)

axiom MyDifferentiable : (ℝ → ℝ) → Prop
axiom MyDifferentiable.cos {f : ℝ → ℝ} :
  MyDifferentiable f → MyDifferentiable fun x => cos (f x)

example : MyDifferentiable fun y ↦ (Complex.cosh ↑(cos y)).re := by
  set_option maxHeartbeats 1 in
  aesop (add safe MyDifferentiable.cos) (rule_sets [-builtin,-default])

The problem is that I can't get Aesop to terminate even with maxHeartbeats 1, so I don't get any traces either. I've tried looking at a backtrace in gdb, but afaict it's just a large stack of isDefEq subroutines. Any ideas on how to debug this?