fix: missing withoutModifyingState at elabSimpConfig

src/Lean/Elab/Tactic/Simp.lean

@@ -31,7 +31,7 @@ def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Confi
     else
       return {}
   else
-    withLCtx {} {} <| withNewMCtxDepth <| Term.withSynthesize do
+    withoutModifyingState <| withLCtx {} {} <| Term.withSynthesize do
       let c ← Term.elabTermEnsuringType optConfig[3] (Lean.mkConst (if ctx then ``Meta.Simp.ConfigCtx else ``Meta.Simp.Config))
       if ctx then
         return (← evalSimpConfigCtx (← instantiateMVars c)).toConfig

tests/lean/run/simpDischargeLoop.lean

@@ -26,3 +26,20 @@ theorem double.inj' : double n = double m → n = m := by
       simp
       apply ih
       simp_all [double]
+
+theorem double.inj'' : double n = double m → n = m := by
+  intro h
+  induction n generalizing m with
+  | zero => cases m <;> trivial
+  | succ n ih =>
+    cases m with
+    | zero   => contradiction
+    | succ m =>
+      simp [ih, double]
+      simp [double] at h
+      apply ih h
+
+theorem double.inj''' : double n = double m → n = m := by
+  simp (config := { maxDischargeDepth := 2 })
+  simp (config := { maxSteps := 2000000 })
+  admit