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 7517af7c8c..eb41c9fea5 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
@@ -2,11 +2,11 @@
 < (define the-error "no-error")
 ---
 > (define the-error "ins does no rebalancing")
-90c90
+91c91
 <    (balance (c (ins n_1 t_1) n_2 t_2))
 ---
 >    (c (ins n_1 t_1) n_2 t_2)
-93c93
+94c94
 <    (balance (c t_1 n_2 (ins n_1 t_2)))
 ---
 >    (c t_1 n_2 (ins n_1 t_2))
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 c22f2e5f15..59301fd37f 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
@@ -2,6 +2,6 @@
 < (define the-error "no-error")
 ---
 > (define the-error "the first case is removed from balance")
-99,100d98
+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))]
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 fe8cb55bbe..ab349f07eb 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
@@ -2,7 +2,7 @@
 < (define the-error "no-error")
 ---
 > (define the-error "doesn't increment black depth in non-empty case")
-75c75
+76c76
 <   [(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)
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 166e8a869b..ebe6b87d82 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
@@ -3,7 +3,8 @@
 (define the-error "ins does no rebalancing")
 
 (require redex/reduction-semantics
-         racket/match)
+         racket/match
+         math/base)
 
 (provide (all-defined-out))
 
@@ -286,4 +287,7 @@
 
 (define (check t)
   (or (not t)
-      (ins-preserves-rb-tree t)))
\ No newline at end of file
+      (ins-preserves-rb-tree t)))
+
+(define (generate-enum-term)
+  (generate-term rbtrees t #:i-th (random-natural #e10e200)))
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 defbaddeae..ed21199c5c 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
@@ -3,7 +3,8 @@
 (define the-error "the first case is removed from balance")
 
 (require redex/reduction-semantics
-         racket/match)
+         racket/match
+         math/base)
 
 (provide (all-defined-out))
 
@@ -284,4 +285,7 @@
 
 (define (check t)
   (or (not t)
-      (ins-preserves-rb-tree t)))
\ No newline at end of file
+      (ins-preserves-rb-tree t)))
+
+(define (generate-enum-term)
+  (generate-term rbtrees t #:i-th (random-natural #e10e200)))
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 2a1e833415..73c75cc2d2 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
@@ -3,7 +3,8 @@
 (define the-error "doesn't increment black depth in non-empty case")
 
 (require redex/reduction-semantics
-         racket/match)
+         racket/match
+         math/base)
 
 (provide (all-defined-out))
 
@@ -286,4 +287,7 @@
 
 (define (check t)
   (or (not t)
-      (ins-preserves-rb-tree t)))
\ No newline at end of file
+      (ins-preserves-rb-tree t)))
+
+(define (generate-enum-term)
+  (generate-term rbtrees t #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
index e3ea0b288c..cd755db2c8 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
@@ -3,7 +3,8 @@
 (define the-error "no-error")
 
 (require redex/reduction-semantics
-         racket/match)
+         racket/match
+         math/base)
 
 (provide (all-defined-out))
 
@@ -286,4 +287,7 @@
 
 (define (check t)
   (or (not t)
-      (ins-preserves-rb-tree t)))
\ No newline at end of file
+      (ins-preserves-rb-tree t)))
+
+(define (generate-enum-term)
+  (generate-term rbtrees t #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
index f8ddc534cb..ca1ee4ab47 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
@@ -8,11 +8,11 @@
 11a10,11
 > (define the-error "the order of the variable clauses is swapped")
 > 
-102,103d101
+103,104d102
 <   [(subst x x M)
 <    M]
-105a104,105
+106a105,106
 >   [(subst x x M)
 >    M]
-253a254
+254a255
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
index f4ba9a249c..5a346d978b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
@@ -8,7 +8,7 @@
 11a10,11
 > (define the-error "only substitutes inside of hd constants")
 > 
-112,113c112,113
+113,114c113,114
 <   [(subst (c M) x M_x)
 <    (c (subst M x M_x))]
 ---
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
index 855b854288..0dd5753829 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
@@ -8,9 +8,9 @@
 11a10,11
 > (define the-error "substitutes rator into rand in application")
 > 
-115c115
+116c116
 <    ((subst M x M_x) (subst N x M_x))]
 ---
 >    ((subst M x M_x) (subst N x M))]
