diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff
index 67f3013f7e..aa65fdf53b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff
@@ -16,11 +16,13 @@
 >   ;; bug 14
 >   [(closure-intact? (box-nc ṽ_1 ...) (imm ṽ_2 ...))
 >    (closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
-475a481,487
-> (test-equal
->  (bytecode-ok?
->    '(let-one 'x 
->              (let-rec ((lam () (0) (application (loc-noclr 0)))) 
->                       'x)))
->  #t)
+475a481,489
+> 
+> (define small-counter-example
+>   '(let-one 'x
+>             (application (proc-const (val val) (loc 0))
+>                          (loc-noclr 2)
+>                          (install-value 2 'y 'z))))
+> 
+> (test-equal (check small-counter-example) #f)
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff
index d5d8807c60..c012b7089b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff
@@ -14,11 +14,11 @@
 ---
 >        `(case-lam ,@(map (curry recur depth #t) ls))]
 475a478,485
-> (test-equal
->  (bytecode-ok?
->    '(let-one 42 
+> 
+> (define small-counter-example
+>   '(let-one 42 
 >              (boxenv 0 
 >                      (application (case-lam (lam (ref) () (loc-box 0))) 
 >                                   (loc-box 1)))))
->  #t)
 > 
+> (test-equal (check small-counter-example) #f)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff
new file mode 100644
index 0000000000..e75e3841be
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff
@@ -0,0 +1,18 @@
+338c338,339
+<    (side-condition (< (term n_0) (term n_h)))]
+---
+>    ;; bug 2
+>    #;(side-condition (< (term n_0) (term n_h)))]
+475a477,487
+> 
+> (define small-counter-example
+>   '(proc-const (val)
+>                 (branch (loc 0)
+>                         (let-one 'x
+>                                  (branch (loc 1)
+>                                          (loc-clr 0)
+>                                          void))
+>                         void)))
+> 
+> (test-equal (check small-counter-example) #f)
+\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff
index 0a64b78f38..53f6ec2229 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff
@@ -14,12 +14,13 @@
 <    (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η))
 ---
 >    (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n uninit s) n_l* #f γ η))
-475a476,483
-> (test-equal
->  (bytecode-ok?
+475a476,484
+> 
+> (define small-counter-example
 >   '(application
 >     (proc-const (val val) (branch (loc-noclr 0) 'a 'b))
 >     'x
 >     (install-value 0 'y (boxenv 0 'z))))
->  #t)
+> 
+> (test-equal (check small-counter-example) #f)
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff
index c53abfe03a..84f429049a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff
@@ -7,10 +7,12 @@
 ---
 >    ;; bug 4
 >    #;(side-condition (< (term n_p) (term n_l)))]
-475a477,482
-> (test-equal
->  (bytecode-ok?
+475a477,484
+> 
+> (define small-counter-example
 >   '(let-one 'x
 >             (branch #f (boxenv 0 'y) (loc-box 0))))
->  #t)
+> 
+> (test-equal (check small-counter-example) #f)
+> 
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff
index c0cb612863..80597b9ae4 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff
@@ -7,12 +7,14 @@
 ---
 >    ;;bug 5
 >    ;;(side-condition (<= (term n) (term n_l)))
-475a477,484
-> (test-equal
->  (bytecode-ok? 
+475a477,486
+> 
+> (define small-counter-example
 >   '(let-void 1 
 >              (branch #f 
 >                      (let-rec ((lam () (0) 'x)) 'y) 
 >                      (loc-noclr 0))))
->  #t)
+> 
+> (test-equal (check small-counter-example) #f)
+> 
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff
index 01b96757c7..79ba6ed2d8 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff
@@ -3,9 +3,12 @@
 ---
 >    ;; bug 6
 >    #;(side-condition (term (AND (lam-verified? l s ?) ...)))]
-474a476,480
-> (test-equal
->  (bytecode-ok?
->   '(let-one 'x (case-lam (lam (val) () (loc-noclr 34)))))
->  #t)
+475a477,483
 > 
+> (define small-counter-example
+>   '(application
+>                (case-lam (lam (val) () (loc-noclr 34)))
+>                'x))
+> 
+> (test-equal (check small-counter-example) #f)
+\ No newline at end of file
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 3a8a17b115..3f48bf8ee6 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
@@ -435,49 +435,49 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(let-one 'x
@@ -487,3 +487,9 @@
 
 (test-equal (check small-counter-example) #f)
 
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 112dcee6e0..ede5f120ce 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
@@ -432,49 +432,49 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(let-one 42 
@@ -483,3 +483,9 @@
                                   (loc-box 1)))))
 
 (test-equal (check small-counter-example) #f)
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 e64d8b7119..64128124aa 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
@@ -431,49 +431,49 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(proc-const (val)
@@ -484,4 +484,10 @@
                                          void))
                         void)))
 
-(test-equal (check small-counter-example) #f)
\ No newline at end of file
+(test-equal (check small-counter-example) #f)
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 abfc076537..99a5c76c76 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
@@ -430,49 +430,49 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(application
@@ -482,3 +482,9 @@
 
 (test-equal (check small-counter-example) #f)
 
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 8ef39f1f3c..4425a866ab 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
@@ -431,49 +431,49 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(let-one 'x
@@ -482,3 +482,9 @@
 (test-equal (check small-counter-example) #f)
 
 
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 05987ac6ff..33b4e21eca 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
@@ -431,49 +431,49 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(let-void 1 
@@ -484,3 +484,9 @@
 (test-equal (check small-counter-example) #f)
 
 
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 a68299ccd9..8975e56f87 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
@@ -431,53 +431,59 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term bytecode e #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed '())
 
 (define small-counter-example
   '(application
                (case-lam (lam (val) () (loc-noclr 34)))
                'x))
 
-(test-equal (check small-counter-example) #f)
\ No newline at end of file
+(test-equal (check small-counter-example) #f)
+    (λ ()
+      (begin0
+        (fix (generate-term bytecode e #:i-th index))
+        (set! index (add1 index))))))
+
+(define fixed '())
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 aa90068c70..fc40aaae95 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
@@ -430,46 +430,52 @@
       [`(quote ,_) expr]
       [(? boolean?) expr])))
 
-(define (check e0)
-  (define e (fix e0))
-  (or (not e)
-      (not (bytecode-ok? e))
-       (match 
-           (with-handlers
-               ([exn:fail? (λ (exc)
-                             (unless
-                                 (regexp-match?
-                                  #"counterexample|domain|clauses"
-                                  (exn-message exc))
-                               (printf "exception on ~s\n~s\n" e
-                                       (exn-message exc)))
-                             #f)])
-             (run e '() 100))
-         [(cutoff) #t]
-         [(answer _) #t]
-         [_ #f])))
+(define (check e)
+  (let/ec fail
+    (or (not e)
+        (implies (with-handlers ([exn:fail? (λ (exc)
+                                              (maybe-log-exn exc e)
+                                              (fail #f))])
+                   (bytecode-ok? e))
+                 (match 
+                     (with-handlers
+                         ([exn:fail? (λ (exc)
+                                       (maybe-log-exn exc e)
+                                       #f)])
+                       (run e '() 100))
+                   [(cutoff) #t]
+                   [(answer _) #t]
+                   [_ #f])))))
+
+(define (maybe-log-exn exc e)
+  (unless
+      (regexp-match?
+       #"counterexample|domain|clauses"
+       (exn-message exc))
+    (printf "exception on ~s\n~s\n" e
+            (exn-message exc))))
 
 
 (define (generate-M-term)
-  (generate-term bytecode e 5))
+  (fix (generate-term bytecode e 5)))
 
 (define (generate-typed-term)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (type-check e)
-  (bytecode-ok? (fix e)))
+  (bytecode-ok? e))
 
 (define (typed-generator)
   (error "not currently implemented for rvm in the benchmark"))
 
 (define (generate-enum-term)
-    (generate-term bytecode e #:i-th (pick-an-index 0.03)))
+    (fix (generate-term bytecode e #:i-th (pick-an-index 0.03))))
 
 (define (ordered-enum-generator)
   (let ([index 0])
     (λ ()
       (begin0
-        (generate-term bytecode e #:i-th index)
+        (fix (generate-term bytecode e #:i-th index))
         (set! index (add1 index))))))
 
 (define fixed '())