diff --git a/collects/redex/private/error.ss b/collects/redex/private/error.ss
index 62e71b8e3d..8d9bfbb33c 100644
--- a/collects/redex/private/error.ss
+++ b/collects/redex/private/error.ss
@@ -4,4 +4,5 @@
   (let ([str (format "~a: ~a" name (apply format fmt args))])
     (raise (make-exn:fail:redex str (current-continuation-marks)))))
 (provide redex-error
-         exn:fail:redex?)
+         exn:fail:redex?
+         (struct-out exn:fail:redex))
diff --git a/collects/redex/private/matcher-test.ss b/collects/redex/private/matcher-test.ss
index 94fc3ff8ea..a2be3fbf12 100644
--- a/collects/redex/private/matcher-test.ss
+++ b/collects/redex/private/matcher-test.ss
@@ -417,21 +417,21 @@
                             '(a (b (c (d e))))
                             none)))
     
-    (test-empty `(+ 1 (side-condition any ,(lambda (bindings) #t)))
+    (test-empty `(+ 1 (side-condition any ,(lambda (bindings) #t) #t))
                 '(+ 1 b)
                 (list (make-test-mtch (make-bindings (list (make-bind 'any 'b))) '(+ 1 b) none)))
-    (test-empty `(+ 1 (side-condition any ,(lambda (bindings) #f)))
+    (test-empty `(+ 1 (side-condition any ,(lambda (bindings) #f) #f))
                 '(+ 1 b)
                 #f)
     
-    (test-empty `(+ 1 (side-condition b ,(lambda (bindings) #t)))
+    (test-empty `(+ 1 (side-condition b ,(lambda (bindings) #t) #t))
                 '(+ 1 b)
                 (list (make-test-mtch (make-bindings '()) '(+ 1 b) none)))
-    (test-empty `(+ 1 (side-condition a ,(lambda (bindings) #t)))
+    (test-empty `(+ 1 (side-condition a ,(lambda (bindings) #t)) #t)
                 '(+ 1 b)
                 #f)
 
-    (test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))
+    (test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a))
                 'a
                 (list 
                  (make-test-mtch (make-bindings (list (make-bind 'x 'a)
@@ -439,7 +439,7 @@
                             'a
                             none)))
 
-    (test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))))
+    (test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a)))
                 '(+ 1 a)
                 (list 
                  (make-test-mtch (make-bindings (list (make-bind 'x 'a)
@@ -447,16 +447,17 @@
                             '(+ 1 a)
                             none)))
 
-    (test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))
+    (test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a))
                 'b
                 #f)
     
-    (test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))))
+    (test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)) (eq? (term x) 'a)))
                 '(+ 1 b)
                 #f)
     
     (test-empty `(side-condition ((any_1 ..._a) (any_2 ..._a))
-                                 ,(lambda (bindings) (error 'should-not-be-called)))
+                                 ,(lambda (bindings) (error 'should-not-be-called))
+                                 (error 'should-not-be-called))
                 '((1 2 3) (4 5))
                 #f)
     
diff --git a/collects/redex/private/matcher.ss b/collects/redex/private/matcher.ss
index f29f7c92e8..c66afd4814 100644
--- a/collects/redex/private/matcher.ss
+++ b/collects/redex/private/matcher.ss
@@ -211,7 +211,7 @@ before the pattern compiler is invoked.
        (loop p1)
        (loop p2)]
       [`(hide-hole ,p) (loop p)]
-      [`(side-condition ,p ,g)
+      [`(side-condition ,p ,g ,e)
        (loop p)]
       [`(cross ,s) (void)]
       [_
@@ -247,7 +247,7 @@ before the pattern compiler is invoked.
        [`(in-hole ,context ,contractum)
         (recur contractum)]
        [`(hide-hole ,arg) #f]
-       [`(side-condition ,pat ,condition)
+       [`(side-condition ,pat ,condition ,expr)
         (recur pat)]
        [(? list?)
         (ormap recur pattern)]
@@ -414,10 +414,10 @@ before the pattern compiler is invoked.
           (let ([m (loop p)])
             (lambda (l)
               `(hide-hole ,(m l))))]
-         [`(side-condition ,pat ,condition)
+         [`(side-condition ,pat ,condition ,expr)
           (let ([patf (loop pat)])
             (lambda (l)
-              `(side-condition ,(patf l) ,condition)))]
+              `(side-condition ,(patf l) ,condition ,expr)))]
          [(? list?)
           (let ([f/pats
                  (let l-loop ([pattern pattern])
@@ -505,7 +505,7 @@ before the pattern compiler is invoked.
      (recur context)]
     [`(hide-hole ,p)
      (recur p)]
-    [`(side-condition ,pat ,condition)
+    [`(side-condition ,pat ,condition ,expr)
      (recur pat)]
     [(? list?)
      #t]
@@ -554,7 +554,7 @@ before the pattern compiler is invoked.
      (recur context)]
     [`(hide-hole ,p)
      (recur p)]
-    [`(side-condition ,pat ,condition)
+    [`(side-condition ,pat ,condition ,expr)
      (recur pat)]
     [(? list?)
      #f]
@@ -765,7 +765,7 @@ before the pattern compiler is invoked.
                         matches))))
           #f))]
       
-      [`(side-condition ,pat ,condition)
+      [`(side-condition ,pat ,condition ,expr)
        (let-values ([(match-pat has-hole?) (compile-pattern/default-cache pat)])
          (values
           (lambda (exp hole-info)
@@ -1485,7 +1485,7 @@ before the pattern compiler is invoked.
            (loop pat (cons (make-bind name '()) ribs)))]
       [`(in-hole ,context ,contractum) (loop context (loop contractum ribs))]
       [`(hide-hole ,p) (loop p ribs)]
-      [`(side-condition ,pat ,test) (loop pat ribs)]
+      [`(side-condition ,pat ,test ,expr) (loop pat ribs)]
       [(? list?)
        (let-values ([(rewritten has-hole?) (rewrite-ellipses non-underscore-binder? pattern (lambda (x) (values x #f)))])
          (let i-loop ([r-exps rewritten]
diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index 8598fdc5f6..a047ccb320 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -162,6 +162,7 @@
                                acc)))])))))
          (rewrite-proc-name make-proc)
          (rewrite-proc-lhs make-proc)
+         (rewrite-proc-lhs-src make-proc)
          (rewrite-proc-id make-proc)))
       (reduction-relation-make-procs red))
      (reduction-relation-rule-names red)
@@ -693,9 +694,11 @@
                                   'predicate
                                   #'#t)])
           (with-syntax ([side-conditions-rewritten (rw-sc from)]
-                        [lhs-w/extras (rw-sc #`(side-condition 
-                                                #,from
-                                                #,test-case-body-code))]
+                        [lhs-w/extras (rw-sc #`(side-condition #,from #,test-case-body-code))]
+                        [lhs-source (format "~a:~a:~a"
+                                            (syntax-source from)
+                                            (syntax-line from)
+                                            (syntax-column from))]
                         [name name]
                         [lang lang]
                         [(names ...) names]
@@ -733,6 +736,7 @@
                            other-matches)))))
                name
                (λ (lang) (let (test-case-compile-pattern-bindings ...) `lhs-w/extras))
+               lhs-source
                case-id)))))))
   
   (define (process-extras stx orig-name name-table extras)
@@ -926,6 +930,7 @@
                other-matches)))))
    (rewrite-proc-name child-make-proc)
    (λ (lang) (subst lhs-frm-id ((rewrite-proc-lhs child-make-proc) lang) rhs-from))
+   (rewrite-proc-lhs child-make-proc)
    (rewrite-proc-id child-make-proc)))
 
 (define relation-coverage (make-parameter #f))
@@ -989,7 +994,7 @@
                           (symbol->string (bind-name y))))))
 
 (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
-  (make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
+  (make-struct-type 'metafunc-proc #f 11 0 #f null (current-inspector) 0))
 (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
 (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
 (define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
@@ -999,6 +1004,7 @@
 (define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 7))
 (define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 8))
 (define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
+(define metafunc-proc-src-locs (make-struct-field-accessor metafunc-proc-ref 10))
 (define-struct metafunction (proc))
 
 (define-syntax (in-domain? stx)
@@ -1105,7 +1111,7 @@
                                   (tl-side-cond/binds ...))
                                  (parse-extras #'((stuff ...) ...))])
                       (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
-                                     (map (λ (sc/b rhs) 
+                                     (map (λ (sc/b rhs)
                                             (let-values ([(body-code cp-let-bindings) 
                                                           (bind-withs
                                                            syn-error-name '()  
@@ -1140,6 +1146,13 @@
                                                     #t
                                                     x))
                                             (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
+                                      [(clause-src ...)
+                                       (map (λ (lhs)
+                                              (format "~a:~a:~a"
+                                                      (syntax-source lhs)
+                                                      (syntax-line lhs)
+                                                      (syntax-column lhs)))
+                                            pats)]
                                       [dom-side-conditions-rewritten
                                        (and dom-ctcs
                                             (rewrite-side-conditions/check-errs
@@ -1252,7 +1265,8 @@
                                          rhss
                                          (let ([name (lambda (x) (name-predicate x))]) name)
                                          dsc
-                                         rg-sc))
+                                         rg-sc
+                                         `(clause-src ...)))
                                       dsc
                                       `codom-side-conditions-rewritten
                                       'name
@@ -1279,7 +1293,7 @@
     ;; initial test determines if a contract is specified or not
     (cond
       [(pair? (syntax-e (car (syntax->list rest))))
-       (values #f #f #'any (check-clauses stx syn-error-name rest relation?))]
+       (values #f #f #'any (check-clauses stx syn-error-name (syntax->list rest) relation?))]
       [else
        (syntax-case rest ()
          [(id colon more ...)
@@ -2140,6 +2154,8 @@
          metafunc-proc-in-dom?
          metafunc-proc-dom-pat
          metafunc-proc-lhs-pats
+         metafunc-proc-src-locs
+         metafunc-proc?
          
          (struct-out binds))
 
diff --git a/collects/redex/private/rewrite-side-conditions.ss b/collects/redex/private/rewrite-side-conditions.ss
index 2d41087d01..4f853a95fe 100644
--- a/collects/redex/private/rewrite-side-conditions.ss
+++ b/collects/redex/private/rewrite-side-conditions.ss
@@ -42,14 +42,18 @@
          (with-syntax ([pat (loop (syntax pre-pat))])
            (let-values ([(names names/ellipses) (extract-names all-nts what bind-names? (syntax pat))])
              (with-syntax ([(name ...) names]
-                           [(name/ellipses ...) names/ellipses])
+                           [(name/ellipses ...) names/ellipses]
+                           [src-loc (parameterize ([print-syntax-width 0])
+                                      (format "~s" #'exp))])
                (syntax/loc term
                  (side-condition
                   pat
                   ,(lambda (bindings)
                      (term-let
                       ([name/ellipses (lookup-binding bindings 'name)] ...)
-                      exp)))))))]
+                      exp))
+                  ; For use in error messages.
+                  src-loc)))))]
         [(side-condition a ...) (expected-exact 'side-condition 2 term)]
         [side-condition (expected-arguments 'side-condition term)]
         [(variable-except a ...) #`(variable-except #,@(map loop (syntax->list (syntax (a ...)))))]
@@ -101,7 +105,7 @@
                  (loop (syntax pat1)
                        (loop (syntax pat2) names depth)
                        depth)]
-                [(side-condition pat e)
+                [(side-condition pat . rest)
                  (loop (syntax pat) names depth)]
                 [(pat ...)
                  (let i-loop ([pats (syntax->list (syntax (pat ...)))]
diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index dc6520eb2d..7b402a9148 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -267,7 +267,7 @@
         null)
   (test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
         '(4 4 4 4 (4 4) (4 4)))
-  (test (raised-exn-msg exn:fail:redex? (generate-term lang e 5 #:retries 42)) 
+  (test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang e 5 #:retries 42)) 
         #rx"generate-term: unable to generate pattern e in 42")
   (test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
   (test (generate-term/decisions 
@@ -319,7 +319,7 @@
     (decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
    '(1 1 2))
   (test
-   (raised-exn-msg exn:fail:redex? (generate-term lang b 5000))
+   (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang b 5000))
    #rx"unable"))
 
 (let ()
@@ -342,10 +342,10 @@
     (x variable))
   (test (generate-term lang b 5) 43)
   (test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
-  (test (raised-exn-msg exn:fail:redex? (generate-term lang c 5))
-        #rx"unable to generate")
+  (test (raised-exn-msg exn:fail:redex:generation-failure? (generate-term lang c 5))
+        #px"unable to generate pattern \\(side-condition a\\_1 #<syntax:.*\\/rg-test\\.ss:\\d+:\\d+>\\)")
   (test (let/ec k
-          (generate-term lang (number_1 (side-condition any (k (term number_1)))) 5))
+          (generate-term lang (number_1 (side-condition 7 (k (term number_1)))) 5))
         'number_1)
   
   (test ; mismatch patterns work with side-condition failure/retry
@@ -665,7 +665,19 @@
              (redex-check lang (n) (eq? 42 (term n)) 
                           #:attempts 1
                           #:source mf)))
-          #rx"counterexample found after 1 attempt with clause #2:\n\\(0\\)\n"))
+          #px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n\\(0\\)\n"))
+  
+  (let ()
+    (define-metafunction lang
+      [(f) 
+       dontcare
+       (side-condition #f)])
+    (test (raised-exn-msg
+           exn:fail:redex:generation-failure?
+           (redex-check lang any #t 
+                        #:attempts 1
+                        #:source f))
+          #px"unable to generate LHS of clause at .*:\\d+:\\d+"))
   
   (let ()
     (define-metafunction lang
@@ -684,18 +696,29 @@
          (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
         #rx"x does not match n")
   (test (raised-exn-msg
-         exn:fail:redex?
+         exn:fail:redex:generation-failure?
          (redex-check lang (side-condition any #f) #t #:retries 42 #:attempts 1))
         #rx"^redex-check: unable .* in 42")
-  (test (raised-exn-msg
-         exn:fail:redex?
-         (redex-check lang any #t 
-                      #:source (reduction-relation 
-                                lang
-                                (--> (side-condition any #f) any))
-                      #:retries 42
-                      #:attempts 1))
-        #rx"^redex-check: unable .* in 42"))
+  (let-syntax ([test-gen-fail
+                (syntax-rules ()
+                  [(_ rhs expected)
+                   (test 
+                    (raised-exn-msg
+                     exn:fail:redex:generation-failure?
+                     (redex-check lang any #t 
+                                  #:source (reduction-relation 
+                                            lang
+                                            rhs)
+                                  #:retries 42
+                                  #:attempts 1))
+                    expected)])])
+    (test-gen-fail 
+     (--> (side-condition any #f) any)
+     #px"^redex-check: unable to generate LHS of clause at .*:\\d+:\\d+ in 42")
+    
+    (test-gen-fail
+     (--> (side-condition any #f) any impossible)
+     #rx"^redex-check: unable to generate LHS of impossible in 42")))
 
 ;; check-metafunction-contract
 (let ()
@@ -749,7 +772,7 @@
   
   ;; Unable to generate domain
   (test (raised-exn-msg
-         exn:fail:redex?
+         exn:fail:redex:generation-failure?
          (check-metafunction-contract j #:attempts 1 #:retries 42))
         #rx"^check-metafunction-contract: unable .* in 42"))
 
@@ -788,7 +811,11 @@
           #rx"counterexample found after 1 attempt with name:\n1\n")
     (test (output 
            (λ () (check-reduction-relation S (curry eq? 1))))
-          #rx"counterexample found after 1 attempt with unnamed:\n3\n"))
+          #px"counterexample found after 1 attempt with clause at .*:\\d+:\\d+:\n3\n"))
+  
+  (test (output 
+         (λ () (check-reduction-relation (reduction-relation L (--> 1 2) (--> 3 4 name)) (curry eq? 1))))
+        #px"counterexample found after 1 attempt with name:\n3\n")
   
   (let ([T (reduction-relation
             L
@@ -810,7 +837,7 @@
   
   (let ([U (reduction-relation L (--> (side-condition any #f) any))])
     (test (raised-exn-msg
-           exn:fail:redex?
+           exn:fail:redex:generation-failure?
            (check-reduction-relation U (λ (_) #t)))
           #rx"^check-reduction-relation: unable")))
 
@@ -847,13 +874,13 @@
   
   (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
   (test (output (λ () (check-metafunction m (curry eq? 1))))
-        #rx"check-metafunction:.*counterexample found after 1 attempt with clause #1")
+        #px"check-metafunction:.*counterexample found after 1 attempt with clause at .*:\\d+:\\d+")
   (test (raised-exn-msg
           exn:fail:contract?
           (check-metafunction m (λ (_) #t) #:attempts 'NaN))
         #rx"check-metafunction: expected")
   (test (raised-exn-msg
-         exn:fail:redex?
+         exn:fail:redex:generation-failure?
          (check-metafunction n (λ (_) #t) #:retries 42))
         #rx"check-metafunction: unable .* in 42"))
 
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 091f8ec73e..da9a09ae2b 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -171,6 +171,12 @@
         [parsed (parse-language lang)])
     (make-rg-lang parsed lits (find-base-cases parsed))))
 
+(define-struct (exn:fail:redex:generation-failure exn:fail:redex) ())
+(define (raise-gen-fail who what attempts)
+  (let ([str (format "~a: unable to generate ~a in ~a attempt~a" 
+                     who what attempts (if (= attempts 1) "" "s"))])
+    (raise (make-exn:fail:redex:generation-failure str (current-continuation-marks)))))
+
 (define (generate lang decisions@ user-gen retries what)
   (define-values/invoke-unit decisions@
     (import) (export decisions^))
@@ -231,10 +237,7 @@
                   [size init-sz]
                   [attempt init-att])
         (if (zero? remaining)
-            (redex-error what "unable to generate pattern ~s in ~a attempt~a" 
-                         name 
-                         retries
-                         (if (= retries 1) "" "s"))
+            (raise-gen-fail what (format "pattern ~a" name) retries)
             (let-values ([(term env) (gen size attempt)])
               (if (pred term env)
                   (values term env)
@@ -317,8 +320,8 @@
         [`string 
          (values ((next-string-decision) (rg-lang-lits lang) attempt)
                  env)]
-        [`(side-condition ,pat ,(? procedure? condition))
-         (generate/pred (unparse-pattern pat) 
+        [`(side-condition ,pat ,(? procedure? condition) ,guard-src-loc)
+         (generate/pred `(side-condition ,(unparse-pattern pat) ,guard-src-loc) 
                         (recur/pat/size-attempt pat)
                         (λ (_ env) (condition (bindings env)))
                         size attempt)]
@@ -575,6 +578,9 @@
       [(and (? (λ (_) (not (eq? mode 'cross)))) `(cross ,(and (? (is-nt? lang)) nt)))
        (let ([nt-str (symbol->string nt)])
          (values `(cross ,(string->symbol (string-append nt-str "-" nt-str))) vars))]
+      [`(side-condition ,pat ,guard ,guard-src-loc)
+       (let-values ([(parsed vars) (recur pat vars)])
+         (values `(side-condition ,parsed ,guard ,guard-src-loc) vars))]
       [(cons first rest)
        (let-values ([(first-parsed vars) (recur first vars)])
          (let-values ([(rest-parsed vars) (recur rest vars)])
@@ -667,11 +673,13 @@
     (if m m (raise-syntax-error #f "not a metafunction" stx name))))
 
 (define (assert-nat name x)
-  (unless (and (integer? x) (>= x 0))
-    (raise-type-error name "natural number" x)))
+  (if (and (integer? x) (>= x 0))
+      x
+      (raise-type-error name "natural number" x)))
 (define (assert-rel name x)
-  (unless (reduction-relation? x)
-    (raise-type-error 'redex-check "reduction-relation" x)))
+  (if (reduction-relation? x)
+      x
+      (raise-type-error 'redex-check "reduction-relation" x)))
 
 (define (defer-all pat size in-hole acc env att recur defer) 
   (defer acc))
@@ -742,8 +750,8 @@
                                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
                                               property)))])
            (quasisyntax/loc stx
-             (let ([att #,attempts-stx]
-                   [ret #,retries-stx]
+             (let ([att (assert-nat 'redex-check #,attempts-stx)]
+                   [ret (assert-nat 'redex-check #,retries-stx)]
                    [custom (contract 
                             (-> any/c natural-number/c any/c any/c hash? natural-number/c
                                 (->* (any/c)
@@ -755,32 +763,21 @@
                                 (-> any/c (values any/c hash?))
                                 (values any/c hash?))
                             #,custom-stx '+ '-)])
-               (assert-nat 'redex-check att)
-               (assert-nat 'redex-check ret)
                (unsyntax
                 (if source-stx
-                    #`(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])
-                                         (assert-rel 'redex-check r)
-                                         (values
-                                          (map (λ (x) ((rewrite-proc-lhs x) lang)) (reduction-relation-make-procs r))
-                                          (reduction-relation-srcs r)
-                                          (reduction-relation-lang r)))])])
-                        (check-prop-srcs
+                    #`(let-values ([(metafunc/red-rel num-cases) 
+                                    #,(cond [(and (identifier? source-stx) (metafunc source-stx))
+                                             => (λ (x) #`(values #,x (length (metafunc-proc-lhs-pats #,x))))]
+                                            [else
+                                             #`(let ([r (assert-rel 'redex-check #,source-stx)])
+                                                 (values r (length (reduction-relation-make-procs r))))])])
+                        (check-lhs-pats
                          lang
-                         pats
-                         srcs
+                         metafunc/red-rel
                          property
                          random-decisions@
                          custom
-                         (max 1 (floor (/ att (length pats))))
+                         (max 1 (floor (/ att num-cases)))
                          ret
                          'redex-check
                          show
@@ -845,8 +842,7 @@
         (let ([lang (metafunc-proc-lang m)]
               [dom (metafunc-proc-dom-pat m)]
               [decisions@ (generation-decisions)]
-              [att attempts])
-          (assert-nat 'check-metafunction-contract att)
+              [att (assert-nat 'check-metafunction-contract attempts)])
           (check-prop 
            ((generate lang decisions@ custom retries 'check-metafunction-contract)
             (if dom dom '(any (... ...))))
@@ -856,26 +852,33 @@
            att
            show))))]))
 
-(define (check-prop-srcs lang pats srcs prop decisions@ custom attempts retries what show
+(define (check-lhs-pats lang mf/rr prop decisions@ custom attempts retries what show
                          [match #f]
                          [match-fail #f])
   (let ([lang-gen (generate lang decisions@ custom retries what)])
-    (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))
-              (compose (curry format "clause #~s") add1)))
+    (let-values ([(pats srcs)
+                  (cond [(metafunc-proc? mf/rr)
+                         (values (metafunc-proc-lhs-pats mf/rr)
+                                 (metafunction-srcs mf/rr))]
+                        [(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
+                 show
+                 #:source src
+                 #:match match
+                 #:match-fail match-fail)))
+        (show
+         (format "no counterexamples in ~a (with each clause)\n"
+                 (format-attempts attempts)))))))
 
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()
@@ -889,13 +892,11 @@
                                    stx)]
                    [show (show-message stx)])
        (syntax/loc stx
-         (let ([att attempts]
-               [ret retries])
-           (assert-nat 'check-metafunction att)
-           (check-prop-srcs 
+         (let ([att (assert-nat 'check-metafunction attempts)]
+               [ret (assert-nat 'check-metafunction retries)])
+           (check-lhs-pats 
             (metafunc-proc-lang m)
-            (metafunc-proc-lhs-pats m)
-            (metafunc-srcs m)
+            m
             (λ (term _) (property term))
             (generation-decisions)
             custom
@@ -905,9 +906,14 @@
             show))))]))
 
 (define (reduction-relation-srcs r)
-  (map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
+  (map (λ (proc) (or (rewrite-proc-name proc)
+                     (format "clause at ~a" (rewrite-proc-lhs-src proc))))
        (reduction-relation-make-procs r)))
 
+(define (metafunction-srcs m)
+  (map (curry format "clause at ~a")
+       (metafunc-proc-src-locs m)))
+
 (define-syntax (check-reduction-relation stx)
   (syntax-case stx ()
     [(_ relation property . kw-args)
@@ -921,15 +927,11 @@
                    [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
+               [ret (assert-nat 'check-reduction-relation retries)]
+               [rel (assert-rel 'check-reduction-relation relation)])
+           (check-lhs-pats
             (reduction-relation-lang rel)
-            (map (λ (x) ((rewrite-proc-lhs x) (reduction-relation-lang rel)))
-                 (reduction-relation-make-procs rel))
-            (reduction-relation-srcs rel)
+            rel
             (λ (term _) (property term))
             decisions@
             custom
@@ -969,7 +971,8 @@
          generate-term
          check-metafunction-contract
          check-reduction-relation
-         check-metafunction)
+         check-metafunction
+         exn:fail:redex:generation-failure?)
 
 (provide (struct-out ellipsis) 
          (struct-out mismatch)
diff --git a/collects/redex/private/struct.ss b/collects/redex/private/struct.ss
index 0c69d780da..e34f211223 100644
--- a/collects/redex/private/struct.ss
+++ b/collects/redex/private/struct.ss
@@ -11,7 +11,8 @@
          build-reduction-relation
          reduction-relation?
          empty-reduction-relation
-         make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs rewrite-proc-id
+         make-rewrite-proc rewrite-proc? rewrite-proc-name 
+         rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id
          (struct-out rule-pict))
 
 (define-struct rule-pict (arrow lhs rhs label side-conditions/pattern-binds fresh-vars))
@@ -24,15 +25,16 @@
 
 (define-values (make-rewrite-proc 
                 rewrite-proc? 
-                rewrite-proc-name rewrite-proc-lhs rewrite-proc-id)
+                rewrite-proc-name rewrite-proc-lhs rewrite-proc-lhs-src rewrite-proc-id)
   (let ()
     (define-values (type constructor predicate accessor mutator) 
-      (make-struct-type 'rewrite-proc #f 4 0 #f '() #f 0))
+      (make-struct-type 'rewrite-proc #f 5 0 #f '() #f 0))
     (values constructor 
             predicate 
             (make-struct-field-accessor accessor 1 'name)
             (make-struct-field-accessor accessor 2 'lhs)
-            (make-struct-field-accessor accessor 3 'id))))
+            (make-struct-field-accessor accessor 3 'lhs-src)
+            (make-struct-field-accessor accessor 4 'id))))
 
 ;; lang : compiled-language
 ;; make-procs = (listof (compiled-lang -> proc))
@@ -78,6 +80,7 @@
                                 ress))))
                         (rewrite-proc-name make-proc)
                         (rewrite-proc-lhs make-proc)
+                        (rewrite-proc-lhs-src make-proc)
                         (rewrite-proc-id make-proc))
                        (loop (cdr make-procs)
                              (+ i 1))))]))])
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index dbbed4658e..6845b3ada9 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -1606,7 +1606,7 @@
     
     ; test shortcut in terms of shortcut
     (test (match ((rewrite-proc-lhs (third (reduction-relation-make-procs r))) grammar)
-            [`(((side-condition 5 ,(? procedure?)) 2) 1) #t]
+            [`(((side-condition 5 ,(? procedure?) ,_) 2) 1) #t]
             [else #f])
           #t))
   
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index e34be6840f..1552ef4333 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -1129,7 +1129,8 @@ sub-term---regenerating the sub-term if necessary. The optional keyword
 argument @scheme[retries-expr] (default @scheme[100]) bounds the number of times that 
 @scheme[generate-term] retries the generation of any sub-term. If 
 @scheme[generate-term] is unable to produce a satisfying term after 
-@scheme[retries-expr] attempts, it raises an error}
+@scheme[retries-expr] attempts, it raises an exception recognized by
+@scheme[exn:fail:redex:generation-failure?].}
 
 @defform/subs[(redex-check language @#,ttpattern property-expr kw-arg ...)
               ([kw-arg (code:line #:attempts attempts-expr)
@@ -1222,6 +1223,12 @@ when @scheme[relation] is a relation on @scheme[L] with @scheme[n] rules.}
                            [retries-expr natural-number/c])]{
 Like @scheme[check-reduction-relation] but for metafunctions.}
 
+@defproc[(exn:fail:redex:generation-failure? [v any/c]) boolean?]{
+  Recognizes the exceptions raised by @scheme[generate-term], 
+  @scheme[redex-check], etc. when those forms are unable to produce
+  a term matching some pattern.
+}
+                                                            
 @deftech{Debugging PLT Redex Programs}
 
 It is easy to write grammars and reduction rules that are
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index f5de7804db..3f65be6ad0 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -47,7 +47,8 @@
          generate-term
          check-metafunction
          check-metafunction-contract
-         check-reduction-relation)
+         check-reduction-relation
+         exn:fail:redex:generation-failure?)
 
 (provide/contract
  [current-traced-metafunctions (parameter/c (or/c 'all (listof symbol?)))]