;; This file was created by make-log-based-eval
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((boolean? b) ((3) 0 () 0 () () (q values #t)) #"" #"")
((boolean? #t) ((3) 0 () 0 () () (q values #t)) #"" #"")
((boolean? #f) ((3) 0 () 0 () () (q values #t)) #"" #"")
((boolean? 1) ((3) 0 () 0 () () (q values #f)) #"" #"")
((not b)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(! b)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((! #f) ((3) 0 () 0 () () (q values #t)) #"" #"")
((! #t) ((3) 0 () 0 () () (q values #f)) #"" #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((! (if b #f 3)) ((3) 0 () 0 () () (q values #t)) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t b)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((&&) ((3) 0 () 0 () () (q values #t)) #"" #"")
((||) ((3) 0 () 0 () () (q values #f)) #"" #"")
((&& #f (begin (displayln "hello") #t))
 ((3) 0 () 0 () () (q values #f))
 #"hello\n"
 #"")
((define-symbolic a b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((&& a (if b #t 1))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "a\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t b)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((=> #f (begin (displayln "hello") #f))
 ((3) 0 () 0 () () (q values #t))
 #"hello\n"
 #"")
((define-symbolic a b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((<=> a (if b #t 1))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "a\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t b)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x y integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((exists (list x y) (= x y))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(exists (x y) (= x y))\n"))))
 #""
 #"")
((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((forall (list b x y) (= (+ (if b x 'x) 1) y))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(forall (b x y) (= y (+ 1 x)))\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t b)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define out (with-vc (= (+ (if b x 'x) 1) y)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
(out
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(normal (= y (+ 1 x)) (vc #t b))\n"))))
 #""
 #"")
((define out-val (result-value out))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((define out-vc (result-state out))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((forall
  (list b x y)
  (=> (&& (vc-assumes out-vc) (vc-asserts out-vc)) out-val))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(forall (b x y) (|| (! b) (= y (+ 1 x))))\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\n"))))
 #""
 #"")
((define-symbolic x y integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define f (forall (list x) (exists (list y) (= x (+ x y)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((solve (assert f))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model)\n"))))
 #""
 #"")
((define g (forall (list x) (= x (+ x y))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((solve (assert g))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [y 0])\n"))))
 #""
 #"")
((define h (exists (list x) (forall (list x) (= x (+ x x)))))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((solve (assert h))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
