diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
index ff00687b27..1a8096e66c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
@@ -4,3 +4,8 @@
 > (define the-error "the ((cons number) v) value has been omitted")
 33d32
 <      ((cons v) v)
+270a270,273
+> 
+> (define small-counter-example
+>   (term ((cons 0) nil)))
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt
index 1dca9ca1b5..70dec7fdea 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt
@@ -267,3 +267,7 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
+
+(define small-counter-example
+  (term ((cons 0) nil)))
+(test-equal (check small-counter-example) #f)