diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index b556163db9..a46e922206 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -155,6 +155,12 @@
           (define next-any-decision (decision any))
           (define next-sequence-decision (decision seq)))))
 
+(define-syntax generate-term/decisions
+  (syntax-rules ()
+    [(_ lang pat size attempt decisions)
+     (parameterize ([generation-decisions decisions])
+       (generate-term lang pat size #:attempt attempt))]))
+
 (let ()
   (define-language lc
     (e (e e) x (λ (x) e))
@@ -162,7 +168,7 @@
   
   ;; Generate (λ (x) x)
   (test 
-   (generate-term 
+   (generate-term/decisions 
     lc e 1 0
     (decisions #:var (list (λ _ 'x) (λ _'x))
                #:nt (patterns third first first first)))
@@ -170,14 +176,14 @@
   
   ;; Generate pattern that's not a non-terminal
   (test 
-   (generate-term 
+   (generate-term/decisions 
     lc (x x x_1 x_1) 1 0
     (decisions #:var (list (λ _ 'x) (λ _ 'y)))) 
    '(x x y y))
   
   ; After choosing (e e), size decremented forces each e to x.
   (test
-   (generate-term 
+   (generate-term/decisions 
     lc e 1 0
     (decisions #:nt (patterns first)
                #:var (list (λ _ 'x) (λ _ 'y))))
@@ -193,7 +199,9 @@
   (let* ([x null]
          [prepend! (λ (c l b a) (begin (set! x (cons (car b) x)) 'x))])
     (test (begin
-            (generate-term lang a 5 0 (decisions #:var (list (λ _ 'x) prepend! prepend!)))
+            (generate-term/decisions
+             lang a 5 0
+             (decisions #:var (list (λ _ 'x) prepend! prepend!)))
             x)
           '(x x))))
 
@@ -204,7 +212,7 @@
     (x (variable-except λ)))
   (test 
    (exn:fail-message 
-     (generate-term 
+     (generate-term/decisions 
       postfix e 2 0
       (decisions #:var (list (λ _ 'x) (λ _ 'y))
                  #:nt (patterns third second first first))))
@@ -215,7 +223,7 @@
   (define-language var
     (e (variable-except x y)))
   (test
-   (generate-term
+   (generate-term/decisions
     var e 2 0
     (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x) (λ _ 'z))))
    'z))
@@ -232,26 +240,28 @@
     (n number)
     (z 4))
   (test
-   (generate-term 
+   (generate-term/decisions 
     lang a 2 0
     (decisions #:num (build-list 3 (λ (n) (λ (_) n)))
                #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 1))))
    `(0 1 2 "foo" "foo" "foo" "bar" #t))
-  (test (generate-term lang b 5 0 (decisions #:seq (list (λ (_) 0))))
+  (test (generate-term/decisions lang b 5 0 (decisions #:seq (list (λ (_) 0))))
         null)
-  (test (generate-term lang c 5 0 (decisions #:seq (list (λ (_) 0))))
+  (test (generate-term/decisions lang c 5 0 (decisions #:seq (list (λ (_) 0))))
         null)
-  (test (generate-term lang d 5 0 (decisions #:seq (list (λ (_) 2))))
+  (test (generate-term/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
         '(4 4 4 4 (4 4) (4 4)))
   (test (exn:fail-message (generate-term lang e 5)) 
         #rx"generate: unable to generate pattern e")
-  (test (generate-term lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
-  (test (generate-term lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
-                  (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 4)
-                                         (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 1) (λ (_) 3))))
+  (test (generate-term/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
+  (test (generate-term/decisions 
+         lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
+         (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 4)
+                                (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 1) (λ (_) 3))))
         '((0 0 0) (0 0 0 0) (1 1 1)))
-  (test (generate-term lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
-                  (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 5))))
+  (test (generate-term/decisions 
+         lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
+         (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 5))))
         '((0 0 0) (0 0 0 0) (1 1 1) (1 1 1 1 1))))
 
 (let ()
@@ -264,7 +274,7 @@
   ;; x and y bound in body
   (test 
    (let/ec k 
-     (generate-term 
+     (generate-term/decisions 
       lc e 10 0
       (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ (c l b a) (k b)))
                  #:nt (patterns first first first third first)
@@ -274,7 +284,7 @@
 (let ()
   (define-language lang (e (variable-prefix pf)))
   (test 
-   (generate-term
+   (generate-term/decisions
     lang e 5 0
     (decisions #:var (list (λ _ 'x))))
    'pfx))
@@ -288,7 +298,7 @@
   (define-language lang
     (e number (e_1 e_2 e e_1 e_2)))
   (test
-   (generate-term
+   (generate-term/decisions
     lang e 5 0
     (decisions #:nt (patterns second first first first)
                #:num (list (λ _ 2) (λ _ 3) (λ _ 4))))
@@ -300,7 +310,7 @@
     (x variable))
   (test
    (let/ec k
-     (generate-term
+     (generate-term/decisions
       lang e 5 0
       (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
    '(x)))
@@ -311,12 +321,12 @@
     (b (c_!_1 c_!_1 c_!_1))
     (c 1 2))
   (test
-   (generate-term
+   (generate-term/decisions
     lang a 5 0
     (decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
    '(1 1 2))
   (test
-   (generate-term
+   (generate-term/decisions
     lang (number_!_1 number_!_2 number_!_1) 5 0
     (decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
    '(1 1 2))
@@ -330,7 +340,7 @@
     (f foo bar))
   (test
    (let/ec k 
-     (generate-term 
+     (generate-term/decisions 
       lang e 5 0 
       (decisions #:str (list (λ (c l a) (k (cons (sort c char<=?) (sort l string<=?))))))))
    (cons '(#\a #\b #\f #\o #\r)
@@ -350,24 +360,26 @@
         #rx"unable to generate")
   (test ; binding works for with side-conditions failure/retry
    (let/ec k
-     (generate-term
+     (generate-term/decisions
       lang d 5 0
       (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'y) (λ (c l b a) (k b))))))
    '(y))
   (test ; mismatch patterns work with side-condition failure/retry
-   (generate-term
+   (generate-term/decisions
     lang e 5 0
     (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'y) (λ _ 'y) (λ _ 'x) (λ _ 'y))))
    '(y x y))
   (test ; generate compiles side-conditions in pattern
-   (generate-term lang (side-condition x_1 (not (eq? (term x_1) 'x))) 5 0
-             (decisions #:var (list (λ _ 'x) (λ _ 'y))))
+   (generate-term/decisions 
+    lang (side-condition x_1 (not (eq? (term x_1) 'x))) 5 0
+    (decisions #:var (list (λ _ 'x) (λ _ 'y))))
    'y)
   (test ; bindings within ellipses collected properly
    (let/ec k
-     (generate-term lang (side-condition (((number_1 3) ...) ...) (k (term ((number_1 ...) ...)))) 5 0
-               (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4))
-                          #:num (build-list 7 (λ (n) (λ (_) n))))))
+     (generate-term/decisions 
+      lang (side-condition (((number_1 3) ...) ...) (k (term ((number_1 ...) ...)))) 5 0
+      (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4))
+                 #:num (build-list 7 (λ (n) (λ (_) n))))))
    '((0 1 2) (3 4 5 6))))
 
 (let ()
@@ -397,7 +409,7 @@
     (y variable))
   
   (test 
-   (generate-term 
+   (generate-term/decisions 
     lang (in-hole A number ) 5 0
     (decisions 
      #:nt (patterns second second first first third first second first first)
@@ -406,19 +418,22 @@
   
   (test (generate-term lang (in-hole (in-hole (1 hole) hole) 5) 5) '(1 5))
   (test (generate-term lang (hole 4) 5) (term (hole 4)))
-  (test (generate-term lang (variable_1 (in-hole C variable_1)) 5 0
-                  (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x))))
+  (test (generate-term/decisions 
+         lang (variable_1 (in-hole C variable_1)) 5 0
+         (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x))))
         '(x x))
-  (test (generate-term lang (variable_!_1 (in-hole C variable_!_1)) 5 0
-                  (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'x) (λ _ 'y))))
+  (test (generate-term/decisions 
+         lang (variable_!_1 (in-hole C variable_!_1)) 5 0
+         (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'x) (λ _ 'y))))
         '(x y))
-  (test (let/ec k (generate-term lang d 5 0 (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
+  (test (let/ec k 
+          (generate-term/decisions lang d 5 0 (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
         '(x))
-  (test (generate-term lang e 5 0 (decisions #:num (list (λ _ 1) (λ _ 2))))
+  (test (generate-term/decisions lang e 5 0 (decisions #:num (list (λ _ 1) (λ _ 2))))
         '((2 (1 1)) 1))
-  (test (generate-term lang g 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 1) (λ _ 0))))
+  (test (generate-term/decisions lang g 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 1) (λ _ 0))))
         '(1 0))
-  (test (generate-term lang h 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 3))))
+  (test (generate-term/decisions lang h 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 3))))
         '((2 ((3 (2 1)) 3)) 1)))
 
 (let ()
@@ -426,7 +441,7 @@
       (e (e e) (+ e e) x v)
       (v (λ (x) e) number)
       (x variable-not-otherwise-mentioned))
-  (test (generate-term lc x 5 0 (decisions #:var (list (λ _ 'λ) (λ _ '+) (λ _ 'x))))
+  (test (generate-term/decisions lc x 5 0 (decisions #:var (list (λ _ 'λ) (λ _ '+) (λ _ 'x))))
         'x))
 
 (let ()
@@ -436,19 +451,24 @@
   (define-language empty)
   
   ;; `any' pattern
-  (test (call-with-values (λ () (pick-any four (make-random 0 1))) list)
-        (list four 'f))
-  (test (call-with-values (λ () (pick-any four (make-random 1))) list)
-        (list sexp 'sexp))
-  (test (generate-term four any 5 0 (decisions #:any (list (λ _ (values four 'e))))) 4)
-  (test (generate-term four any 5 0 
-                  (decisions #:any (list (λ _ (values sexp 'sexp)))
-                             #:nt (patterns fifth second second second)
-                             #:seq (list (λ _ 3))
-                             #:str (list (λ _ "foo") (λ _ "bar") (λ _ "baz"))))
+  (let ([four (prepare-lang four)]
+        [sexp (prepare-lang sexp)])
+    (test (call-with-values (λ () (pick-any four sexp (make-random 0 1))) list)
+          (list four 'f))
+    (test (call-with-values (λ () (pick-any four sexp (make-random 1))) list)
+          (list sexp 'sexp)))
+  (test (generate-term/decisions 
+         four any 5 0 (decisions #:any (list (λ (lang sexp) (values lang 'e))))) 4)
+  (test (generate-term/decisions
+         four any 5 0 
+         (decisions #:any (list (λ (lang sexp) (values sexp 'sexp)))
+                    #:nt (patterns fifth second second second)
+                    #:seq (list (λ _ 3))
+                    #:str (list (λ _ "foo") (λ _ "bar") (λ _ "baz"))))
         '("foo" "bar" "baz"))
-  (test (generate-term empty any 5 0 (decisions #:nt (patterns first)
-                                                     #:var (list (λ _ 'x))))
+  (test (generate-term/decisions
+         empty any 5 0 (decisions #:nt (patterns first)
+                                  #:var (list (λ _ 'x))))
         'x))
 
 ;; `hide-hole' pattern
@@ -469,15 +489,16 @@
     (e x (e e) v)
     (v (λ (x) e))
     (x variable-not-otherwise-mentioned))
-  (test (generate-term lang (cross e) 3 0 
-                  (decisions #:nt (patterns fourth first first second first first first)
-                             #:var (list (λ _ 'x) (λ _ 'y))))
+  (test (generate-term/decisions
+         lang (cross e) 3 0 
+         (decisions #:nt (patterns fourth first first second first first first)
+                    #:var (list (λ _ 'x) (λ _ 'y))))
         (term (λ (x) (hole y)))))
 
-;; current-error-port-output : (-> (-> any) string)
-(define (current-error-port-output thunk)
+;; current-output : (-> (-> any) string)
+(define (current-output thunk)
   (let ([p (open-output-string)])
-    (parameterize ([current-error-port p])
+    (parameterize ([current-output-port p])
       (thunk))
     (begin0
       (get-output-string p)
@@ -487,16 +508,78 @@
 (let ()
   (define-language lang
     (d 5)
-    (e e 4))
-  (test (current-error-port-output (λ () (check lang d 2 #f))) 
-        "failed after 1 attempts:\n5\n")
+    (e e 4)
+    (n number))
+  (test (current-output (λ () (check lang d #f))) 
+        "counterexample found after 1 attempts:\n5\n")
   (test (check lang d #t) #t)
-  (test (check lang (d e) 2 (and (eq? (term d) 5) (eq? (term e) 4))) #t)
-  (test (check lang (d ...) 2 (zero? (modulo (foldl + 0 (term (d ...))) 5))) #t)
-  (test (current-error-port-output (λ () (check lang (d e) 2 #f)))
-        "failed after 1 attempts:\n(5 4)\n")
-  (test (current-error-port-output (λ () (check lang d 2 (error 'pred-raised))))
-        "failed after 1 attempts:\n5\n"))
+  (test (check lang (d e) (and (eq? (term d) 5) (eq? (term e) 4)) #:attempts 2) #t)
+  (test (check lang (d ...) (zero? (modulo (foldl + 0 (term (d ...))) 5)) #:attempts 2) #t)
+  (test (current-output (λ () (check lang (d e) #f)))
+        "counterexample found after 1 attempts:\n(5 4)\n")
+  (test (current-output (λ () (check lang d (error 'pred-raised))))
+        "counterexample found after 1 attempts:\n5\n")
+  (test (parameterize ([check-randomness (make-random 0 0)])
+          (check lang n (eq? 42 (term n)) 
+                 #:attempts 1
+                 #:source (reduction-relation lang (--> 42 x))))
+        #t)
+  (test (current-output
+         (λ ()
+           (parameterize ([check-randomness (make-random 0 0)])
+             (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
+         (λ ()
+           (parameterize ([check-randomness (make-random 1)])
+             (check lang d (eq? 42 (term n)) 
+                    #:attempts 1
+                    #:source (reduction-relation lang (--> 0 x z))))))
+        "counterexample found after 1 attempts:\n5\n")
+  (test (let ([r (reduction-relation lang (--> 0 x z))])
+          (check lang n (number? (term n)) 
+                 #:attempts 10
+                 #:source r))
+        #t)
+  (let ()
+    (define-metafunction lang
+      [(mf 0) 0]
+      [(mf 42) 0])
+    (test (parameterize ([check-randomness (make-random 0 1)])
+            (check lang (n) (eq? 42 (term n)) 
+                   #:attempts 1
+                   #:source mf))
+          #t))
+  (let ()
+    (define-language L)
+    (test (with-handlers ([exn:fail? exn-message])
+            (check lang any #t #:source (reduction-relation L (--> 1 1))))
+          #rx"language for secondary source"))
+  (let ()
+    (test (with-handlers ([exn:fail? exn-message])
+            (check lang n #t #:source (reduction-relation lang (--> x 1))))
+          #rx"x does not match n"))
+  
+  (let ([stx-err (λ (stx)
+                   (with-handlers ([exn:fail:syntax? exn-message])
+                     (expand stx)
+                     'no-syntax-error))])
+    (parameterize ([current-namespace (make-base-namespace)])
+      (eval '(require "../reduction-semantics.ss"
+                      "rg.ss"))
+      (eval '(define-language empty))
+      (test (stx-err '(check empty any #t #:typo 3))
+            #rx"check: bad keyword syntax")
+      (test (stx-err '(check empty any #t #:attempts 3 #:attempts 4))
+            #rx"bad keyword syntax")
+      (test (stx-err '(check empty any #t #:attempts))
+            #rx"bad keyword syntax")
+      (test (stx-err '(check empty any #t #:attempts 3 4))
+            #rx"bad keyword syntax")
+      (test (stx-err '(check empty any #t #:source #:attempts))
+            #rx"bad keyword syntax"))))
 
 ;; check-metafunction-contract
 (let ()
@@ -518,22 +601,31 @@
     [(i any ...) (any ...)])
   
   ;; Dom(f) < Ctc(f)
-  (test (current-error-port-output 
-         (λ () (check-metafunction-contract f (decisions #:num (list (λ _ 2) (λ _ 5))))))
-        "failed after 1 attempts:\n(5)\n")
+  (test (current-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-error-port-output
-         (λ () (check-metafunction-contract f (decisions #:num (list (λ _ 3))))))
-        "failed after 1 attempts:\n(3)\n")
+  (test (current-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-error-port-output
-         (λ () (check-metafunction-contract g (decisions #:num (list (λ _ 1) (λ _ 1))
-                                                         #:seq (list (λ _ 2))))))
-        "failed after 1 attempts:\n(1 1)\n")
+  (test (current-output
+         (λ () 
+           (parameterize ([generation-decisions
+                           (decisions #:num (list (λ _ 1) (λ _ 1))
+                                      #:seq (list (λ _ 2)))])
+             (check-metafunction-contract g))))
+        "counterexample found after 1 attempts:\n(1 1)\n")
   ;; OK -- generated from Dom(h)
   (test (check-metafunction-contract h) #t)
   ;; OK -- generated from pattern (any ...)
-  (test (check-metafunction-contract i) #t))
+  (test (check-metafunction-contract i #:attempts 5) #t))
 
 ;; check-reduction-relation
 (let ()
@@ -562,12 +654,12 @@
   
   (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
     (test (check-reduction-relation S (λ (x) #t) #:attempts 1) #t)
-    (test (current-error-port-output 
+    (test (current-output 
            (λ () (check-reduction-relation S (λ (x) #f))))
-          "checking name failed after 1 attempts:\n1\n")
-    (test (current-error-port-output 
+          "counterexample found after 1 attempts with name:\n1\n")
+    (test (current-output 
            (λ () (check-reduction-relation S (curry eq? 1))))
-          "checking unnamed failed after 1 attempts:\n3\n"))
+          "counterexample found after 1 attempts with unnamed:\n3\n"))
   
   (let ([T (reduction-relation
             L
@@ -593,11 +685,14 @@
     [(m 2) whatever])
   (let ([generated null])
     (test (begin
-            (check-metafunction m (λ (t) (set! generated (cons t generated))) 1)
+            (check-metafunction m (λ (t) (set! generated (cons t generated))) #:attempts 1)
             generated) 
           (reverse '((1) (2)))))
-  (test (current-error-port-output (λ () (check-metafunction m (curry eq? 1))))
-        #rx"checking clause #1 failed after 1 attempt"))
+  (test (current-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))
+        #rx"check-metafunction: expected"))
 
 ;; parse/unparse-pattern
 (let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 834700ce45..6174f0ac82 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -76,10 +76,12 @@ To do a better job of not generating programs with free variables,
       (pick-from-list lang-lits random)
       (list->string (build-list length (λ (_) (pick-char attempt lang-chars random))))))
 
-(define (pick-any lang [random random]) 
-  (if (and (not (null? (compiled-lang-lang lang))) (zero? (random 5)))
-      (values lang (pick-from-list (map nt-name (compiled-lang-lang lang)) random))
-      (values sexp (nt-name (car (compiled-lang-lang sexp))))))
+(define (pick-any lang sexp [random random]) 
+  (let ([c-lang (rg-lang-clang lang)]
+        [c-sexp (rg-lang-clang sexp)])
+    (if (and (not (null? (compiled-lang-lang c-lang))) (zero? (random 5)))
+        (values lang (pick-from-list (map nt-name (compiled-lang-lang c-lang)) random))
+        (values sexp (nt-name (car (compiled-lang-lang c-sexp)))))))
 
 (define (pick-string lang-chars lang-lits attempt [random random])
   (random-string lang-chars lang-lits (random-natural 1/5 random) attempt random))
@@ -153,21 +155,24 @@ To do a better job of not generating programs with free variables,
 (define (pick-sequence-length attempt)
   (random-natural (expected-value->p (attempt->size attempt))))
 
+(define (zip . lists)
+  (apply (curry map list) lists))
+
 (define (min-prods nt base-table)
   (let* ([sizes (hash-ref base-table (nt-name nt))]
-         [min-size (apply min/f sizes)]
-         [zip (λ (l m) (map cons l m))])
-    (map cdr (filter (λ (x) (equal? min-size (car x))) (zip sizes (nt-rhs nt))))))
+         [min-size (apply min/f sizes)])
+    (map cadr (filter (λ (x) (equal? min-size (car x))) (zip sizes (nt-rhs nt))))))
+
+(define-struct rg-lang (clang lits chars base-table))
+(define (prepare-lang lang)
+  (let ([lits (map symbol->string (compiled-lang-literals lang))])
+    (make-rg-lang (parse-language lang) lits (unique-chars lits) (find-base-cases lang))))
 
 (define (generate lang decisions@)
   (define-values/invoke-unit decisions@
     (import) (export decisions^))
   
-  (define lang-lits (map symbol->string (compiled-lang-literals lang)))
-  (define lang-chars (unique-chars lang-lits))
-  (define base-table (find-base-cases lang))
-  
-  (define (generate-nt name fvt-id bound-vars size attempt in-hole state)
+  (define ((generate-nt lang generate base-table) name fvt-id bound-vars size attempt in-hole state)
     (let*-values
         ([(bound-vars) (append (extract-bound-vars fvt-id state) bound-vars)]
          [(term _)
@@ -178,8 +183,9 @@ To do a better job of not generating programs with free variables,
                          (if (zero? size)
                              (min-prods (nt-by-name lang name) base-table)
                              ((next-non-terminal-decision) name lang bound-vars attempt)))])
-               (((generate-pat bound-vars (max 0 (sub1 size)) attempt) (rhs-pattern rhs) in-hole)
-                (make-state (map fvt-entry (rhs-var-info rhs)) #hash()))))
+               (generate bound-vars (max 0 (sub1 size)) attempt 
+                         (make-state (map fvt-entry (rhs-var-info rhs)) #hash())
+                         in-hole (rhs-pattern rhs))))
            (λ (_ env) (mismatches-satisfied? env)))])
       (values term (extend-found-vars fvt-id term state))))
   
@@ -202,8 +208,7 @@ To do a better job of not generating programs with free variables,
             (if (null? envs)
                 (values null null fvt)
                 (let*-values 
-                    ([(term state) ((generate (ellipsis-pattern ellipsis) the-hole) 
-                                    (make-state fvt (car envs)))]
+                    ([(term state) (generate (make-state fvt (car envs)) the-hole (ellipsis-pattern ellipsis))]
                      [(terms envs fvt) (recur (state-fvt state) (cdr envs))])
                   (values (cons term terms) (cons (state-env state) envs) fvt))))])
       (values seq (make-state fvt (merge-environments envs)))))
@@ -241,6 +246,7 @@ To do a better job of not generating programs with free variables,
                    (hash-set! prior val #t)))))))
   
   (define-struct state (fvt env))
+  (define new-state (make-state null #hash()))
   (define (set-env state name value)
     (make-state (state-fvt state) (hash-set (state-env state) name value)))
   
@@ -255,9 +261,12 @@ To do a better job of not generating programs with free variables,
   (define (fvt-entry binds)
     (make-found-vars (binds-binds binds) (binds-source binds) '() #f))
   
-  (define (((generate-pat bound-vars size attempt) pat in-hole) state)
-    (define recur (generate-pat bound-vars size attempt))
-    (define (recur/pat pat) ((recur pat in-hole) state))
+  (define (generate-pat lang sexp bound-vars size attempt state in-hole pat)
+    (define recur (curry generate-pat lang sexp bound-vars size attempt))
+    (define recur/pat (recur state in-hole))
+    
+    (define clang (rg-lang-clang lang))
+    (define gen-nt (generate-nt clang (curry generate-pat lang sexp) (rg-lang-base-table lang)))
     
     (match pat
       [`number (values ((next-number-decision) attempt) state)]
@@ -265,17 +274,22 @@ To do a better job of not generating programs with free variables,
        (generate/pred 'variable
                       (λ () (recur/pat 'variable))
                       (λ (var _) (not (memq var vars))))]
-      [`variable (values ((next-variable-decision) lang-chars lang-lits bound-vars attempt) state)]
+      [`variable 
+       (values ((next-variable-decision)
+                (rg-lang-chars lang) (rg-lang-lits lang) bound-vars attempt)
+               state)]
       [`variable-not-otherwise-mentioned
        (generate/pred 'variable
                       (λ () (recur/pat 'variable)) 
-                      (λ (var _) (not (memq var (compiled-lang-literals lang)))))]
+                      (λ (var _) (not (memq var (compiled-lang-literals clang)))))]
       [`(variable-prefix ,prefix) 
        (define (symbol-append prefix suffix)
          (string->symbol (string-append (symbol->string prefix) (symbol->string suffix))))
        (let-values ([(term state) (recur/pat 'variable)])
          (values (symbol-append prefix term) state))]
-      [`string (values ((next-string-decision) lang-chars lang-lits attempt) state)]
+      [`string 
+       (values ((next-string-decision) (rg-lang-chars lang) (rg-lang-lits lang) attempt)
+               state)]
       [`(side-condition ,pat ,(? procedure? condition))
        (generate/pred (unparse-pattern pat) 
                       (λ () (recur/pat pat))
@@ -286,38 +300,38 @@ To do a better job of not generating programs with free variables,
       [`hole (values in-hole state)]
       [`(in-hole ,context ,contractum)
        (let-values ([(term state) (recur/pat contractum)])
-         ((recur context term) state))]
-      [`(hide-hole ,pattern) ((recur pattern the-hole) state)]
+         (recur state term context))]
+      [`(hide-hole ,pattern) (recur state the-hole pattern)]
       [`any
-       (let*-values ([(lang nt) ((next-any-decision) lang)]
-                     [(term _) (((generate lang decisions@) nt) size attempt)])
+       (let*-values ([(lang nt) ((next-any-decision) lang sexp)]
+                     [(term _) (generate-pat lang sexp null size attempt new-state the-hole nt)])
          (values term state))]
-      [(? (is-nt? lang))
-       (generate-nt pat pat bound-vars size attempt in-hole state)]
-      [(struct binder ((and name (or (? (is-nt? lang) nt) (app (symbol-match named-nt-rx) (? (is-nt? lang) nt))))))
-       (generate/prior pat state (λ () (generate-nt nt name bound-vars size attempt in-hole state)))]
+      [(? (is-nt? clang))
+       (gen-nt pat pat bound-vars size attempt in-hole state)]
+      [(struct binder ((and name (or (? (is-nt? clang) nt) (app (symbol-match named-nt-rx) (? (is-nt? clang) nt))))))
+       (generate/prior pat state (λ () (gen-nt nt name bound-vars size attempt in-hole state)))]
       [(struct binder ((or (? built-in? b) (app (symbol-match named-nt-rx) (? built-in? b)))))
        (generate/prior pat state (λ () (recur/pat b)))]
-      [(struct mismatch (name (app (symbol-match mismatch-nt-rx) (? symbol? (? (is-nt? lang) nt)))))
-       (let-values ([(term state) (generate-nt nt pat bound-vars size attempt in-hole state)])
+      [(struct mismatch (name (app (symbol-match mismatch-nt-rx) (? symbol? (? (is-nt? clang) nt)))))
+       (let-values ([(term state) (gen-nt nt pat bound-vars size attempt in-hole state)])
          (values term (set-env state pat term)))]
       [(struct mismatch (name (app (symbol-match mismatch-nt-rx) (? symbol? (? built-in? b)))))
        (let-values ([(term state) (recur/pat b)])
          (values term (set-env state pat term)))]
       [`(cross ,(? symbol? cross-nt))
-       (generate-nt cross-nt #f bound-vars size attempt in-hole state)]
+       (gen-nt cross-nt #f bound-vars size attempt in-hole state)]
       [(or (? symbol?) (? number?) (? string?) (? boolean?) (? null?)) (values pat state)]
       [(list-rest (and (struct ellipsis (name sub-pat class vars)) ellipsis) rest)
        (let*-values ([(length) (let ([prior (hash-ref (state-env state) class #f)])
                                  (if prior prior ((next-sequence-decision) attempt)))]
                      [(seq state) (generate-sequence ellipsis recur state length)]
-                     [(rest state) ((recur rest in-hole) 
-                                    (set-env (set-env state class length) name length))])
+                     [(rest state) (recur (set-env (set-env state class length) name length)
+                                     in-hole rest)])
          (values (append seq rest) state))]
       [(list-rest pat rest)
        (let*-values 
            ([(pat-term state) (recur/pat pat)]
-            [(rest-term state) ((recur rest in-hole) state)])
+            [(rest-term state) (recur state in-hole rest)])
          (values (cons pat-term rest-term) state))]
       [else
        (error 'generate "unknown pattern ~s\n" pat)]))
@@ -356,17 +370,19 @@ To do a better job of not generating programs with free variables,
       (state-fvt state))
      (state-env state)))
   
-  (λ (pat)
-    (let ([unparsed (unparse-pattern pat)])
-      (λ (size attempt)
-        (let-values ([(term state)
-                      (generate/pred 
-                       unparsed
-                       (λ () 
-                         (((generate-pat null size attempt) pat the-hole)
-                          (make-state null #hash())))
-                       (λ (_ env) (mismatches-satisfied? env)))])
-          (values term (bindings (state-env state))))))))
+  (let ([rg-lang (prepare-lang lang)]
+        [rg-sexp (prepare-lang sexp)])
+    (λ (pat)
+      (let ([parsed (reassign-classes (parse-pattern pat lang 'top-level))])
+        (λ (size attempt)
+          (let-values ([(term state)
+                        (generate/pred 
+                         pat
+                         (λ ()
+                           (generate-pat rg-lang rg-sexp null size attempt 
+                                         new-state the-hole parsed))
+                         (λ (_ env) (mismatches-satisfied? env)))])
+            (values term (bindings (state-env state)))))))))
 
 ;; find-base-cases : compiled-language -> hash-table
 (define (find-base-cases lang)
@@ -604,133 +620,198 @@ To do a better job of not generating programs with free variables,
         [_ pat]))))
 
 ;; used in generating the `any' pattern
-(define sexp
-  (let ()
-    (define-language sexp (sexp variable string number hole (sexp ...)))
-    (parse-language sexp)))
+(define-language sexp (sexp variable string number hole (sexp ...)))
+
+(define-for-syntax (metafunc name)
+  (let ([tf (syntax-local-value name (λ () #f))])
+    (and (term-fn? tf) (term-fn-get-id tf))))
+
+(define-for-syntax (metafunc/err name stx)
+  (let ([m (metafunc name)])
+    (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)))
+
+(define-for-syntax (term-generator lang pat decisions what)
+  (with-syntax ([pattern 
+                 (rewrite-side-conditions/check-errs 
+                  (language-id-nts lang what)
+                  what #t pat)]
+                [lang lang]
+                [decisions decisions])
+    (syntax ((generate lang (decisions lang)) `pattern))))
+
+(define-syntax (generate-term stx)
+  (syntax-case stx ()
+    [(_ lang pat size #:attempt attempt)
+     (with-syntax ([generate (term-generator #'lang #'pat #'(generation-decisions) 'generate-term)])
+       (syntax/loc stx
+         (let-values ([(term _) (generate size attempt)])
+           term)))]
+    [(_ lang pat size)
+     (syntax/loc stx (generate-term lang pat size #:attempt 1))]))
+
+(define check-randomness (make-parameter random))
 
 (define-syntax (check stx)
   (syntax-case stx ()
-    [(_ lang pat property)
-     (syntax/loc stx (check lang pat default-check-attempts property))]
-    [(_ lang pat attempts property)
+    [(_ lang pat property . kw-args)
      (let-values ([(names names/ellipses) 
-                   (extract-names (language-id-nts #'lang 'generate) 'check #t #'pat)])
+                   (extract-names (language-id-nts #'lang 'check) 'check #t #'pat)]
+                  [(attempts-stx source-stx)
+                   (let loop ([args (syntax kw-args)]
+                              [attempts #f]
+                              [source #f])
+                     (syntax-case args ()
+                       [() (values attempts source)]
+                       [(#:attempts a . rest)
+                        (not (or attempts (keyword? (syntax-e #'a))))
+                        (loop #'rest #'a source)]
+                       [(#:source s . rest)
+                        (not (or source (keyword? (syntax-e #'s))))
+                        (loop #'rest attempts #'s)]
+                       [else (raise-syntax-error #f "bad keyword syntax" stx args)]))])
        (with-syntax ([(name ...) names]
-                     [(name/ellipses ...) names/ellipses])
-         (syntax/loc stx
-           (or (check-property 
-                (term-generator lang pat random-decisions)
-                (λ (_ bindings)
-                  (with-handlers ([exn:fail? (λ (_) #f)])
+                     [(name/ellipses ...) names/ellipses]
+                     [attempts (or attempts-stx #'default-check-attempts)])
+         (quasisyntax/loc stx
+           (let ([att attempts])
+             (assert-nat 'check att)
+             (or (check-property 
+                  (cons (list #,(term-generator #'lang #'pat #'random-decisions '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 '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 '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 'check "~s does not match ~s" generated 'pat))
+                  (λ (_ bindings)
                     (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
-                              property)))
-                attempts)
-               (void)))))]))
+                              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 generate property attempts [source #f])
+(define (check-property gens-srcs match match-fail property attempts display [random random])
   (let loop ([remaining attempts])
     (if (zero? remaining)
         #t
         (let ([attempt (add1 (- attempts remaining))])
-          (let-values ([(term bindings) 
-                        (generate (attempt->size attempt) attempt)])
-            (if (property term bindings)
+          (let*-values ([(generator source)
+                         (apply values 
+                                (if (and (not (null? (cdr gens-srcs))) (zero? (random 10)))
+                                    (pick-from-list (cdr gens-srcs) random)
+                                    (car gens-srcs)))]
+                        [(term bindings) 
+                         (generator (attempt->size attempt) attempt)])
+            (if (andmap (λ (bindings) 
+                          (with-handlers ([exn:fail? (λ (_) #f)])
+                            (property term bindings)))
+                        (cond [(and match (match term)) 
+                               => (curry map (compose make-bindings match-bindings))]
+                              [match (match-fail term)]
+                              [else (list bindings)]))
                 (loop (sub1 remaining))
                 (begin
-                  (when source
-                    (fprintf (current-error-port) "checking ~a " source))
-                  (fprintf (current-error-port) "failed after ~s attempts:\n" attempt)
-                  (pretty-print term (current-error-port))
+                  (display term attempt source (current-output-port))
                   #f)))))))
 
-(define-syntax generate-term
-  (syntax-rules ()
-    [(_ lang pat size attempt decisions)
-     (let-values ([(term _) ((term-generator lang pat decisions) size attempt)])
-       term)]
-    [(_ lang pat size attempt)
-     (generate-term lang pat size attempt random-decisions)]
-    [(_ lang pat size)
-     (generate-term lang pat size 1)]))
-
-(define-syntax (term-generator stx)
-  (syntax-case stx ()
-    [(_ lang pat decisions)
-     (with-syntax ([pattern 
-                    (rewrite-side-conditions/check-errs 
-                     (language-id-nts #'lang 'generate)
-                     'generate #t #'pat)])
-       (syntax/loc stx 
-         (let ([lang (parse-language lang)])
-           ((generate lang (decisions lang))
-            (reassign-classes (parse-pattern `pattern lang 'top-level))))))]))
-
-(define-for-syntax (metafunc name stx)
-  (let ([tf (syntax-local-value name (λ () #f))])
-    (if (term-fn? tf)
-        (term-fn-get-id tf)
-        (raise-syntax-error #f "not a metafunction" stx name))))
-
 (define-syntax (check-metafunction-contract stx)
   (syntax-case stx ()
-    [(_ name) 
-     (syntax/loc stx (check-metafunction-contract name random-decisions))]
-    [(_ name decisions)
+    [(_ name)
+     (syntax/loc stx 
+       (check-metafunction-contract name #:attempts default-check-attempts))]
+    [(_ name #:attempts attempts)
      (identifier? #'name)
-     (with-syntax ([m (metafunc #'name stx)])
+     (with-syntax ([m (metafunc/err #'name stx)])
        (syntax/loc stx 
-        (let ([lang (parse-language (metafunc-proc-lang m))]
-              [dom (metafunc-proc-dom-pat m)])
+        (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 
-           ((generate lang (decisions lang))
-            (reassign-classes (parse-pattern (if dom dom '(any (... ...))) lang 'top-level)))
-           (λ (t _) 
-             (with-handlers ([exn:fail:redex? (λ (_) #f)])
-               (begin (term (name ,@t)) #t)))
-           default-check-attempts))))]))
+           (list (list ((generate lang (decisions lang)) (if dom dom '(any (... ...)))) #f))
+           #f
+           #f
+           (λ (t _) (begin (term (name ,@t)) #t))
+           att
+           (λ (term attempt _ port)
+             (fprintf port "counterexample found after ~a attempts:\n" attempt)
+             (pretty-print term port))))))]))
 
-(define (check-property-many lang patterns ids prop decisions attempts)
-  (let* ([lang-gen (generate lang (decisions lang))]
-         [pat-gens (map (λ (pat) (lang-gen (reassign-classes (parse-pattern pat lang 'top-level))))
-                        patterns)])
-    (for/and ([pat patterns]
-              [id ids])
+(define (check-property-many lang pats srcs prop decisions attempts)
+  (let ([lang-gen (generate lang (decisions lang))])
+    (for/and ([pat pats] [src srcs])
       (check-property
-       (let ([gen (lang-gen (reassign-classes (parse-pattern pat lang 'top-level)))])
-         (λ (size attempt) (gen size attempt)))
+       (let ([gen (lang-gen pat)])
+         (list (list (λ (size attempt) (gen size attempt)) src)))
+       #f
+       #f
        (λ (term _) (prop term))
        attempts
-       id))))
+       (λ (term attempt source port)
+         (fprintf port "counterexample found after ~a attempts with ~a:\n" 
+                  attempt source)
+         (pretty-print term port))))))
+
+(define (metafunc-srcs m)
+  (build-list (length (metafunc-proc-lhs-pats m))
+              (compose (curry format "clause #~s") add1)))
 
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()
     [(_ name property)
-     (syntax/loc stx (check-metafunction name property default-check-attempts))]
-    [(_ name property attempts)
-     (syntax/loc stx (check-metafunction name property random-decisions attempts))]
-    [(_ name property decisions attempts)
-     (with-syntax ([m (metafunc #'name stx)])
+     (syntax/loc stx (check-metafunction name property #:attempts default-check-attempts))]
+    [(_ name property #:attempts attempts)
+     (with-syntax ([m (metafunc/err #'name stx)])
        (syntax/loc stx
-         (or (check-property-many
-              (parse-language (metafunc-proc-lang m))
-              (metafunc-proc-lhs-pats m)
-              (build-list (length (metafunc-proc-lhs-pats m))
-                          (compose (curry format "clause #~s") add1))
-              property
-              decisions
-              attempts)
-             (void))))]))
+         (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)))))]))
+
+(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])
   (or (check-property-many
-       (parse-language (reduction-relation-lang relation))
+       (reduction-relation-lang relation)
        (map rewrite-proc-lhs (reduction-relation-make-procs relation))
-       (map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
-            (reduction-relation-make-procs relation))
+       (reduction-relation-srcs relation)
        property
        decisions
        attempts)
@@ -758,14 +839,17 @@ To do a better job of not generating programs with free variables,
         (define (next-any-decision) pick-any)
         (define (next-string-decision) pick-string)))
 
+(define generation-decisions (make-parameter random-decisions))
+
 (provide pick-from-list pick-var min-prods decisions^ pick-sequence-length
          is-nt? pick-char random-string pick-string check nt-by-name
          pick-nt unique-chars pick-any sexp generate-term parse-pattern
          class-reassignments reassign-classes unparse-pattern
          (struct-out ellipsis) (struct-out mismatch) (struct-out class)
-         (struct-out binder) check-metafunction-contract
+         (struct-out binder) check-metafunction-contract prepare-lang
          pick-number parse-language check-reduction-relation 
-         preferred-production-threshold check-metafunction)
+         preferred-production-threshold check-metafunction check-randomness
+         generation-decisions)
 
 (provide/contract
  [find-base-cases (-> compiled-lang? hash?)])
\ No newline at end of file