diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
index dc826fa6aa..4cfe9af64c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
@@ -6,3 +6,7 @@
 <    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
 ---
 >    (λ (x_new τ) (subst (replace M x_new x_1) x_2 v))
+290a291,293
+> (define small-counter-example
+>   (term ((λ (x int) (λ (y int) y)) 1)))
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
index 98e1b8a2fa..74ca800935 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
@@ -288,3 +288,6 @@
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  (term ((λ (x int) (λ (y int) y)) 1)))
+(test-equal (check small-counter-example) #f)