diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
index eb41c9fea5..28b9f96ba1 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
@@ -10,3 +10,10 @@
 <    (balance (c t_1 n_2 (ins n_1 t_2)))
 ---
 >    (c t_1 n_2 (ins n_1 t_2))
+301a302,307
+> (define small-counter-example
+>   (term (B (R E (num->n 0) E)
+>            (num->n 2)
+>            E)))
+> (test-equal (check small-counter-example) #f)
+> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
index 59301fd37f..f70058c005 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
@@ -5,3 +5,10 @@
 100,101d99
 <   [(balance (B (R (R t_1 n_1 t_2) n_2 t_3) n_3 t_4))
 <    (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
+301a300,305
+> (define small-counter-example
+>   (term (B (R E (num->n 1) E)
+>            (num->n 2)
+>            E)))
+> (test-equal (check small-counter-example) #f)
+> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
index ab349f07eb..beb2092ac7 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
@@ -6,3 +6,14 @@
 <   [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max (s n_bd))
 ---
 >   [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max n_bd)
+301a302,311
+> (define small-counter-example
+>   (term (B 
+>          (B 
+>           (R E (num->n 1) E)
+>           (num->n 2)
+>           (R E (num->n 3) E))
+>          (num->n 4)
+>          (R E (num->n 5) E))))
+> (test-equal (check small-counter-example) #f)
+> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
index 29bb95c3c3..650a892bad 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
@@ -299,6 +299,12 @@
         (generate-term rbtrees t #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  (term (B (R E (num->n 0) E)
+           (num->n 2)
+           E)))
+(test-equal (check small-counter-example) #f)
+
 (define fixed
   (term
    (;; 1 and 2
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
index 519e16d2f6..5f7b19856a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
@@ -297,6 +297,12 @@
         (generate-term rbtrees t #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  (term (B (R E (num->n 1) E)
+           (num->n 2)
+           E)))
+(test-equal (check small-counter-example) #f)
+
 (define fixed
   (term
    (;; 1 and 2
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
index 9787aeb134..b557baf65a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
@@ -299,6 +299,16 @@
         (generate-term rbtrees t #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  (term (B 
+         (B 
+          (R E (num->n 1) E)
+          (num->n 2)
+          (R E (num->n 3) E))
+         (num->n 4)
+         (R E (num->n 5) E))))
+(test-equal (check small-counter-example) #f)
+
 (define fixed
   (term
    (;; 1 and 2