diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
index 964a460abb..76e869b770 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
@@ -6,3 +6,8 @@
 <    (int → ((list int) → (list int)))]
 ---
 >    (int → ((list int) → int))]
+270a271,274
+> 
+> (define small-counter-example
+>   (term ((+ 1) ((cons 1) nil))))
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
index 9446d9ad2b..9cdbc925f5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
@@ -268,3 +268,7 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
+
+(define small-counter-example
+  (term ((+ 1) ((cons 1) nil))))
+(test-equal (check small-counter-example) #f)