diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean
index 131283467919f..7f84a6b567d16 100644
--- a/Mathlib/Testing/SlimCheck/Testable.lean
+++ b/Mathlib/Testing/SlimCheck/Testable.lean
@@ -509,8 +509,8 @@ open Lean
 quantifiers and add `NamedBinder` annotations next to them. -/
 partial def addDecorations (e : Expr) : MetaM Expr :=
   Meta.transform e fun expr => do
-    if not (← Meta.inferType e).isProp then
-      return .continue
+    if not (← Meta.inferType expr).isProp then
+      return .done expr
     else if let Expr.forallE name type body data := expr then
       let newType ← addDecorations type
       let newBody ← Meta.withLocalDecl name data type fun fvar => do
diff --git a/test/slim_check.lean b/test/slim_check.lean
index bef7c77904b48..aa764cc89305f 100644
--- a/test/slim_check.lean
+++ b/test/slim_check.lean
@@ -413,6 +413,21 @@ issue: ⋯ does not hold
     exact test_sorry
   trivial
 
+open scoped BigOperators in
+example (n : ℕ) : true := by
+  have : ∑ f : Unit → Fin (n + 1), f () = 0 := by
+    success_if_fail_with_msg "
+===================
+Found problems!
+n := 1
+issue: 1 = 0 does not hold
+(0 shrinks)
+-------------------
+"
+      slim_check (config := { randomSeed := some 257 })
+    exact test_sorry
+  trivial
+
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20question/near/412709012
 open scoped BigOperators in
 /--