diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 377a956762..f17fb995aa 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -194,19 +194,11 @@ protected def saveState : TermElabM SavedState := do
 
 def SavedState.restore (s : SavedState) : TermElabM Unit := do
   let traceState ← getTraceState -- We never backtrack trace message
-  -- We also preserve `TacticInfo` nodes to be able to display the tactic state of broken tactic scripts
-  let infoStateNew := (← get).infoState
-  let oldInfoSize  := s.elab.infoState.trees.size
+  let infoState := (← get).infoState -- We also do not backtrack the info nodes
   s.meta.restore
   set s.elab
   setTraceState traceState
-  -- Add new `TacticInfo` nodes back to restored `infoState`
-  modify fun s => { s with
-    infoState.trees := infoStateNew.trees.foldl (init := s.infoState.trees) (start := oldInfoSize) fun trees info =>
-      match info with
-      | InfoTree.node (Info.ofTacticInfo _) _ => trees.push info
-      | _ => trees
-  }
+  modify fun s => { s with infoState := infoState }
 
 instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState
diff --git a/tests/lean/interactive/haveInfo.lean b/tests/lean/interactive/haveInfo.lean
new file mode 100644
index 0000000000..f71cc79168
--- /dev/null
+++ b/tests/lean/interactive/haveInfo.lean
@@ -0,0 +1,6 @@
+example : False := by
+  have True by
+    skip
+  --^ $/lean/plainGoal
+    skip
+  admit
diff --git a/tests/lean/interactive/haveInfo.lean.expected.out b/tests/lean/interactive/haveInfo.lean.expected.out
new file mode 100644
index 0000000000..803419d4f7
--- /dev/null
+++ b/tests/lean/interactive/haveInfo.lean.expected.out
@@ -0,0 +1,3 @@
+{"textDocument": {"uri": "file://haveInfo.lean"},
+ "position": {"line": 2, "character": 4}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}