diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt
index e241407237..347fddeb03 100644
--- a/collects/redex/examples/racket-machine/verification-test.rkt
+++ b/collects/redex/examples/racket-machine/verification-test.rkt
@@ -390,6 +390,10 @@
  (negate bytecode-ok?)
  '(let-void 1 (branch #f (let-rec ((lam () (0) 'x)) 'y) (loc-noclr 0))))
 
+(test-predicate
+ (negate bytecode-ok?)
+ '(let-void 1 (let-rec ((lam () () 'x)) 'y)))
+
 ;; ignored? properly maintained
 (test-predicate
  (negate bytecode-ok?)
diff --git a/collects/redex/examples/racket-machine/verification.rkt b/collects/redex/examples/racket-machine/verification.rkt
index 6c55d629e4..ffebd96855 100644
--- a/collects/redex/examples/racket-machine/verification.rkt
+++ b/collects/redex/examples/racket-machine/verification.rkt
@@ -140,7 +140,7 @@
    (side-condition (< (term n_p) (term n_l)))]
   
   ; let-rec
-  [(verify (let-rec ((name l (lam ((name v val) ...) (n_0 ...) e_0)) ...) e) (ṽ_0 ... ṽ_n ...) n_l b γ η f)
+  [(verify (let-rec ((name l (lam ((name v val) ...) (n_0 n_1 ...) e_0)) ...) e) (ṽ_0 ... ṽ_n ...) n_l b γ η f)
    (verify e s_1 n_l b γ η f)
    (where n ,(length (term (l ...))))
    (side-condition (= (length (term (ṽ_0 ...))) (term n)))