diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index 08393a1a2d..b6f562decd 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -495,11 +495,12 @@
                     #:var (list (λ _ 'x) (λ _ 'y))))
         (term (λ (x) (hole y)))))
 
-;; current-output : (-> (-> any) string)
-(define (current-output thunk)
+;; output : (-> (-> void) string)
+(define (output thunk)
   (let ([p (open-output-string)])
     (parameterize ([current-output-port p])
-      (thunk))
+      (unless (void? (thunk))
+        (error 'output "expected void result")))
     (begin0
       (get-output-string p)
       (close-output-port p))))
@@ -510,28 +511,38 @@
     (d 5)
     (e e 4)
     (n number))
-  (test (current-output (λ () (redex-check lang d #f))) 
+  (test (output (λ () (redex-check lang d #f))) 
         "counterexample found after 1 attempts:\n5\n")
-  (test (redex-check lang d #t) #t)
-  (test (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2) #t)
-  (test (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2) #t)
-  (test (current-output (λ () (redex-check lang (d e) #f)))
+  (test (output (λ () (redex-check lang d #t))) "")
+  (test (output (λ () (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2)))
+        "")
+  (test (output (λ () (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2)))
+        "")
+  (test (output (λ () (redex-check lang (d e) #f)))
         "counterexample found after 1 attempts:\n(5 4)\n")
-  (test (current-output (λ () (redex-check lang d (error 'pred-raised))))
-        "counterexample found after 1 attempts:\n5\n")
+  (let* ([p (open-output-string)]
+         [m (parameterize ([current-error-port p])
+              (with-handlers ([exn:fail? exn-message])
+                (redex-check lang d (error 'pred-raised))
+                'no-exn-raised))])
+    (test m "error: pred-raised")
+    (test (get-output-string p) #rx"checking 5 raises.*\n$")
+    (close-output-port p))
   (test (parameterize ([check-randomness (make-random 0 0)])
-          (redex-check lang n (eq? 42 (term n)) 
-                       #:attempts 1
-                       #:source (reduction-relation lang (--> 42 x))))
-        #t)
-  (test (current-output
+          (output
+           (λ ()
+             (redex-check lang n (eq? 42 (term n)) 
+                          #:attempts 1
+                          #:source (reduction-relation lang (--> 42 x))))))
+        "")
+  (test (output
          (λ ()
            (parameterize ([check-randomness (make-random 0 0)])
              (redex-check lang n (eq? 42 (term n)) 
                           #:attempts 1
                           #:source (reduction-relation lang (--> 0 x z))))))
         "counterexample found (z) after 1 attempts:\n0\n")
-  (test (current-output
+  (test (output
          (λ ()
            (parameterize ([check-randomness (make-random 1)])
              (redex-check lang d (eq? 42 (term n)) 
@@ -539,19 +550,23 @@
                           #:source (reduction-relation lang (--> 0 x z))))))
         "counterexample found after 1 attempts:\n5\n")
   (test (let ([r (reduction-relation lang (--> 0 x z))])
-          (redex-check lang n (number? (term n)) 
-                       #:attempts 10
-                       #:source r))
-        #t)
+          (output 
+           (λ ()
+             (redex-check lang n (number? (term n)) 
+                          #:attempts 10
+                          #:source r))))
+        "")
   (let ()
     (define-metafunction lang
       [(mf 0) 0]
       [(mf 42) 0])
     (test (parameterize ([check-randomness (make-random 0 1)])
-            (redex-check lang (n) (eq? 42 (term n)) 
-                         #:attempts 1
-                         #:source mf))
-          #t))
+            (output 
+             (λ ()
+               (redex-check lang (n) (eq? 42 (term n)) 
+                            #:attempts 1
+                            #:source mf))))
+          ""))
   (let ()
     (define-language L)
     (test (with-handlers ([exn:fail? exn-message])
@@ -601,21 +616,21 @@
     [(i any ...) (any ...)])
   
   ;; Dom(f) < Ctc(f)
-  (test (current-output 
+  (test (output 
          (λ () 
            (parameterize ([generation-decisions 
                            (decisions #:num (list (λ _ 2) (λ _ 5)))])
              (check-metafunction-contract f))))
         "counterexample found after 1 attempts:\n(5)\n")
   ;; Rng(f) > Codom(f)
-  (test (current-output
+  (test (output
          (λ () 
            (parameterize ([generation-decisions
                            (decisions #:num (list (λ _ 3)))])
              (check-metafunction-contract f))))
         "counterexample found after 1 attempts:\n(3)\n")
   ;; LHS matches multiple ways
-  (test (current-output
+  (test (output
          (λ () 
            (parameterize ([generation-decisions
                            (decisions #:num (list (λ _ 1) (λ _ 1))
@@ -623,9 +638,9 @@
              (check-metafunction-contract g))))
         "counterexample found after 1 attempts:\n(1 1)\n")
   ;; OK -- generated from Dom(h)
-  (test (check-metafunction-contract h) #t)
+  (test (output (λ () (check-metafunction-contract h))) "")
   ;; OK -- generated from pattern (any ...)
-  (test (check-metafunction-contract i #:attempts 5) #t))
+  (test (output (λ () (check-metafunction-contract i #:attempts 5))) ""))
 
 ;; check-reduction-relation
 (let ()
@@ -653,11 +668,11 @@
           (reverse '((+ (+)) 0))))
   
   (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
-    (test (check-reduction-relation S (λ (x) #t) #:attempts 1) #t)
-    (test (current-output 
+    (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1))) "")
+    (test (output 
            (λ () (check-reduction-relation S (λ (x) #f))))
           "counterexample found after 1 attempts with name:\n1\n")
-    (test (current-output 
+    (test (output 
            (λ () (check-reduction-relation S (curry eq? 1))))
           "counterexample found after 1 attempts with unnamed:\n3\n"))
   
@@ -671,11 +686,13 @@
             with
             [(--> (9 a) b)
              (==> a b)])])
-    (test (check-reduction-relation 
-           T (curry equal? '(9 4)) 
-           #:attempts 1
-           #:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))
-          #t)))
+    (test (output
+           (λ ()
+             (check-reduction-relation 
+              T (curry equal? '(9 4)) 
+              #:attempts 1
+              #:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))))
+          "")))
 
 ; check-metafunction
 (let ()
@@ -688,7 +705,8 @@
             (check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)
             generated) 
           (reverse '((1) (2)))))
-  (test (current-output (λ () (check-metafunction m (curry eq? 1))))
+  (test (output (λ () (check-metafunction m (λ (_) #t)))) "")
+  (test (output (λ () (check-metafunction m (curry eq? 1))))
         #rx"counterexample found after 1 attempts with clause #1")
   (test (with-handlers ([exn:fail:contract? exn-message])
           (check-metafunction m #t #:attempts 'NaN))
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 3b700c2424..c293b00359 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -680,41 +680,41 @@ To do a better job of not generating programs with free variables,
          (quasisyntax/loc stx
            (let ([att attempts])
              (assert-nat 'redex-check att)
-             (or (check-property 
-                  (cons (list #,(term-generator #'lang #'pat #'random-decisions 'redex-check) #f)
-                        (let ([lang-gen (generate lang (random-decisions lang))])
-                          #,(if (not source-stx)
-                                #'null
-                                #`(let-values
-                                      ([(pats srcs src-lang)
-                                        #,(cond [(and (identifier? source-stx) (metafunc source-stx))
-                                                 => 
-                                                 (λ (m) #`(values (metafunc-proc-lhs-pats #,m)
-                                                                  (metafunc-srcs #,m)
-                                                                  (metafunc-proc-lang #,m)))]
-                                                [else
-                                                 #`(let ([r #,source-stx])
-                                                     (unless (reduction-relation? r)
-                                                       (raise-type-error 'redex-check "reduction-relation" r))
-                                                     (values
-                                                      (map rewrite-proc-lhs (reduction-relation-make-procs r))
-                                                      (reduction-relation-srcs r)
-                                                      (reduction-relation-lang r)))])])
-                                    (unless (eq? src-lang lang)
-                                      (error 'redex-check "language for secondary source must match primary pattern's language"))
-                                    (zip (map lang-gen pats) srcs)))))
-                  #,(and source-stx #'(test-match lang pat))
-                  (λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))
-                  (λ (_ bindings)
-                    (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
-                              property))
-                  att
-                  (λ (term attempt source port)
-                    (fprintf port "counterexample found~aafter ~a attempts:\n"
-                             (if source (format " (~a) " source) " ") attempt)
-                    (pretty-print term port))
-                  (check-randomness))
-                 (void))))))]))
+             (check-property 
+              (cons (list #,(term-generator #'lang #'pat #'random-decisions 'redex-check) #f)
+                    (let ([lang-gen (generate lang (random-decisions lang))])
+                      #,(if (not source-stx)
+                            #'null
+                            #`(let-values
+                                  ([(pats srcs src-lang)
+                                    #,(cond [(and (identifier? source-stx) (metafunc source-stx))
+                                             => 
+                                             (λ (m) #`(values (metafunc-proc-lhs-pats #,m)
+                                                              (metafunc-srcs #,m)
+                                                              (metafunc-proc-lang #,m)))]
+                                            [else
+                                             #`(let ([r #,source-stx])
+                                                 (unless (reduction-relation? r)
+                                                   (raise-type-error 'redex-check "reduction-relation" r))
+                                                 (values
+                                                  (map rewrite-proc-lhs (reduction-relation-make-procs r))
+                                                  (reduction-relation-srcs r)
+                                                  (reduction-relation-lang r)))])])
+                                (unless (eq? src-lang lang)
+                                  (error 'redex-check "language for secondary source must match primary pattern's language"))
+                                (zip (map lang-gen pats) srcs)))))
+              #,(and source-stx #'(test-match lang pat))
+              (λ (generated) (error 'redex-check "~s does not match ~s" generated 'pat))
+              (λ (_ bindings)
+                (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
+                          property))
+              att
+              (λ (term attempt source port)
+                (fprintf port "counterexample found~aafter ~a attempts:\n"
+                         (if source (format " (~a) " source) " ") attempt)
+                (pretty-print term port))
+              (check-randomness))
+             (void)))))]))
 
 (define (check-property gens-srcs match match-fail property attempts display [random random])
   (let loop ([remaining attempts])
@@ -729,7 +729,11 @@ To do a better job of not generating programs with free variables,
                         [(term bindings) 
                          (generator (attempt->size attempt) attempt)])
             (if (andmap (λ (bindings) 
-                          (with-handlers ([exn:fail? (λ (_) #f)])
+                          (with-handlers ([exn:fail? (λ (exn) 
+                                                       (fprintf (current-error-port)
+                                                                "checking ~s raises ~s\n"
+                                                                term exn)
+                                                       (raise exn))])
                             (property term bindings)))
                         (cond [(and match (match term)) 
                                => (curry map (compose make-bindings match-bindings))]
@@ -758,11 +762,14 @@ To do a better job of not generating programs with free variables,
            (list (list ((generate lang (decisions lang)) (if dom dom '(any (... ...)))) #f))
            #f
            #f
-           (λ (t _) (begin (term (name ,@t)) #t))
+           (λ (t _) 
+             (with-handlers ([exn:fail:redex? (λ (_) #f)])
+               (begin (term (name ,@t)) #t)))
            att
            (λ (term attempt _ port)
              (fprintf port "counterexample found after ~a attempts:\n" attempt)
-             (pretty-print term port))))))]))
+             (pretty-print term port)))
+          (void))))]))
 
 (define (check-property-many lang pats srcs prop decisions attempts)
   (let ([lang-gen (generate lang (decisions lang))])
@@ -777,7 +784,8 @@ To do a better job of not generating programs with free variables,
        (λ (term attempt source port)
          (fprintf port "counterexample found after ~a attempts with ~a:\n" 
                   attempt source)
-         (pretty-print term port))))))
+         (pretty-print term port))))
+    (void)))
 
 (define (metafunc-srcs m)
   (build-list (length (metafunc-proc-lhs-pats m))
@@ -792,14 +800,13 @@ To do a better job of not generating programs with free variables,
        (syntax/loc stx
          (let ([att attempts])
            (assert-nat 'check-metafunction att)
-           (or (check-property-many 
-                (metafunc-proc-lang m)
-                (metafunc-proc-lhs-pats m)
-                (metafunc-srcs m)
-                property
-                (generation-decisions)
-                att)
-               (void)))))]))
+           (check-property-many 
+            (metafunc-proc-lang m)
+            (metafunc-proc-lhs-pats m)
+            (metafunc-srcs m)
+            property
+            (generation-decisions)
+            att))))]))
 
 (define (reduction-relation-srcs r)
   (map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
@@ -809,14 +816,13 @@ To do a better job of not generating programs with free variables,
          relation property 
          #:decisions [decisions random-decisions]
          #:attempts [attempts default-check-attempts])
-  (or (check-property-many
-       (reduction-relation-lang relation)
-       (map rewrite-proc-lhs (reduction-relation-make-procs relation))
-       (reduction-relation-srcs relation)
-       property
-       decisions
-       attempts)
-      (void)))
+  (check-property-many
+   (reduction-relation-lang relation)
+   (map rewrite-proc-lhs (reduction-relation-make-procs relation))
+   (reduction-relation-srcs relation)
+   property
+   decisions
+   attempts))
 
 (define-signature decisions^
   (next-variable-decision