Fixes a bug in the VM model

collects/redex/examples/racket-machine/verification-test.rkt

@@ -496,6 +496,14 @@
  (negate bytecode-ok?)
  '(let-void-box 1 (application (case-lam (lam (ref) () (loc-box-noclr 0))) (loc-noclr 1))))
 
+(test-predicate
+ (negate bytecode-ok?)
+ '(let-one 42
+           (boxenv 0
+                   (application
+                    (case-lam (lam (ref) () (loc-box 0)))
+                    (loc-box 1)))))
+
 ; literals
 (test-predicate bytecode-ok? #t)
 

collects/redex/examples/racket-machine/verification.rkt

@@ -108,7 +108,7 @@
    (verify (lam (τ ...) () e) s n_l b γ η f)]
   
   ; case-lam
-  [(verify (case-lam l ...) s n_l b γ η f)
+  [(verify (case-lam (name l (lam (val ...) (n ...) e)) ...) s n_l b γ η f)
    (s γ η)
    (side-condition (term (AND (verify-lam l s ?) ...)))]