diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt
index 5f29731105..b2230a0397 100644
--- a/collects/redex/private/rg.rkt
+++ b/collects/redex/private/rg.rkt
@@ -104,8 +104,27 @@
 
 ; Determines a size measure for numbers, sequences, etc., using the
 ; attempt count.
-(define (attempt->size n)
-  (inexact->exact (floor (/ (log (add1 n)) (log 5)))))
+(define attempt->size
+  (make-parameter (λ (n) (inexact->exact (floor (/ (log (add1 n)) (log 5)))))))
+(define-for-syntax (with-attempt->size arg-stx redex-form body)
+  (if arg-stx
+      #`(parameterize ([attempt->size
+                        (contract (-> natural-number/c natural-number/c) #,arg-stx
+                                  #,(let ([m (syntax-source-module arg-stx)])
+                                      (cond [(module-path-index? m)
+                                             (format "~a" (module-path-index-resolve m))]
+                                            [(or (symbol? m) (path? m))
+                                             (format "~a" m)]
+                                            [else (format "~s client" redex-form)]))
+                                  '#,redex-form 
+                                  "#:attempt-size argument"
+                                  #(#,(syntax-source arg-stx)
+                                    #,(syntax-line arg-stx) 
+                                    #,(syntax-column arg-stx) 
+                                    #,(syntax-position arg-stx)
+                                    #,(syntax-span arg-stx)))])
+          #,body)
+      body))
 
 (define (pick-number attempt #:top-threshold [top-threshold complex-threshold] [random random])
   (let loop ([threshold 0] 
@@ -118,7 +137,7 @@
             (< attempt (caar levels))
             (< top-threshold (caar levels))
             (not (exotic-choice? random)))
-        (generator (expected-value->p (attempt->size (- attempt threshold))) random)
+        (generator (expected-value->p ((attempt->size) (- attempt threshold))) random)
         (loop (caar levels) (cdar levels) (cdr levels)))))
 
 (define (pick-natural attempt [random random])
@@ -131,7 +150,7 @@
   (pick-number attempt #:top-threshold real-threshold random))
 
 (define (pick-sequence-length attempt)
-  (random-natural (expected-value->p (attempt->size attempt))))
+  (random-natural (expected-value->p ((attempt->size) attempt))))
 
 (define (min-prods nt prods base-table)
   (let* ([sizes (hash-ref base-table nt)]
@@ -709,12 +728,13 @@
      (let-values ([(names names/ellipses) 
                    (extract-names (language-id-nts #'lang 'redex-check)
                                   'redex-check #t #'pat)]
-                  [(attempts-stx source-stx retries-stx print?-stx)
+                  [(attempts-stx source-stx retries-stx print?-stx size-stx)
                    (apply values
                           (parse-kw-args `((#:attempts . ,#'default-check-attempts)
                                            (#:source . #f)
                                            (#:retries . ,#'default-retries)
-                                           (#:print? . #t))
+                                           (#:print? . #t)
+                                           (#:attempt-size . #f))
                                          (syntax kw-args)
                                          stx))])
        (with-syntax ([(name ...) names]
@@ -728,27 +748,28 @@
              (let ([att (assert-nat 'redex-check #,attempts-stx)]
                    [ret (assert-nat 'redex-check #,retries-stx)]
                    [print? #,print?-stx])
-               (unsyntax
-                (if source-stx
-                    #`(let-values ([(metafunc/red-rel num-cases) 
-                                    #,(cond [(and (identifier? source-stx) (metafunc source-stx))
-                                             => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
-                                            [else
-                                             #`(let ([r (assert-rel 'redex-check #,source-stx)])
-                                                 (values r (length (reduction-relation-make-procs r))))])])
-                        (check-lhs-pats
-                         lang
-                         metafunc/red-rel
-                         property
-                         (max 1 (floor (/ att num-cases)))
-                         ret
-                         'redex-check
-                         (and print? show)
-                         (test-match lang pat)
-                         (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
-                    #`(check-prop
-                       #,(term-generator #'lang #'pat 'redex-check)
-                       property att ret (and print? show)))))))))]))
+               #,(with-attempt->size
+                  size-stx 'redex-check
+                  (if source-stx
+                      #`(let-values ([(metafunc/red-rel num-cases) 
+                                      #,(cond [(and (identifier? source-stx) (metafunc source-stx))
+                                               => (λ (x) #`(values #,x (length (metafunc-proc-cases #,x))))]
+                                              [else
+                                               #`(let ([r (assert-rel 'redex-check #,source-stx)])
+                                                   (values r (length (reduction-relation-make-procs r))))])])
+                          (check-lhs-pats
+                           lang
+                           metafunc/red-rel
+                           property
+                           (max 1 (floor (/ att num-cases)))
+                           ret
+                           'redex-check
+                           (and print? show)
+                           (test-match lang pat)
+                           (λ (generated) (redex-error 'redex-check "~s does not match ~s" generated 'pat))))
+                      #`(check-prop
+                         #,(term-generator #'lang #'pat 'redex-check)
+                         property att ret (and print? show)))))))))]))
 
 (define (format-attempts a)
   (format "~a attempt~a" a (if (= 1 a) "" "s")))
