diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt
index 080e8aef63..dc6904896a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt
@@ -942,8 +942,8 @@
   (judgment-holds (tc · · ,e t)))
 
 
-(define (generate-enum-term)
-  (generate-term abort-lang e #:i-th (pick-an-index 0.125)))
+(define (generate-enum-term [p-value 0.125])
+  (generate-term abort-lang e #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (define index -1)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt
index 59a1885920..7e4e2905a4 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt
@@ -940,8 +940,8 @@
 
 
 
-(define (generate-enum-term)
-  (generate-term abort-lang e #:i-th (pick-an-index 0.125)))
+(define (generate-enum-term [p-value 0.125])
+  (generate-term abort-lang e #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (define index -1)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt
index f9efb4f10f..c40ced8351 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt
@@ -940,8 +940,8 @@
 
 
 
-(define (generate-enum-term)
-  (generate-term abort-lang e #:i-th (pick-an-index 0.125)))
+(define (generate-enum-term [p-value 0.125])
+  (generate-term abort-lang e #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (define index -1)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt
index d9b8cd1e41..11e6bf5f2d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt
@@ -937,8 +937,8 @@
 (define (type-check e)
   (judgment-holds (tc · · ,e t)))
 
-(define (generate-enum-term)
-  (generate-term abort-lang e #:i-th (pick-an-index 0.125)))
+(define (generate-enum-term [p-value 0.125])
+  (generate-term abort-lang e #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (define index -1)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
index b7f2afabb3..28947f9521 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
@@ -518,8 +518,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
index 4683930a75..1433eeaa73 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
@@ -513,8 +513,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
index 721d20ee72..830cab1342 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
@@ -518,8 +518,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
index fbc6b945d1..2bc9fe185c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
@@ -520,8 +520,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
index 9389f8bab5..80bb752eea 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
@@ -520,8 +520,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
index 07024185dd..bbcd97f6e5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
@@ -518,8 +518,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
index 12fb6d34b1..734132372f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
@@ -519,8 +519,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
index ada35ec3dc..2d22cfd265 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
@@ -518,8 +518,8 @@ Generators
          M]
         [#f #f]))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt
index 54a9a1ddcb..fb901727e5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt
@@ -433,8 +433,8 @@
      p]
     [#f #f]))
 
-(define (generate-enum-term)
-  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
+(define (generate-enum-term [p-value 0.5])
+  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt
index be0844ba2b..93409f9b5b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt
@@ -433,8 +433,8 @@
      p]
     [#f #f]))
 
-(define (generate-enum-term)
-  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
+(define (generate-enum-term [p-value 0.5])
+  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt
index 4c2cbbb025..3f04680bbc 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt
@@ -429,8 +429,8 @@
      p]
     [#f #f]))
 
-(define (generate-enum-term)
-  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
+(define (generate-enum-term [p-value 0.5])
+  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt
index 6f3a9ffcd9..6de280571a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt
@@ -429,8 +429,8 @@
      p]
     [#f #f]))
 
-(define (generate-enum-term)
-  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index 0.5)))
+(define (generate-enum-term [p-value 0.5])
+  (generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/p-calc.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/p-calc.rkt
new file mode 100644
index 0000000000..8d988cbc2a
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/p-calc.rkt
@@ -0,0 +1,125 @@
+#lang racket
+
+(require math/statistics)
+
+#|
+
+From the command line, for example:
+racket p-calc.rkt stlc
+
+Finds a p-value such that the average size of generated terms 
+is within 0.5 of the maximum counterexample size for that model.
+This target size will likely need to change.
+(Also makes sure that the standard error in the mean is less than 0.5.)
+
+Doesn't work well with rbtrees, which has an extremely large standard deviation.
+
+|#
+
+(module+
+    main
+  (command-line
+   #:args (dir)
+   (printf "p-value: ~s\n" 
+           (exact->inexact 
+            (model-p-value 
+             (string->symbol 
+              (string-append
+               "redex/examples/benchmark/"
+               dir)))))))
+
+(define (model-p-value mod-path)
+  (define target-size (max-cexp-size mod-path))
+  (define base (test-mod-path->base mod-path))
+  (define enum-gen (dynamic-require base 'generate-enum-term))
+  (find-p-value enum-gen target-size))
+
+(define (find-p-value enum-gen target-size)
+  (fpv-search enum-gen target-size 0 1 100))
+
+(define (fpv-search gen size l r num-samples)
+  (define mid (/ (+ l r) 2))
+  (printf "Target: ~s, current interval: (~s ~s)\n" size l r)
+  (define-values (m e) (sample-sizes gen mid num-samples))
+  (printf "At ~s, mean: ~s, stderr: ~s, with ~s samples\n" mid m e num-samples)
+  (cond
+    [(e . > . 0.5)
+     (fpv-search gen size l r (* num-samples 2))]
+    [((abs (- size m)) . < . 0.5)
+     mid]
+    [(m . < . size)
+     (fpv-search gen size l mid num-samples)]
+    [(m . > . size)
+     (fpv-search gen size mid r num-samples)]))  
+
+(define (sample-sizes enum-gen p-value num-samples)
+  (define sizes
+    (for/list ([_ (in-range num-samples)])
+      (count-size
+       (enum-gen p-value))))
+  (values (mean sizes)
+          (/ (stddev sizes) 
+             (sqrt num-samples))))
+
+(module+
+    test
+  (require rackunit)
+  (define stlc-path 'redex/examples/benchmark/stlc)
+  (define stlc-base 'redex/examples/benchmark/stlc/stlc-base)
+  (define stlc-gen (dynamic-require stlc-base 'generate-enum-term))
+  (define-values (m e) (sample-sizes stlc-gen 0.03125 100))
+  (check-not-false
+   ((abs (- m 15)) . < . (* 2 e))))
+
+(define max-bug-num 20)
+  
+(define (test-paths t-m-p)
+  (for/list ([n (in-range 1 max-bug-num)])
+    (string->symbol
+     (string-append
+      (test-mod-path->stem t-m-p)
+      (number->string n)))))
+
+(define (test-mod-path->base t-m-p)
+  (string->symbol
+   (string-append
+    (test-mod-path->stem t-m-p)
+    "base")))
+
+(define (test-mod-path->stem t-m-p)
+  (define tms (symbol->string t-m-p))
+  (define name (second (regexp-match #rx"^.*/(.*)$" tms)))
+  (string-append tms "/" name "-"))
+
+(define (cexps t-m-p)
+  (filter 
+   values
+   (map
+    (λ (p)
+      (with-handlers
+          ([exn:fail:filesystem?
+            (λ (e)
+              (if (regexp-match? #rx"No such file"
+                                 (exn-message e))
+                  #f
+                  (raise e)))])
+        (dynamic-require p 'small-counter-example)))
+    (test-paths t-m-p))))
+
+(define (count-size l)
+  (cond
+    [(list? l) (apply + 1 (map count-size l))]
+    [else 1]))
+
+(define (cexp-sizes t-m-p)
+  (map count-size (cexps t-m-p)))
+
+(define (max-cexp-size t-m-p)
+  (apply max (cexp-sizes t-m-p)))
+
+(module+
+    test
+  (check-equal? (test-mod-path->stem stlc-path)
+                "redex/examples/benchmark/stlc/stlc-")
+  (define stlc-size (max-cexp-size stlc-path))
+  (check-equal? stlc-size 15))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
index 862d09c344..9840cf8863 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
index 2a2fd63d66..ffacfdf9e4 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
@@ -280,8 +280,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
index 69187abaed..9d2c21e920 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 5b6dc7488e..a76e72d7b1 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
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
index 631005b6c2..3bc509d3e3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
index 43760e0b97..93184fbb46 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
index 842f2e0b90..3515452a0a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
@@ -281,8 +281,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
index a69a035628..c54619131b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
index 5939fa1db9..227ec884aa 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
index b98d3ec0e2..d92460e3c8 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
@@ -282,8 +282,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term poly-stlc M #:i-th (pick-an-index 0.065)))
+(define (generate-enum-term [p-value 0.065])
+  (generate-term poly-stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 10160d1eb1..09cd875456 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
@@ -289,8 +289,8 @@
   (or (not t)
       (implies (type-check t) (ins-preserves-rb-tree t))))
 
-(define (generate-enum-term)
-  (generate-term rbtrees t #:i-th (pick-an-index 0.25)))
+(define (generate-enum-term [p-value 0.25])
+  (generate-term rbtrees t #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 4f3025bb64..b32337b575 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
@@ -287,8 +287,8 @@
   (or (not t)
       (implies (type-check t) (ins-preserves-rb-tree t))))
 
-(define (generate-enum-term)
-  (generate-term rbtrees t #:i-th (pick-an-index 0.25)))
+(define (generate-enum-term [p-value 0.25])
+  (generate-term rbtrees t #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 611c47d003..9cfa295030 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
@@ -289,8 +289,8 @@
   (or (not t)
       (implies (type-check t) (ins-preserves-rb-tree t))))
 
-(define (generate-enum-term)
-  (generate-term rbtrees t #:i-th (pick-an-index 0.25)))
+(define (generate-enum-term [p-value 0.25])
+  (generate-term rbtrees t #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 2b254377f3..a867083dcc 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
@@ -289,8 +289,8 @@
   (or (not t)
       (implies (type-check t) (ins-preserves-rb-tree t))))
 
-(define (generate-enum-term)
-  (generate-term rbtrees t #:i-th (pick-an-index 0.25)))
+(define (generate-enum-term [p-value 0.25])
+  (generate-term rbtrees t #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt
index 97928eb84c..01e1aa6e8b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt
@@ -473,8 +473,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt
index 6c7f3281bb..a3cf6d0cd4 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt
@@ -470,8 +470,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt
index 5dbd749933..43e3e85599 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt
@@ -469,8 +469,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt
index 8b2ca24005..ba93411742 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt
@@ -468,8 +468,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt
index 19f3d7bc5c..f2fbd9fec6 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt
@@ -469,8 +469,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt
index 10815e24b6..2454c39e95 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt
@@ -469,8 +469,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt
index 8b373ca55f..941cdeec90 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt
@@ -469,8 +469,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-base.rkt
index fc40aaae95..73a3e26868 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-base.rkt
@@ -468,8 +468,8 @@
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
-(define (generate-enum-term)
-    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
+(define (generate-enum-term [p-value 0.03])
+    (fix (generate-term bytecode e #:i-th (pick-an-index p-value))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 1bf07508fb..975ebe01e2 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
@@ -300,8 +300,8 @@
                                    (and (equal? (type-check a1) M-type)
                                         (equal? (type-check a2) M-type)))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (x int) x) 1)))
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 7c5ee23c84..f784b0f1fd 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
@@ -303,8 +303,8 @@
                                    (and (equal? (type-check a1) M-type)
                                         (equal? (type-check a2) M-type)))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (x int) (λ (y int) y)) 1)))
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 ca46184a00..a77dccb2d2 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
@@ -302,8 +302,8 @@
                                    (and (equal? (type-check a1) M-type)
                                         (equal? (type-check a2) M-type)))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
   
 (define small-counter-example
   (term ((λ (x int) (+ 1)) 1)))
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 fc5ace3754..8bb5e09675 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
@@ -302,8 +302,8 @@
                                    (and (equal? (type-check a1) M-type)
                                         (equal? (type-check a2) M-type)))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (z int) (((λ (y1 int) (λ (y int) y)) z) 1)) 0)))
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 c5430ec671..afc3fbc8e2 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
@@ -302,8 +302,8 @@
                                    (and (equal? (type-check a1) M-type)
                                         (equal? (type-check a2) M-type)))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
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 dccc1a074e..4ff14d619c 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
@@ -289,8 +289,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (x int) x) 1)))
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 765e724f4a..65388d0f41 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
@@ -292,8 +292,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (x int) (λ (y int) y)) 1)))
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 29886a7882..cf5c0ac0c0 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
@@ -291,8 +291,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
   
 (define small-counter-example
   (term ((λ (x int) (+ 1)) 1)))
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 aa4562ff22..427dd23380 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
@@ -291,8 +291,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define small-counter-example
   (term ((λ (a (list int)) (λ (x int) x)) nil)))
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 a5941bd9b9..37eb9c589e 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
@@ -302,8 +302,8 @@
                                    (and (equal? (type-check a1) M-type)
                                         (equal? (type-check a2) M-type)))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
index 9186e9bdf0..17a2c34f2c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
@@ -258,8 +258,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
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 fbcf0972bf..b2ed06ffe6 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
@@ -258,8 +258,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt
index 59c89408c9..1e7c0d5477 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt
@@ -259,8 +259,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
index 9cdbc925f5..238c7a39ed 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
@@ -259,8 +259,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt
index 249d479082..e993a74f16 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt
@@ -258,8 +258,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt
index 3d18923d8d..b6a2f456c8 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt
@@ -258,8 +258,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
index 8c9439996c..149e8995c9 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
@@ -257,8 +257,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt
index a87e9fa20a..eb2c06c1aa 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt
@@ -258,8 +258,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt
index 285547eb6e..cc9e5e9e13 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt
@@ -258,8 +258,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt
index ccc37c6faf..9296fe7838 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt
@@ -259,8 +259,8 @@
                       (let ([red-type (type-check red-t)])
                         (equal? t-type red-type))))))))))
 
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+(define (generate-enum-term [p-value 0.035])
+  (generate-term stlc M #:i-th (pick-an-index p-value)))
 
 (define (ordered-enum-generator)
   (let ([index 0])