Server crash using `by decide`

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following code crashes the lean server:

set_option maxRecDepth 10000
example : ∀ n < 2000, n != 2025 := by decide

Steps to Reproduce

1. Run the code above in the online editor.

Expected behavior: Either success (as it happens if 2000 were to be replaced with smaller numbers), or a message stating that the recursion limit was exceeded.

Actual behavior:: The lean server crashes

Versions

Lean 4.20.0-nightly-2025-05-09

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal by decide example in the Lean online editor or against the reported nightly version, then compare it with smaller bounds. Done means the Lean server no longer crashes and instead succeeds or reports that the recursion limit was exceeded.