diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index c2502d28ab..04df780210 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -695,11 +695,12 @@
      (let-values ([(names names/ellipses) 
                    (extract-names (language-id-nts #'lang 'redex-check)
                                   'redex-check #t #'pat)]
-                  [(attempts-stx source-stx retries-stx)
+                  [(attempts-stx source-stx retries-stx print?-stx)
                    (apply values
                           (parse-kw-args `((#:attempts . ,#'default-check-attempts)
                                            (#:source . #f)
-                                           (#:retries . ,#'default-retries))
+                                           (#:retries . ,#'default-retries)
+                                           (#:print? . #t))
                                          (syntax kw-args)
                                          stx))])
        (with-syntax ([(name ...) names]
@@ -711,7 +712,8 @@
                                               property)))])
            (quasisyntax/loc stx
              (let ([att (assert-nat 'redex-check #,attempts-stx)]
-                   [ret (assert-nat 'redex-check #,retries-stx)])
+                   [ret (assert-nat 'redex-check #,retries-stx)]
+                   [print? #,print?-stx])
                (unsyntax
                 (if source-stx
                     #`(let-values ([(metafunc/red-rel num-cases) 
@@ -728,21 +730,27 @@
                          (max 1 (floor (/ att num-cases)))
                          ret
                          'redex-check
-                         show
+                         (and print? show)
                          (test-match lang pat)
                          (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
                     #`(check-prop
                        #,(term-generator #'lang #'pat #'random-decisions@ 'redex-check)
-                       property att ret show)))
-               (void))))))]))
+                       property att ret (and print? show)))))))))]))
 
 (define (format-attempts a)
   (format "~a attempt~a" a (if (= 1 a) "" "s")))
 
