diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
index e388ce9f54..fb11874bd1 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
@@ -6,3 +6,12 @@
 <    (where x_new ,(variable-not-in (term (x_1 e x_2))
 ---
 >    (where x_new ,(variable-not-in (term e)
+290a291,298
+> (define small-counter-example
+>   ;; XXX I don't think this actually has an error because if x_1 !=
+>   ;; x_2 and v is a closed term, then what could go wrong? If we
+>   ;; remove the other special case of subst for λs that match, then it
+>   ;; would be bad, though.
+>   (term ((λ (x int) (λ (y int) (λ (y int) ((+ x) y))))
+>          1)))
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
index 88dc194034..2f48c00f3f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
@@ -288,3 +288,11 @@
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  ;; XXX I don't think this actually has an error because if x_1 !=
+  ;; x_2 and v is a closed term, then what could go wrong? If we
+  ;; remove the other special case of subst for λs that match, then it
+  ;; would be bad, though.
+  (term ((λ (x int) (λ (y int) (λ (y int) ((+ x) y))))
+         1)))
+(test-equal (check small-counter-example) #f)