;; This file was created by make-log-based-eval
((define y (vector 0 1 2)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((if b (vector-set! y 1 3) (vector-set! y 2 4))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
(y
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (v! 0 (0 (u . "(ite b 3 1)")) (0 (u . "(ite b 2 4)")))))
 #""
 #"")
((define env1 (solve (assert b)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((evaluate y env1) ((3) 0 () 0 () () (c values c (v! 0 3 2))) #"" #"")
((define env2 (solve (assert (not b))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((evaluate y env2) ((3) 0 () 0 () () (c values c (v! 0 1 4))) #"" #"")
((require (only-in racket make-hash hash-clear! hash-ref))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define h (make-hash '((1 . 2))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define-symbolic key integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((hash-ref h key 0) ((3) 0 () 0 () () (q values 0)) #"" #"")
((when b (hash-clear! h)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
(h ((3) 0 () 0 () () (c values c (h ! (equal)))) #"" #"")
