diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt
index c91a430a83..9ca315320a 100644
--- a/collects/redex/examples/racket-machine/verification-test.rkt
+++ b/collects/redex/examples/racket-machine/verification-test.rkt
@@ -383,6 +383,13 @@
                               void)
                       (application (loc 2)))))
 
+(test-predicate
+ bytecode-ok?
+ '(let-one 'x
+           (branch #f
+                   (let-one (loc-noclr 1) void)
+                   (loc-clr 0))))
+
 ; let-rec
 (test-predicate
  bytecode-ok?
diff --git a/collects/redex/examples/racket-machine/verification.rkt b/collects/redex/examples/racket-machine/verification.rkt
index 23ab03806c..cc98c4a0c2 100644
--- a/collects/redex/examples/racket-machine/verification.rkt
+++ b/collects/redex/examples/racket-machine/verification.rkt
@@ -65,7 +65,7 @@
   
   ; let-one
   [(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f)
-   (verify e_b (imm ṽ_1* ...) ,(add1 (term n_l)) b γ η (shift 1 f))
+   (verify e_b (imm ṽ_1* ...) ,(add1 (term n_l)) b γ_1 η_1 (shift 1 f))
    (where s_0 (uninit ṽ_1 ...))
    (where (s_1 γ_1 η_1) (verify e_r s_0 ,(add1 (term n_l)) #f γ η ∅))
    (where (uninit ṽ_1* ...) (trim s_1 s_0))]