-(define (check-prop generator property attempts retries show)
-  (when (check generator property attempts retries show)
-    (show (format "no counterexamples in ~a\n"
-                  (format-attempts attempts)))))
+(define (check-prop generator property attempts retries show) 
+  (let ([c (check generator property attempts retries show)])
+    (if (counterexample? c)
+        (unless show c) ; check printed it
+        (if show
+            (show (format "no counterexamples in ~a\n"
+                          (format-attempts attempts)))
+            #t))))
+
+(define-struct (exn:fail:redex:test exn:fail:redex) (source term))
+(define-struct counterexample (term))
 
 (define (check generator property attempts retries show
                #:source [source #f]
@@ -757,9 +765,16 @@
                           (with-handlers 
                               ([exn:fail?
                                 (λ (exn) 
-                                  (show 
-                                   (format "checking ~s raises an exception\n" term))
-                                  (raise exn))])
+                                  (when show 
+                                    (show (format "checking ~s raises an exception\n" term)))
+                                  (raise 
+                                   (if show
+                                       exn
+                                       (make-exn:fail:redex:test
+                                        (format "checking ~s raises an exception:\n~a" term (exn-message exn))
+                                        (current-continuation-marks)
+                                        exn
+                                        term))))])
                             (property term bindings)))
                         (cond [(and match match-fail (match term)) 
                                => (curry map (compose make-bindings match-bindings))]
@@ -767,12 +782,13 @@
                               [else (list bindings)]))
                 (loop (sub1 remaining))
                 (begin
-                  (show
-                   (format "counterexample found after ~a~a:\n"
-                           (format-attempts attempt)
-                           (if source (format " with ~a" source) "")))
-                  (pretty-print term (current-output-port))
-                  #f)))))))
+                  (when show
+                    (show
+                     (format "counterexample found after ~a~a:\n"
+                             (format-attempts attempt)
+                             (if source (format " with ~a" source) "")))
+                    (pretty-print term (current-output-port)))
+                  (make-counterexample term))))))))
 
 (define-syntax (check-metafunction-contract stx)
   (syntax-case stx ()
@@ -801,8 +817,8 @@
            show))))]))
 
 (define (check-lhs-pats lang mf/rr prop decisions@ attempts retries what show
-                         [match #f]
-                         [match-fail #f])
+                        [match #f]
+                        [match-fail #f])
   (let ([lang-gen (generate lang decisions@ what)])
     (let-values ([(pats srcs)
                   (cond [(metafunc-proc? mf/rr)
@@ -811,46 +827,53 @@
                         [(reduction-relation? mf/rr)
                          (values (map (λ (rwp) ((rewrite-proc-lhs rwp) lang)) (reduction-relation-make-procs mf/rr))
                                  (reduction-relation-srcs mf/rr))])])
-      (when (for/and ([pat pats] [src srcs])
-              (with-handlers ([exn:fail:redex:generation-failure?
-                               ; Produce an error message that blames the LHS as a whole.
-                               (λ (_)
-                                 (raise-gen-fail what (format "LHS of ~a" src) retries))])
-                (check
-                 (lang-gen pat)
-                 prop
-                 attempts
-                 retries
-                 show
-                 #:source src
-                 #:match match
-                 #:match-fail match-fail)))
-        (show
-         (format "no counterexamples in ~a (with each clause)\n"
-                 (format-attempts attempts)))))))
+      (let loop ([pats pats] [srcs srcs])
+        (if (and (null? pats) (null? srcs))
+            (if show
+                (show
+                 (format "no counterexamples in ~a (with each clause)\n"
+                         (format-attempts attempts)))
+                #t)
+            (let ([c (with-handlers ([exn:fail:redex:generation-failure?
+                                      ; Produce an error message that blames the LHS as a whole.
+                                      (λ (_)
+                                        (raise-gen-fail what (format "LHS of ~a" (car srcs)) retries))])
+                       (check
+                        (lang-gen (car pats))
+                        prop
+                        attempts
+                        retries
+                        show
+                        #:source (car srcs)
+                        #:match match
+                        #:match-fail match-fail))])
+              (if (counterexample? c)
+                  (unless show c)
+                  (loop (cdr pats) (cdr srcs)))))))))
 
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()
     [(_ name property . kw-args)
      (with-syntax ([m (metafunc/err #'name stx)]
-                   [(attempts retries)
+                   [(attempts retries print?) 
                     (parse-kw-args `((#:attempts . , #'default-check-attempts)
-                                     (#:retries . ,#'default-retries))
+                                     (#:retries . ,#'default-retries)
+                                     (#:print? . #t))
                                    (syntax kw-args)
-                                   stx)]
-                   [show (show-message stx)])
-       (syntax/loc stx
-         (let ([att (assert-nat 'check-metafunction attempts)]
-               [ret (assert-nat 'check-metafunction retries)])
-           (check-lhs-pats 
-            (metafunc-proc-lang m)
-            m
-            (λ (term _) (property term))
-            (generation-decisions)
-            att
-            ret
-            'check-metafunction
-            show))))]))
+                                   stx)])
+       (with-syntax ([show (show-message stx)])
+         (syntax/loc stx
+           (let ([att (assert-nat 'check-metafunction attempts)]
+                 [ret (assert-nat 'check-metafunction retries)])
+             (check-lhs-pats 
+              (metafunc-proc-lang m)
+              m
+              (λ (term _) (property term))
+              (generation-decisions)
+              att
+              ret
+              'check-metafunction
+              (and print? show))))))]))
 
 (define (reduction-relation-srcs r)
   (map (λ (proc) (or (rewrite-proc-name proc)
@@ -864,10 +887,11 @@
 (define-syntax (check-reduction-relation stx)
   (syntax-case stx ()
     [(_ relation property . kw-args)
-     (with-syntax ([(attempts retries decisions@)
+     (with-syntax ([(attempts retries decisions@ print?)
                     (parse-kw-args `((#:attempts . , #'default-check-attempts)
                                      (#:retries . ,#'default-retries)
-                                     (#:decisions . ,#'random-decisions@))
+                                     (#:decisions . ,#'random-decisions@)
+                                     (#:print? . #t))
                                    (syntax kw-args)
                                    stx)]
                    [show (show-message stx)])
@@ -883,7 +907,7 @@
             attempts
             retries
             'check-reduction-relation
-            show))))]))
+            (and print? show)))))]))
 
 (define-signature decisions^
   (next-variable-decision
@@ -921,7 +945,9 @@
          (struct-out mismatch)
          (struct-out class)
          (struct-out binder)
-         (struct-out base-cases))
+         (struct-out base-cases)
+         (struct-out counterexample)
+         (struct-out exn:fail:redex:test))
 
 (provide pick-from-list pick-sequence-length pick-nts
          pick-char pick-var pick-string pick-any
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 9eb594b227..9d062200fb 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -1166,11 +1166,13 @@ repeating as necessary. The optional keyword argument @scheme[retries-expr]
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:source metafunction)
                        (code:line #:source relation-expr)
-                       (code:line #:retries retries-expr)])
+                       (code:line #:retries retries-expr)
+                       (code:line #:print? print?-expr)])
               #:contracts ([property-expr any/c]
                            [attempts-expr natural-number/c]
                            [relation-expr reduction-relation?]
-                           [retries-expr natural-number/c])]{
+                           [retries-expr natural-number/c]
+                           [print?-expr any/c])]{
 Searches for a counterexample to @scheme[property-expr], interpreted
 as a predicate universally quantified over the pattern variables
 bound by @scheme[pattern]. @scheme[redex-check] constructs and tests 
@@ -1180,8 +1182,18 @@ using the @scheme[match-bindings] produced by @scheme[match]ing
 @math{t} against @scheme[pattern].
 
 @scheme[redex-check] generates at most @scheme[attempts-expr] (default @scheme[1000])
-random terms in its search. The size and complexity of terms it generates
-gradually increases with each failed attempt.
+random terms in its search. The size and complexity of these terms increase with 
+each failed attempt. 
+
+When @scheme[print?-expr] produces any non-@scheme[#f] value (the default), 
+@scheme[redex-check] prints the test outcome on @scheme[current-output-port].
+When @scheme[print?-expr] produces @scheme[#f], @scheme[redex-check] prints
+nothing, instead 
+@itemlist[
+  @item{returning a @scheme[counterexample] structure when the test reveals a counterexample,}
+  @item{returning @scheme[#t] when all tests pass, or}
+  @item{raising a @scheme[exn:fail:redex:test] when checking the property raises an exception.}
+]
 
 When passed a metafunction or reduction relation via the optional @scheme[#:source]
 argument, @scheme[redex-check] distributes its attempts across the left-hand sides
@@ -1228,6 +1240,16 @@ term that does not match @scheme[pattern].}
           #:attempts 3
           #:source R))]
 
+@defstruct[counterexample ([term any/c])]{
+Produced by @scheme[redex-check], @scheme[check-reduction-relation], and 
+@scheme[check-metafunction] when testing falsifies a property.}
+
+@defstruct[(exn:fail:redex:test exn:fail:redex) ([source exn:fail?] [term any/c])]{
+Raised by @scheme[redex-check], @scheme[check-reduction-relation], and 
+@scheme[check-metafunction] when testing a property raises an exception.
+The @scheme[exn:fail:redex:test-source] component contains the exception raised by the property,
+and the @scheme[exn:fail:redex:test-term] component contains the term that induced the exception.}
+
 @defform/subs[(check-reduction-relation relation property kw-args ...)
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:retries retries-expr)])
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index fc8a9ff9d0..ad0c601b0e 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -50,7 +50,9 @@
          check-metafunction
          check-metafunction-contract
          check-reduction-relation
-         exn:fail:redex:generation-failure?)
+         exn:fail:redex:generation-failure?
+         (struct-out exn:fail:redex:test)
+         (struct-out counterexample))
 
 (provide/contract
  [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
diff --git a/collects/redex/tests/rg-test.ss b/collects/redex/tests/rg-test.ss
index abd12b2ae5..12c8571c1b 100644
--- a/collects/redex/tests/rg-test.ss
+++ b/collects/redex/tests/rg-test.ss
@@ -540,6 +540,16 @@
     (d 5)
     (e e 4)
     (n number))
+  
+  (test (redex-check lang d #t #:attempts 1 #:print? (not #t)) #t)
+  (test (counterexample-term (redex-check lang d #f #:print? #f)) 5)
+  (let ([exn (with-handlers ([exn:fail:redex:test? values])
+               (redex-check lang d (error 'boom ":(") #:print? #f)
+               'not-an-exn)])
+    (test (exn-message exn) "checking 5 raises an exception:\nboom: :(")
+    (test (exn-message (exn:fail:redex:test-source exn)) "boom: :(")
+    (test (exn:fail:redex:test-term exn) 5))
+  
   (test (output (λ () (redex-check lang d #f)))
         #rx"redex-check: .*:.*\ncounterexample found after 1 attempt:\n5\n")
   (test (output (λ () (redex-check lang d #t))) 
@@ -574,17 +584,29 @@
                                   (--> 0 dontcare z)))))
         #rx"counterexample found after 1 attempt with z:\n0\n")
   
-  (let ([generated null])
+  (let ([generated null]
+        [R (reduction-relation 
+            lang 
+            (--> 1 dontcare)
+            (--> 2 dontcare))])
     (test (output
            (λ ()
              (redex-check lang n (set! generated (cons (term n) generated)) 
                           #:attempts 5
-                          #:source (reduction-relation 
-                                    lang 
-                                    (--> 1 dontcare)
-                                    (--> 2 dontcare)))))
+                          #:source R)))
           #rx"no counterexamples.*with each clause")
-    (test generated '(2 2 1 1)))
+    (test generated '(2 2 1 1))
+    
+    (test (redex-check lang any #t 
+                       #:attempts 1 
+                       #:source R
+                       #:print? (not #t))
+          #t)
+    (test (counterexample-term
+           (redex-check lang any (= (term any) 1)
+                        #:source R
+                        #:print? #f))
+          2))
   
   (let ()
     (define-metafunction lang
@@ -595,7 +617,17 @@
              (redex-check lang (n) (eq? 42 (term n)) 
                           #:attempts 1
                           #:source mf)))
-          #px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n\\(0\\)\n"))
+          #px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n\\(0\\)\n")
+    (test (redex-check lang any #t 
+                       #:attempts 1 
+                       #:source mf
+                       #:print? (not #t))
+          #t)
+    (test (counterexample-term
+           (redex-check lang any (= (car (term any)) 42)
+                        #:source mf
+                        #:print? #f))
+          '(0)))
   
   (let ()
     (define-metafunction lang
@@ -720,6 +752,14 @@
     (E* hole E*)
     (n 4))
   
+  (let ([R (reduction-relation
+            L
+            (--> 1 2)
+            (--> 2 3))])
+    (test (check-reduction-relation R (λ (_) #t) #:print? #f) #t)
+    (test (counterexample-term (check-reduction-relation R (curry = 1) #:print? #f))
+          2))
+  
   (let ([generated null]
         [R (reduction-relation
             L
@@ -787,6 +827,11 @@
   (define-metafunction empty
     [(n (side-condition any #f)) any])
   
+  (test (check-metafunction m (λ (_) #t) #:print? #f) #t)
+  (test (counterexample-term
+         (check-metafunction m (compose (curry = 1) car) #:print? #f))
+        '(2))
+  
   (let ([generated null])
     (test (begin
             (output