Fixes another bug in model's `branch' verification

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?

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