-253a254
+254a255
 > 
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 a66b387786..fb1ca997eb 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
@@ -8,14 +8,14 @@
 11a10,11
 > (define the-error "substitutes inside of λ that binds the sub variable")
 > 
-106,107d105
+107,108d106
 <   [(subst (λ (x τ) M) x M_x)
 <    (λ (x τ) M)]
-112,113d109
+113,114d110
 <   [(subst (c M) x M_x)
 <    (c (subst M x M_x))]
-115a112,113
+116a113,114
 >   [(subst (c M) x M_x)
 >    (c (subst M x M_x))]
-253a252
+254a253
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
index 6bf401e5bd..05e0301030 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
@@ -8,9 +8,9 @@
 11a10,11
 > (define the-error "swaps to/from expressions when recurring inside a constant")
 > 
-113c113
+114c114
 <    (c (subst M x M_x))]
 ---
 >    (c (subst M_x x M))]
-253a254
+254a255
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
index d35f2507bd..e4f442586c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
@@ -8,9 +8,9 @@
 11a10,11
 > (define the-error "swaps the order of the λ clauses")
 > 
-106,107d105
+107,108d106
 <   [(subst (λ (x τ) M) x M_x)
 <    (λ (x τ) M)]
-111a110,111
+112a111,112
 >   [(subst (λ (x τ) M) x M_x)
 >    (λ (x τ) M)]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
index 354ea1d0ad..4706728b62 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
@@ -11,8 +11,8 @@
 111a112,113
 >   [(subst (M N) x M_x)
 >    ((subst M_x x M) (subst N x M_x))]
-114,115d115
+115,116d116
 <   [(subst (M N) x M_x)
 <    ((subst M x M_x) (subst N x M_x))]
-253a254
+254a255
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
index 790abef466..2249a82dcc 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "the order of the variable clauses is swapped")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -272,3 +273,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
index 9df85e390e..808a1bfbcb 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "only substitutes inside of hd constants")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -271,3 +272,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
index 070013417a..4bde6efbf5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "substitutes rator into rand in application")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -272,3 +273,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
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 e67e63f38c..b0d5ca4032 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
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "substitutes inside of λ that binds the sub variable")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -270,3 +271,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
index f0eb07c5ae..df60e977a0 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "picks up the bound variable when recurring inside λ")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -250,8 +251,8 @@
             (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
     [`(typeof • ,M ,τ)
      M]
-    [#f #f]))
 
+    [#f #f]))
 (define (typed-generator)
   (let ([g (redex-generator stlc 
                             (typeof • M τ)
@@ -272,3 +273,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
index 5009497a50..18e40f2ad3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "swaps the bound var when recurring inside λ")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -250,8 +251,8 @@
             (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
     [`(typeof • ,M ,τ)
      M]
-    [#f #f]))
 
+    [#f #f]))
 (define (typed-generator)
   (let ([g (redex-generator stlc 
                             (typeof • M τ)
@@ -272,3 +273,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
index ef30fa0e99..259225ba0d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "swaps to/from expressions when recurring inside a constant")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -272,3 +273,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
index a9972bcc3d..ca89249d84 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "swaps the order of the λ clauses")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -271,3 +272,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
index c3701271d6..dcb7df79c2 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
@@ -3,12 +3,13 @@
 (require redex/reduction-semantics
          racket/list
          racket/match
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
-
 (define the-error "swaps to/from expressions when recurring in the rhs of app")
 
+
 (define-language stlc
   (M N ::= 
      (λ (x σ) M)
@@ -108,9 +109,9 @@
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
    (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
   [(subst (M N) x M_x)
    ((subst M_x x M) (subst N x M_x))]
+                                  (term x_1)))]
   [(subst (c M) x M_x)
    (c (subst M x M_x))]
   [(subst M x M_x)
@@ -272,3 +273,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
index 815f0874ca..50ef10aa3c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
@@ -5,7 +5,8 @@
 (require redex/reduction-semantics
          racket/match
          racket/list
-         racket/contract)
+         racket/contract
+         math/base)
 
 (provide (all-defined-out))
 
@@ -271,3 +272,6 @@
 	 (or 
           (equal? (car red-res) "error")
           (equal? t-type (type-check (car red-res))))))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (random-natural #e10e200)))