diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index 2a0e6974fd..c8cae85b5d 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -579,6 +579,16 @@
                         (if (= attempt finish) 0 'x))))
     (test attempts (list finish retry-threshold start))))
 
+;; output : (-> (-> void) string)
+(define (output thunk)
+  (let ([p (open-output-string)])
+    (parameterize ([current-output-port p])
+      (unless (void? (thunk))
+        (error 'output "expected void result")))
+    (begin0
+      (get-output-string p)
+      (close-output-port p))))
+
 ;; preferred productions
 (let ([make-pick-nt (λ opt (λ req (apply pick-nt (append req opt))))])
   (define-language L
@@ -606,47 +616,45 @@
      '(+ (+ 7 7) (+ 7 7)))
     (test
      (let ([generated null])
-       (check-reduction-relation
-        (reduction-relation L (--> e e))
-        (λ (t) (set! generated (cons t generated)))
-        #:decisions (decisions #:nt (make-pick-nt (make-random)
-                                                  (λ (att rand) #t))
-                               #:pref (list (λ (_) 'dontcare)
-                                            (λ (_) 'dontcare)
-                                            (λ (_) 'dontcare)
-                                            (λ (L) (make-immutable-hash `((e ,(car (pats L))))))
-                                            (λ (L) (make-immutable-hash `((e ,(cadr (pats L))))))))
-        #:attempts 5)
+       (output
+        (λ ()
+          (check-reduction-relation
+           (reduction-relation L (--> e e))
+           (λ (t) (set! generated (cons t generated)))
+           #:decisions (decisions #:nt (make-pick-nt (make-random)
+                                                     (λ (att rand) #t))
+                                  #:pref (list (λ (_) 'dontcare)
+                                               (λ (_) 'dontcare)
+                                               (λ (_) 'dontcare)
+                                               (λ (L) (make-immutable-hash `((e ,(car (pats L))))))
+                                               (λ (L) (make-immutable-hash `((e ,(cadr (pats L))))))))
+           #:attempts 5)))
        generated)
      '((* 7 7) (+ 7 7) 7 7 7))))
 
-;; output : (-> (-> void) string)
-(define (output thunk)
-  (let ([p (open-output-string)])
-    (parameterize ([current-output-port p])
-      (unless (void? (thunk))
-        (error 'output "expected void result")))
-    (begin0
-      (get-output-string p)
-      (close-output-port p))))
-
 ;; redex-check
 (let ()
   (define-language lang
     (d 5)
     (e e 4)
     (n number))
-  (test (output (λ () (redex-check lang d #f))) 
-        "counterexample found after 1 attempt:\n5\n")
-  (test (output (λ () (redex-check lang d #t))) "")
+  (test (output (λ () (redex-check lang d #f)))
+        #rx"redex-check: .*:.*\ncounterexample found after 1 attempt:\n5\n")
+  (test (output (λ () (redex-check lang d #t))) 
+        #rx"redex-check: .*:.*\nno counterexamples in 1000 attempts\n")
+  (let-syntax ([noloc (λ (stx)
+                        (syntax-case stx ()
+                          [(_ e) (datum->syntax stx (syntax->datum #'e) #f)]))])
+    (test (output (λ () (noloc (redex-check lang d #t)))) 
+          "redex-check: no counterexamples in 1000 attempts\n"))
   (test (output (λ () (redex-check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2)))
-        "")
+        #rx"no counterexamples")
   (test (output (λ () (redex-check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2)))
-        "")
+        #rx"no counterexamples")
   (test (output (λ () (redex-check lang (d e) #f)))
-        "counterexample found after 1 attempt:\n(5 4)\n")
+        #rx"counterexample found after 1 attempt:\n\\(5 4\\)\n")
   (let* ([p (open-output-string)]
-         [m (parameterize ([current-error-port p])
+         [m (parameterize ([current-output-port p])
               (with-handlers ([exn:fail? exn-message])
                 (redex-check lang d (error 'pred-raised))
                 'no-exn-raised))])
@@ -662,7 +670,7 @@
                                   lang 
                                   (--> 42 dontcare)
                                   (--> 0 dontcare z)))))
-        "counterexample found after 1 attempt with z:\n0\n")
+        #rx"counterexample found after 1 attempt with z:\n0\n")
   
   (let ([generated null])
     (test (output
@@ -673,7 +681,7 @@
                                     lang 
                                     (--> 1 dontcare)
                                     (--> 2 dontcare)))))
-          "")
+          #rx"no counterexamples.*with each clause")
     (test generated '(2 2 1 1)))
   
   (let ()
@@ -685,7 +693,7 @@
              (redex-check lang (n) (eq? 42 (term n)) 
                           #:attempts 1
                           #:source mf)))
-          "counterexample found after 1 attempt with clause #2:\n(0)\n"))
+          #rx"counterexample found after 1 attempt with clause #2:\n\\(0\\)\n"))
   
   (let ()
     (define-metafunction lang
@@ -697,13 +705,12 @@
                                (= (term number_2) 4)) 
                           #:attempts 1
                           #:source mf)))
-          ""))
+          #rx"no counterexamples"))
   
-  (let ()
-    (test (raised-exn-msg 
-           exn:fail:redex?
-           (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
-          #rx"x does not match n"))
+  (test (raised-exn-msg 
+         exn:fail:redex?
+         (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
+        #rx"x does not match n")
   (test (raised-exn-msg
          exn:fail:redex?
          (redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
@@ -747,14 +754,14 @@
            (parameterize ([generation-decisions 
                            (decisions #:num (list (λ _ 2) (λ _ 5)))])
              (check-metafunction-contract f))))
-        "counterexample found after 1 attempt:\n(5)\n")
+        #rx"check-metafunction-contract:.*counterexample found after 1 attempt:\n\\(5\\)\n")
   ;; Rng(f) > Codom(f)
   (test (output
          (λ () 
            (parameterize ([generation-decisions
                            (decisions #:num (list (λ _ 3)))])
              (check-metafunction-contract f))))
-        "counterexample found after 1 attempt:\n(3)\n")
+        #rx"counterexample found after 1 attempt:\n\\(3\\)\n")
   ;; LHS matches multiple ways
   (test (output
          (λ () 
@@ -762,11 +769,11 @@
                            (decisions #:num (list (λ _ 1) (λ _ 1))
                                       #:seq (list (λ _ 2)))])
              (check-metafunction-contract g))))
-        "counterexample found after 1 attempt:\n(1 1)\n")
+        #rx"counterexample found after 1 attempt:\n\\(1 1\\)\n")
   ;; OK -- generated from Dom(h)
-  (test (output (λ () (check-metafunction-contract h))) "")
+  (test (output (λ () (check-metafunction-contract h))) #rx"no counterexamples")
   ;; OK -- generated from pattern (any ...)
-  (test (output (λ () (check-metafunction-contract i #:attempts 5))) "")
+  (test (output (λ () (check-metafunction-contract i #:attempts 5))) #rx"no counterexamples")
   
   ;; Unable to generate domain
   (test (raised-exn-msg
@@ -791,22 +798,25 @@
             [(--> (in-hole E a) whatever)
              (==> a b)])])
     (test (begin
-            (check-reduction-relation 
-             R (λ (term) (set! generated (cons term generated)))
-             #:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
-                                    #:num (list (λ _ 1) (λ _ 1) (λ _ 0)))
-             #:attempts 1)
+            (output
+             (λ ()
+               (check-reduction-relation 
+                R (λ (term) (set! generated (cons term generated)))
+                #:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
+                                       #:num (list (λ _ 1) (λ _ 1) (λ _ 0)))
+                #:attempts 1)))
             generated)
           (reverse '((+ (+)) 0))))
   
   (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
-    (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1))) "")
+    (test (output (λ () (check-reduction-relation S (λ (x) #t) #:attempts 1)))
+          #rx"check-reduction-relation:.*no counterexamples")
     (test (output 
            (λ () (check-reduction-relation S (λ (x) #f))))
-          "counterexample found after 1 attempt with name:\n1\n")
+          #rx"counterexample found after 1 attempt with name:\n1\n")
     (test (output 
            (λ () (check-reduction-relation S (curry eq? 1))))
-          "counterexample found after 1 attempt with unnamed:\n3\n"))
+          #rx"counterexample found after 1 attempt with unnamed:\n3\n"))
   
   (let ([T (reduction-relation
             L
@@ -824,7 +834,7 @@
               T (curry equal? '(9 4)) 
               #:attempts 1
               #:decisions (decisions #:num (build-list 5 (λ (x) (λ _ x)))))))
-          ""))
+          #rx"no counterexamples"))
   
   (let ([U (reduction-relation L (--> (side-condition any #f) any))])
     (test (raised-exn-msg
@@ -842,12 +852,14 @@
     [(n (side-condition any #f)) any])
   (let ([generated null])
     (test (begin
-            (check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)
+            (output 
+             (λ ()
+               (check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)))
             generated) 
           (reverse '((1) (2)))))
-  (test (output (λ () (check-metafunction m (λ (_) #t)))) "")
+  (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
   (test (output (λ () (check-metafunction m (curry eq? 1))))
-        #rx"counterexample found after 1 attempt with clause #1")
+        #rx"check-metafunction:.*counterexample found after 1 attempt with clause #1")
   (test (raised-exn-msg
           exn:fail:contract?
           (check-metafunction m (λ (_) #t) #:attempts 'NaN))
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 65b9b00463..5f0376d566 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -696,6 +696,9 @@ To do a better job of not generating programs with free variables,
 (define (assert-nat name x)
   (unless (and (integer? x) (>= x 0))
     (raise-type-error name "natural number" x)))
+(define (assert-rel name x)
+  (unless (reduction-relation? x)
+    (raise-type-error 'redex-check "reduction-relation" x)))
 
 (define-for-syntax (term-generator lang pat decisions@ retries what)
   (with-syntax ([pattern 
@@ -719,6 +722,22 @@ To do a better job of not generating programs with free variables,
     [(_ lang pat size)
      (syntax/loc stx (generate-term lang pat size #:attempt 1))]))
 
+(define-for-syntax (show-message stx)
+  (syntax-case stx ()
+    [(what . _)
+     (identifier? #'what)
+     (with-syntax ([loc (if (and (path? (syntax-source stx))
+                                 (syntax-line stx))
+                            (format "~a:~a"
+                                    (path->string (syntax-source stx)) 
+                                    (syntax-line stx))
+                            #f)])
+       #`(λ (msg)
+           (fprintf 
+            (current-output-port)
+            "~a: ~a~a"
+            'what (if loc (string-append loc "\n") "") msg)))]))
+
 (define-syntax (redex-check stx)
   (syntax-case stx ()
     [(_ lang pat property . kw-args)
@@ -735,7 +754,8 @@ To do a better job of not generating programs with free variables,
        (with-syntax ([(name ...) names]
                      [(name/ellipses ...) names/ellipses]
                      [attempts attempts-stx]
-                     [retries retries-stx])
+                     [retries retries-stx]
+                     [show (show-message stx)])
          (with-syntax ([property (syntax
                                   (λ (_ bindings)
                                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
@@ -756,49 +776,57 @@ To do a better job of not generating programs with free variables,
                                                       (metafunc-proc-lang #,m)))]
                                     [else
                                      #`(let ([r #,source-stx])
-                                         (unless (reduction-relation? r)
-                                           (raise-type-error 'redex-check "reduction-relation" r))
+                                         (assert-rel 'redex-check r)
                                          (values
                                           (map rewrite-proc-lhs (reduction-relation-make-procs r))
                                           (reduction-relation-srcs r)
                                           (reduction-relation-lang r)))])])
-                        (check-property-many 
+                        (check-prop-srcs 
                          lang pats srcs property random-decisions@ (max 1 (floor (/ att (length pats)))) ret
                          'redex-check
+                         show
                          (test-match lang pat)
                          (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
-                    #`(check-property
+                    #`(check-prop
                        #,(term-generator #'lang #'pat #'random-decisions@ #'ret 'redex-check)
-                       property att)))
+                       property att show)))
                (void))))))]))
 
-(define (check-property generator property attempts 
-                        #:source [source #f]
-                        #:match [match #f]
-                        #:match-fail [match-fail #f])
+(define (format-attempts a)
+  (format "~a attempt~a" a (if (= 1 a) "" "s")))
+
+(define (check-prop generator property attempts show)
+  (when (check generator property attempts show)
+    (show (format "no counterexamples in ~a\n"
+                  (format-attempts attempts)))))
+
+(define (check generator property attempts show
+               #:source [source #f]
+               #:match [match #f]
+               #:match-fail [match-fail #f])
   (let loop ([remaining attempts])
     (if (zero? remaining)
         #t
         (let ([attempt (add1 (- attempts remaining))])
           (let-values ([(term bindings) (generator (attempt->size attempt) attempt)])
             (if (andmap (λ (bindings) 
-                          (with-handlers ([exn:fail? (λ (exn) 
-                                                       (fprintf (current-error-port) 
-                                                                "checking ~s raises an exception\n"
-                                                                term)
-                                                       (raise exn))])
+                          (with-handlers 
+                              ([exn:fail?
+                                (λ (exn) 
+                                  (show 
+                                   (format "checking ~s raises an exception\n" term))
+                                  (raise exn))])
                             (property term bindings)))
-                        (cond [(and match (match term)) 
+                        (cond [(and match match-fail (match term)) 
                                => (curry map (compose make-bindings match-bindings))]
                               [match (match-fail term)]
                               [else (list bindings)]))
                 (loop (sub1 remaining))
                 (begin
-                  (fprintf (current-output-port)
-                           "counterexample found after ~a attempt~a~a:\n"
-                           attempt
-                           (if (= attempt 1) "" "s")
-                           (if source (format " with ~a" source) ""))
+                  (show
+                   (format "counterexample found after ~a~a:\n"
+                           (format-attempts attempt)
+                           (if source (format " with ~a" source) "")))
                   (pretty-print term (current-output-port))
                   #f)))))))
 
@@ -811,33 +839,39 @@ To do a better job of not generating programs with free variables,
                     (parse-kw-args `((#:attempts . ,#'default-check-attempts)
                                      (#:retries . ,#'default-retries))
                                    (syntax kw-args)
-                                   stx)])
+                                   stx)]
+                   [show (show-message stx)])
        (syntax/loc stx 
         (let ([lang (metafunc-proc-lang m)]
               [dom (metafunc-proc-dom-pat m)]
               [decisions@ (generation-decisions)]
               [att attempts])
           (assert-nat 'check-metafunction-contract att)
-          (check-property 
+          (check-prop 
            ((generate lang decisions@ retries 'check-metafunction-contract)
             (if dom dom '(any (... ...))))
            (λ (t _) 
              (with-handlers ([exn:fail:redex? (λ (_) #f)])
                (begin (term (name ,@t)) #t)))
-           att)
-          (void))))]))
+           att
+           show))))]))
 
-(define (check-property-many lang pats srcs prop decisions@ attempts retries what [match #f] [match-fail #f])
+(define (check-prop-srcs lang pats srcs prop decisions@ attempts retries what show
+                         [match #f]
+                         [match-fail #f])
   (let ([lang-gen (generate lang decisions@ retries what)])
-    (for/and ([pat pats] [src srcs])
-      (check-property
-       (lang-gen pat)
-       prop
-       attempts
-       #:source src
-       #:match match
-       #:match-fail match-fail))
-    (void)))
+    (when (for/and ([pat pats] [src srcs])
+            (check
+             (lang-gen pat)
+             prop
+             attempts
+             show
+             #:source src
+             #:match match
+             #:match-fail match-fail))
+      (show
+       (format "no counterexamples in ~a (with each clause)\n"
+               (format-attempts attempts))))))
 
 (define (metafunc-srcs m)
   (build-list (length (metafunc-proc-lhs-pats m))
@@ -845,20 +879,19 @@ To do a better job of not generating programs with free variables,
 
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()
-    [(_ name property)
-     (syntax/loc stx (check-metafunction name property #:attempts default-check-attempts))]
     [(_ name property . kw-args)
      (with-syntax ([m (metafunc/err #'name stx)]
                    [(attempts retries)
                     (parse-kw-args `((#:attempts . , #'default-check-attempts)
                                      (#:retries . ,#'default-retries))
                                    (syntax kw-args)
-                                   stx)])
+                                   stx)]
+                   [show (show-message stx)])
        (syntax/loc stx
          (let ([att attempts]
                [ret retries])
            (assert-nat 'check-metafunction att)
-           (check-property-many 
+           (check-prop-srcs 
             (metafunc-proc-lang m)
             (metafunc-proc-lhs-pats m)
             (metafunc-srcs m)
@@ -866,26 +899,39 @@ To do a better job of not generating programs with free variables,
             (generation-decisions)
             att
             ret
-            'check-metafunction))))]))
+            'check-metafunction
+            show))))]))
 
 (define (reduction-relation-srcs r)
   (map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
        (reduction-relation-make-procs r)))
 
-(define (check-reduction-relation 
-         relation property 
-         #:decisions [decisions@ random-decisions@]
-         #:attempts [attempts default-check-attempts]
-         #:retries [retries default-retries])
-  (check-property-many
-   (reduction-relation-lang relation)
-   (map rewrite-proc-lhs (reduction-relation-make-procs relation))
-   (reduction-relation-srcs relation)
-   (λ (term _) (property term))
-   decisions@
-   attempts
-   retries
-   'check-reduction-relation))
+(define-syntax (check-reduction-relation stx)
+  (syntax-case stx ()
+    [(_ relation property . kw-args)
+     (with-syntax ([(attempts retries decisions@)
+                    (parse-kw-args `((#:attempts . , #'default-check-attempts)
+                                     (#:retries . ,#'default-retries)
+                                     (#:decisions . ,#'random-decisions@))
+                                   (syntax kw-args)
+                                   stx)]
+                   [show (show-message stx)])
+       (syntax/loc stx
+         (let ([att attempts]
+               [ret retries]
+               [rel relation])
+           (assert-nat 'check-reduction-relation att)
+           (assert-rel 'check-reduction-relation rel)
+           (check-prop-srcs
+            (reduction-relation-lang rel)
+            (map rewrite-proc-lhs (reduction-relation-make-procs rel))
+            (reduction-relation-srcs rel)
+            (λ (term _) (property term))
+            decisions@
+            attempts
+            retries
+            'check-reduction-relation
+            show))))]))
 
 (define-signature decisions^
   (next-variable-decision
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index c32ada5c18..35d67463dd 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -1101,11 +1101,12 @@ argument @scheme[retries-expr] (default @scheme[100]) bounds the number of times
                            [relation-expr reduction-relation?]
                            [retries-expr natural-number/c])]{
 Searches for a counterexample to @scheme[property-expr], interpreted
-as a predicate universally quantified over its free
-@pattech[term]-variables. @scheme[redex-check] chooses substitutions for 
-these free @pattech[term]-variables by generating random terms matching
-@scheme[pattern] and extracting the sub-terms bound by the
-@pattech[names] and non-terminals in @scheme[pattern].
+as a predicate universally quantified over the pattern variables
+bound by @scheme[pattern]. @scheme[redex-check] constructs and tests 
+a candidate counterexample by choosing a random term @math{t} that 
+matches @scheme[pattern] then evaluating @scheme[property-expr]
+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
@@ -1156,22 +1157,22 @@ term that does not match @scheme[pattern].}
           #:attempts 3
           #:source R))]
 
-@defproc[(check-reduction-relation 
-          [relation reduction-relation?]
-          [property (-> any/c any/c)]
-          [#:attempts attempts natural-number/c 1000]
-          [#:retries retries natural-number/c 100])
-         void?]{
+@defform/subs[(check-reduction-relation relation property kw-args ...)
+              ([kw-arg (code:line #:attempts attempts-expr)
+                       (code:line #:retries retries-expr)])
+              #:contracts ([property (-> any/c any/c)]
+                           [attempts-expr natural-number/c]
+                           [retries-expr natural-number/c])]{
 Tests @scheme[relation] as follows: for each case of @scheme[relation],
 @scheme[check-reduction-relation] generates @scheme[attempts] random
 terms that match that case's left-hand side and applies @scheme[property] 
 to each random term.
 
-This function provides a more convenient notation for
+This form provides a more convenient notation for
 @schemeblock[(redex-check L any (property (term any)) 
                           #:attempts (* n attempts)
                           #:source relation)]
-when @scheme[relation] is a relation on @scheme[L] and has @scheme[n] rules.}
+when @scheme[relation] is a relation on @scheme[L] with @scheme[n] rules.}
 
 @defform/subs[(check-metafunction metafunction property kw-args ...)
               ([kw-arg (code:line #:attempts attempts-expr)
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index 1cad442633..773dbaab19 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -45,7 +45,8 @@
 (provide redex-check
          generate-term
          check-metafunction
-         check-metafunction-contract)
+         check-metafunction-contract
+         check-reduction-relation)
 
 (provide/contract
  [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]
@@ -66,10 +67,6 @@
                   (-> bindings? symbol? (-> any) any))]
  [variable-not-in (any/c symbol? . -> . symbol?)]
  [variables-not-in (any/c (listof symbol?) . -> . (listof symbol?))]
- [check-reduction-relation (->* (reduction-relation? (-> any/c any/c))
-                                (#:attempts natural-number/c
-                                 #:retries natural-number/c)
-                                (one-of/c #t (void)))]
  [relation-coverage (parameter/c (or/c false/c coverage?))]
  [make-coverage (-> reduction-relation? coverage?)]
  [covered-cases (-> coverage? (listof (cons/c string? natural-number/c)))])