simp_all? ≠ simp_all and an old bug?

Stream: lean4

[Malvin Gattinger]

I stumbled into a case where simp_all affects my tactic state somehow, but when I change it to simp_all? the effect is different and it recommends a simp_all only ... that does fewer steps. I could not make an MWE easliy yet, but found this older Lean bug from February that is possibly related and apparently is now happening again? https://github.com/leanprover/lean4/issues/3519

Can someome tell me if I am misunderstanding something or if indeed this old bug is happening again with current Lean? (I ran into it while switching from 4.11 to 4.12).

example {P : Nat → Prop} : let x := 0; P x := by
  intro x
  simp_all? [x] -- Try this: simp_all only
  sorry

example {P : Nat → Prop} : let x := 0; P x := by
  intro x
  simp_all only -- simp_all made no progress
  sorry

(Or maybe it is normal that simp_all? behaves different than simp_all does?)

[Jannis Limperg]

This is not expected; the bug seems to be back. It should probably be reopened.