diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
index 61968e952e..575ee48a6f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
@@ -8,7 +8,33 @@
 <   [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
 ---
 >   [(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
-552a555,557
+541,552c543,558
+<       (let ([t-type (type-check M)])
+<         (implies
+<          t-type
+<          (let loop ([Σ+M `(· ,M)] [n 100])
+<            (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+<            (and (consistent-with? t-type new-type)
+<                 (or (v? (list-ref Σ+M 1))
+<                     (let ([red-res (apply-reduction-relation red Σ+M)])
+<                       (and (= (length red-res) 1)
+<                            (let ([red-t (car red-res)])
+<                              (or (equal? red-t "error")
+<                                  (zero? n) (loop red-t (- n 1)))))))))))))
+---
+>       (with-handlers ([exn:fail? (λ (x) #f)])
+>         (let ([t-type (type-check M)])
+>           (implies
+>            t-type
+>            (let loop ([Σ+M `(· ,M)] [n 100])
+>              (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+>              (and (consistent-with? t-type new-type)
+>                   (or (v? (list-ref Σ+M 1))
+>                       (let ([red-res (apply-reduction-relation red Σ+M)])
+>                         (and (= (length red-res) 1)
+>                              (let ([red-t (car red-res)])
+>                                (or (equal? red-t "error")
+>                                    (zero? n) (loop red-t (- n 1))))))))))))))
 > 
 > (define small-counter-example (term ((λ x (x x)) hd)))
 > (test-equal (check small-counter-example) #f)
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 df0045c7e2..fbc6b945d1 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
@@ -540,18 +540,19 @@ reachable from the given term.
 
 (define (check M)
   (or (not M)
-      (let ([t-type (type-check M)])
-        (implies
-         t-type
-         (let loop ([Σ+M `(· ,M)] [n 100])
-           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-           (and (consistent-with? t-type new-type)
-                (or (v? (list-ref Σ+M 1))
-                    (let ([red-res (apply-reduction-relation red Σ+M)])
-                      (and (= (length red-res) 1)
-                           (let ([red-t (car red-res)])
-                             (or (equal? red-t "error")
-                                 (zero? n) (loop red-t (- n 1)))))))))))))
+      (with-handlers ([exn:fail? (λ (x) #f)])
+        (let ([t-type (type-check M)])
+          (implies
+           t-type
+           (let loop ([Σ+M `(· ,M)] [n 100])
+             (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+             (and (consistent-with? t-type new-type)
+                  (or (v? (list-ref Σ+M 1))
+                      (let ([red-res (apply-reduction-relation red Σ+M)])
+                        (and (= (length red-res) 1)
+                             (let ([red-t (car red-res)])
+                               (or (equal? red-t "error")
+                                   (zero? n) (loop red-t (- n 1))))))))))))))
 
 (define small-counter-example (term ((λ x (x x)) hd)))
 (test-equal (check small-counter-example) #f)