;; This file was created by make-log-based-eval
((define v1 (box 1)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define v2 (box 1)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((eq? v1 v2) ((3) 0 () 0 () () (q values #f)) #"" #"")
((equal? v1 v2) ((3) 0 () 0 () () (q values #t)) #"" #"")
((define v3 (box-immutable 1)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define v4 (box-immutable 1)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((eq? v3 v4) ((3) 0 () 0 () () (q values #t)) #"" #"")
((equal? v1 v3) ((3) 0 () 0 () () (q values #t)) #"" #"")
((define-symbolic x integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define v1 (box x)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define v2 (if b v1 (box 3))) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define sol (solve (assert (= 4 (unbox v2)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
(sol
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 4]\n [b #t])\n"))))
 #""
 #"")
((evaluate v1 sol)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'#&4\n"))))
 #""
 #"")
((evaluate v2 sol)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "'#&4\n"))))
 #""
 #"")
((evaluate (eq? v1 v2) sol) ((3) 0 () 0 () () (q values #t)) #"" #"")
