;; 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 (0 (u . "(vector 0 (ite b 3 1) (ite b 2 4))\n"))))
 #""
 #"")
((define sol1 (solve (assert b)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((evaluate y sol1)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'#(0 3 2)\n"))))
 #""
 #"")
((define sol2 (solve (assert (not b))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((evaluate y sol2)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'#(0 1 4)\n"))))
 #""
 #"")
((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 (pretty-print (vc)) (hash-clear! h))
 ((3) 0 () 0 () () (c values c (void)))
 #"(vc b #t)\n"
 #"")
(h
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'#hash()\n"))))
 #""
 #"")
