diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index e46c0a65ea..4deac82cb6 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -159,7 +159,7 @@ where
       let init := r.expr
       modify fun s => { s with numSteps := s.numSteps + 1 }
       match (← pre r.expr) with
-      | Step.done r   => cacheResult cfg r
+      | Step.done r'  => cacheResult cfg (← mkEqTrans r r')
       | Step.visit r' =>
         let r ← mkEqTrans r r'
         let r ← mkEqTrans r (← simpStep r.expr)
diff --git a/tests/lean/run/simpLoopBug.lean b/tests/lean/run/simpLoopBug.lean
new file mode 100644
index 0000000000..d79ea0a686
--- /dev/null
+++ b/tests/lean/run/simpLoopBug.lean
@@ -0,0 +1 @@
+example (a : α) : ¬ some (some a) = some none := by simp