diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff
index 9a2d852da5..f49b67f0de 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff
@@ -6,3 +6,7 @@
 <    (∀ a (a → ((list a) → (list a))))]
 ---
 >    (∀ a (a → ((list a) → a)))]
+294a295,297
+> (define small-counter-example
+>   (term ((+ 1) (([cons @ int] 1) [nil @ int]))))
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
index c63183ad50..5b6dc7488e 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
@@ -292,3 +292,6 @@
         (generate-term poly-stlc M #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  (term ((+ 1) (([cons @ int] 1) [nil @ int]))))
+(test-equal (check small-counter-example) #f)