diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
index 825e83e90d..2748321322 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
@@ -9,3 +9,8 @@
 >      (E M)))
 238d236
 < 
+270a269,272
+> 
+> (define small-counter-example
+>   (term ((λ (x int) x) (hd ((cons 1) nil)))))
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
index a959244c51..8c9439996c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
@@ -266,3 +266,7 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
+
+(define small-counter-example
+  (term ((λ (x int) x) (hd ((cons 1) nil)))))
+(test-equal (check small-counter-example) #f)