diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
index dc99882edf..e47334df83 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
@@ -2,11 +2,9 @@
 < (define the-error "no error")
 ---
 > (define the-error "app rule the range of the function is matched to the argument")
-32a33
->      ((cons v) v)
-54c55
+55c55
 <    (typeof Γ M_2 σ)
 ---
 >    (typeof Γ M_2 σ_2)
-237d237
+238d237
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
index 8c390c8a25..ed42dd860c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
@@ -2,5 +2,3 @@
 < (define the-error "no error")
 ---
 > (define the-error "the ((cons number) v) value has been omitted")
-32a33
->      ((cons v) v)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff
index 215a3155d3..0ff1128edf 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff
@@ -2,9 +2,7 @@
 < (define the-error "no error")
 ---
 > (define the-error "the order of the types in the function position of application has been swapped")
-32a33
->      ((cons v) v)
-53c54
+54c54
 <   [(typeof Γ M (σ → σ_2))
 ---
 >   [(typeof Γ M (σ_2 → σ))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
index 036138e02c..964a460abb 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
@@ -2,9 +2,7 @@
 < (define the-error "no error")
 ---
 > (define the-error "the type of cons is incorrect")
-32a33
->      ((cons v) v)
-63c64
+64c64
 <    (int → ((list int) → (list int)))]
 ---
 >    (int → ((list int) → int))]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff
index 67db030638..402c54fc40 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff
@@ -2,11 +2,9 @@
 < (define the-error "no error")
 ---
 > (define the-error "the tail reduction returns the wrong value")
-32a33
->      ((cons v) v)
-92c93
+93c93
 <         (in-hole E v_2)
 ---
 >         (in-hole E v_1)
-237d237
+238d237
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff
index 973f186b01..ff0356704f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff
@@ -2,11 +2,9 @@
 < (define the-error "no error")
 ---
 > (define the-error "hd reduction acts on partially applied cons")
-32a33
->      ((cons v) v)
-88c89
+89c89
 <    (--> (in-hole E (hd ((cons v_1) v_2)))
 ---
 >    (--> (in-hole E (hd (cons v_1)))
-237d237
+238d237
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
index 5560f3fc75..825e83e90d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
@@ -2,12 +2,10 @@
 < (define the-error "no error")
 ---
 > (define the-error "evaluation isn't allowed on the rhs of applications")
-32a33
->      ((cons v) v)
-35,36c36
+36,37c36
 <      (E M)
 <      (v E)))
 ---
 >      (E M)))
-237d236
+238d236
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff
index 51bba017ea..44c94ca2f6 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff
@@ -2,11 +2,9 @@
 < (define the-error "no error")
 ---
 > (define the-error "lookup always returns int")
-32a33
->      ((cons v) v)
-76c77
+77c77
 <    σ]
 ---
 >    int]
-237d237
+238d237
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff
index 6b331737f4..673f5bb06b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff
@@ -2,11 +2,9 @@
 < (define the-error "no error")
 ---
 > (define the-error "variables aren't required to match in lookup")
-32a33
->      ((cons v) v)
-75c76
+76c76
 <   [(lookup (x σ Γ) x)
 ---
 >   [(lookup (x σ Γ) x_2)
-237d237
+238d237
 < 
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 2f2113a4e4..0b53b88384 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 bb2d576d51..25d1fa3a4f 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 a0606ab9c6..8e47c81c11 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 22e33222d3..9446d9ad2b 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 0364a3f661..11b2f09e18 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 2eb0ce335f..cd1181cf6a 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 1f6f3e176f..a959244c51 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)))
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 3b2fc72df2..eaa76e8c1d 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
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 c8b605ec15..9f7839e99f 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
@@ -31,7 +31,6 @@
      c
      (cons v)
      ((cons v) v)
-     ((cons v) v)
      (+ v))
   (E hole
      (E M)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
index 5c65a2eb36..10a16ec42f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
@@ -181,7 +181,6 @@
   (define typed-generator (dynamic-require fpath 'typed-generator))
   (define gen-enum (dynamic-require fpath 'generate-enum-term))
   (define ordered-generator (dynamic-require fpath 'ordered-enum-generator))
-  (define fixed (dynamic-require fpath 'fixed))
   (define err (dynamic-require fpath 'the-error))
   (printf "\n-------------------------------------------------------------------\n")
   (printf "~a has the error: ~a\n\n" fpath err)
@@ -194,12 +193,18 @@
            t)))
   (cond
     [(equal? gen-type 'fixed)
-     (define some-failed?
-       (for/or ([t (in-list fixed)])
-         (define ok? (check (and (tc t) t)))
-         (not ok?)))
-     (unless some-failed?
-       (error 'fixed "Expected some term to fail, but didn't find one in ~a" fixed))]
+     (define small-counter-example
+       (dynamic-require 
+        fpath 'small-counter-example 
+        (λ ()
+          (error 'fixed "contains no small counter example"))))
+     (unless (tc small-counter-example)
+       (error 'fixed "The counter example doesn't type-check: ~e"
+              small-counter-example))
+     (define ok? (check small-counter-example))
+     (when ok?
+       (error 'fixed "Expected ~e to fail on check, but it didn't"
+              small-counter-example))]
     [(equal? gen-type 'grammar)
      (run/spawn-generations fpath verbose? no-errs? (λ () (gen-and-type gen-term))
                       check seconds gen-type)]