;; This file was created by make-log-based-eval
((require (only-in racket string->symbol))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define p (if b * -)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define sol (synthesize #:forall (list x) #:guarantee (assert (= x (p x 1)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((evaluate p sol)
 ((3)
  1
  (((lib "rosette/doc/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "*"))))
 #""
 #"")
((define sol (synthesize #:forall (list x) #:guarantee (assert (= x (p x 0)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((evaluate p sol)
 ((3)
  1
  (((lib "rosette/doc/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "-"))))
 #""
 #"")