@@ -773,7 +794,7 @@
     (if (zero? remaining)
         #t
         (let ([attempt (add1 (- attempts remaining))])
-          (let-values ([(term bindings) (generator (attempt->size attempt) attempt retries)])
+          (let-values ([(term bindings) (generator ((attempt->size) attempt) attempt retries)])
             (if (andmap (λ (bindings) 
                           (with-handlers 
                               ([exn:fail?
@@ -866,25 +887,28 @@
 (define-syntax (check-metafunction stx)
   (syntax-case stx ()
     [(_ name property . kw-args)
-     (with-syntax ([m (metafunc/err #'name stx)]
-                   [(attempts retries print?) 
-                    (parse-kw-args `((#:attempts . , #'default-check-attempts)
-                                     (#:retries . ,#'default-retries)
-                                     (#:print? . #t))
-                                   (syntax kw-args)
-                                   stx)])
-       (with-syntax ([show (show-message stx)])
-         (syntax/loc stx
-           (let ([att (assert-nat 'check-metafunction attempts)]
-                 [ret (assert-nat 'check-metafunction retries)])
-             (check-lhs-pats 
-              (metafunc-proc-lang m)
-              m
-              (λ (term _) (property term))
-              att
-              ret
-              'check-metafunction
-              (and print? show))))))]))
+     (let-values ([(attempts retries print? size)
+                   (apply values
+                          (parse-kw-args `((#:attempts . , #'default-check-attempts)
+                                           (#:retries . ,#'default-retries)
+                                           (#:print? . #t)
+                                           (#:attempt-size . #f))
+                                         (syntax kw-args)
+                                         stx))]
+                  [(m) (metafunc/err #'name stx)])
+       (with-attempt->size
+        size 'check-metafunction
+        (quasisyntax/loc stx
+          (let ([att (assert-nat 'check-metafunction #,attempts)]
+                [ret (assert-nat 'check-metafunction #,retries)])
+            (check-lhs-pats 
+             (metafunc-proc-lang #,m)
+             #,m
+             (λ (term _) (property term))
+             att
+             ret
+             'check-metafunction
+             (and #,print? #,(show-message stx)))))))]))
 
 (define (reduction-relation-srcs r)
   (map (λ (proc) (or (rewrite-proc-name proc)
@@ -898,25 +922,28 @@
 (define-syntax (check-reduction-relation stx)
   (syntax-case stx ()
     [(_ relation property . kw-args)
-     (with-syntax ([(attempts retries print?)
-                    (parse-kw-args `((#:attempts . , #'default-check-attempts)
-                                     (#:retries . ,#'default-retries)
-                                     (#:print? . #t))
-                                   (syntax kw-args)
-                                   stx)]
-                   [show (show-message stx)])
-       (syntax/loc stx
-         (let ([att attempts]
-               [ret (assert-nat 'check-reduction-relation retries)]
-               [rel (assert-rel 'check-reduction-relation relation)])
-           (check-lhs-pats
-            (reduction-relation-lang rel)
-            rel
-            (λ (term _) (property term))
-            attempts
-            retries
-            'check-reduction-relation
-            (and print? show)))))]))
+     (let-values ([(attempts retries print? size)
+                   (apply values
+                          (parse-kw-args `((#:attempts . , #'default-check-attempts)
+                                           (#:retries . ,#'default-retries)
+                                           (#:print? . #t)
+                                           (#:attempt-size . #f))
+                                         (syntax kw-args)
+                                         stx))])
+       (with-attempt->size
+        size 'check-reduction-relation
+        (quasisyntax/loc stx
+          (let ([att (assert-nat 'check-reduction-relation #,attempts)]
+                [ret (assert-nat 'check-reduction-relation #,retries)]
+                [rel (assert-rel 'check-reduction-relation relation)])
+            (check-lhs-pats
+             (reduction-relation-lang rel)
+             rel
+             (λ (term _) (property term))
+             att
+             ret
+             'check-reduction-relation
+             (and #,print? #,(show-message stx)))))))]))
 
 (define-signature decisions^
   (next-variable-decision
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index a50fafd936..7da2bab25a 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -1209,12 +1209,14 @@ repeating as necessary. The optional keyword argument @racket[retries-expr]
                        (code:line #:source metafunction)
                        (code:line #:source relation-expr)
                        (code:line #:retries retries-expr)
-                       (code:line #:print? print?-expr)])
+                       (code:line #:print? print?-expr)
+                       (code:line #:attempt-size attempt-size-expr)])
               #:contracts ([property-expr any/c]
                            [attempts-expr natural-number/c]
                            [relation-expr reduction-relation?]
                            [retries-expr natural-number/c]
-                           [print?-expr any/c])]{
+                           [print?-expr any/c]
+                           [attempt-size-expr (-> natural-number/c natural-number/c)])]{
 Searches for a counterexample to @racket[property-expr], interpreted
 as a predicate universally quantified over the pattern variables
 bound by @racket[pattern]. @racket[redex-check] constructs and tests 
@@ -1224,8 +1226,11 @@ using the @racket[match-bindings] produced by @racket[match]ing
 @math{t} against @racket[pattern].
 
 @racket[redex-check] generates at most @racket[attempts-expr] (default @racket[1000])
-random terms in its search. The size and complexity of these terms increase with 
-each failed attempt. 
+random terms in its search. The size and complexity of these terms tend to increase 
+with each failed attempt. The @racket[#:attempt-size] keyword determines the rate at which
+terms grow by supplying a function that bounds term size based on the number of failed
+attempts (see @racket[generate-term]'s @racket[#:size] keyword). By default, the bound
+grows logarithmically with failed attempts.
 
 When @racket[print?-expr] produces any non-@racket[#f] value (the default), 
 @racket[redex-check] prints the test outcome on @racket[current-output-port].
@@ -1295,11 +1300,13 @@ and the @racket[exn:fail:redex:test-term] component contains the term that induc
 @defform/subs[(check-reduction-relation relation property kw-args ...)
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:retries retries-expr)
-                       (code:line #:print? print?-expr)])
+                       (code:line #:print? print?-expr)
+                       (code:line #:attempt-size attempt-size-expr)])
               #:contracts ([property (-> any/c any/c)]
                            [attempts-expr natural-number/c]
                            [retries-expr natural-number/c]
-                           [print?-expr any/c])]{
+                           [print?-expr any/c]
+                           [attempt-size-expr (-> natural-number/c natural-number/c)])]{
 Tests @racket[relation] as follows: for each case of @racket[relation],
 @racket[check-reduction-relation] generates @racket[attempts] random
 terms that match that case's left-hand side and applies @racket[property] 
@@ -1314,11 +1321,13 @@ when @racket[relation] is a relation on @racket[L] with @racket[n] rules.}
 @defform/subs[(check-metafunction metafunction property kw-args ...)
               ([kw-arg (code:line #:attempts attempts-expr)
                        (code:line #:retries retries-expr)
-                       (code:line #:print? print?-expr)])
+                       (code:line #:print? print?-expr)
+                       (code:line #:attempt-size attempt-size-expr)])
               #:contracts ([property (-> (listof any/c) any/c)]
                            [attempts-expr natural-number/c]
                            [retries-expr natural-number/c]
-                           [print?-expr any/c])]{
+                           [print?-expr any/c]
+                           [attempt-size-expr (-> natural-number/c natural-number/c)])]{
 Like @racket[check-reduction-relation] but for metafunctions. 
 @racket[check-metafunction] calls @racket[property] with lists
 containing arguments to the metafunction.}
diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt
index bab60b4856..b4fda93812 100644
--- a/collects/redex/tests/rg-test.rkt
+++ b/collects/redex/tests/rg-test.rkt
@@ -662,6 +662,15 @@
                           #:source mf)))
           #rx"no counterexamples"))
   
+  ; Without the #:attempt-size argument, the attempt would use size 0,
+  ; which does not require a non-terminal decision.
+  (test (let/ec k
+          (parameterize ([generation-decisions 
+                          (decisions #:nt (list (λ _ (k #t))))])
+            (redex-check lang d #t #:attempts 1 #:print? #f #:attempt-size add1)
+            #f))
+        #t)
+  
   (test (raised-exn-msg 
          exn:fail:redex?
          (redex-check lang n #t #:source (reduction-relation lang (--> x 1))))
@@ -818,6 +827,15 @@
          (λ () (check-reduction-relation (reduction-relation L (--> 1 2) (--> 3 4 name)) (curry eq? 1))))
         #px"counterexample found after 1 attempt with name:\n3\n")
   
+  (test (let/ec k
+          (parameterize ([generation-decisions 
+                          (decisions #:nt (list (λ _ (k #t))))])
+            (check-reduction-relation 
+             (reduction-relation L (--> e e))
+             (λ _ #t) #:attempts 1 #:print? #f #:attempt-size add1)
+            #f))
+        #t)
+  
   (let ([T (reduction-relation
             L
             (==> number number
@@ -909,6 +927,16 @@
           generated)
         '((4 4) (4 3) (3 4)))
   
+  (test (let/ec k
+          (define-language L (n number))
+          (define-metafunction L
+            [(f n) n])
+          (parameterize ([generation-decisions 
+                          (decisions #:nt (list (λ _ (k #t))))])
+            (check-metafunction f (λ _ #t) #:attempts 1 #:print? #f #:attempt-size add1)
+            #f))
+        #t)
+  
   (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
   (test (output (λ () (check-metafunction m (curry eq? 1))))
         #px"check-metafunction:.*counterexample found after 1 attempt with clause at .*:\\d+:\\d+")