diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt
index 9ca315320a..20c4fd4de0 100644
--- a/collects/redex/examples/racket-machine/verification-test.rkt
+++ b/collects/redex/examples/racket-machine/verification-test.rkt
@@ -390,6 +390,15 @@
                    (let-one (loc-noclr 1) void)
                    (loc-clr 0))))
 
+(test-predicate
+ (negate bytecode-ok?)
+ '(proc-const (val)
+              (seq
+               (branch (loc 0)
+                       (loc-clr 0)
+                       void)
+               (install-value 0 'x void))))
+
 ; 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 cc98c4a0c2..0c0b904635 100644
--- a/collects/redex/examples/racket-machine/verification.rkt
+++ b/collects/redex/examples/racket-machine/verification.rkt
@@ -310,7 +310,7 @@
   [(redo-clears γ invalid) invalid]
   [(redo-clears () s) s]
   [(redo-clears ((n_0 ṽ_0) (n_1 ṽ_1) ...) s) 
-   (redo-clears ((n_1 ṽ_1) ...) (set uninit n_0 s))])
+   (redo-clears ((n_1 ṽ_1) ...) (set not n_0 s))])
 
 (define-metafunction verification
   trim : s s -> s