;; 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)"))))
 #""
 #"")
((clear-asserts!) ((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)) #"" #"")
((asserts)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (c (0 (u . "b")))))
 #""
 #"")
((clear-asserts!) ((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))
 #""
 #"")
((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"))))
 #""
 #"")
((asserts)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (c (0 (u . "b")))))
 #""
 #"")
((clear-asserts!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((=> #f (begin (displayln "hello") #f))
 ((3) 0 () 0 () () (q values #t))
 #""
 #"")
((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"))))
 #""
 #"")
((asserts)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (c (0 (u . "b")))))
 #""
 #"")
((clear-asserts!) ((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))"))))
 #""
 #"")
((define-symbolic t boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((forall (list t x y) (= (+ (if t x 'x) 1) y))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(forall (t x y) (= y (+ 1 x)))"))))
 #""
 #"")
((asserts)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (c (0 (u . "t")))))
 #""
 #"")
((clear-asserts!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-values (q-body q-asserts) (with-asserts (= (+ (if t x 'x) 1) y)))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
(q-body
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(= y (+ 1 x))"))))
 #""
 #"")
(q-asserts
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (c (0 (u . "t")))))
 #""
 #"")
((forall (list t x y) (=> (apply && q-asserts) q-body))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(forall (t x y) (|| (! t) (= y (+ 1 x))))"))))
 #""
 #"")
((asserts) ((3) 0 () 0 () () (q values ())) #"" #"")
((define-symbolic a b integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define f (forall (list a) (exists (list b) (= a (+ a b)))))
 ((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)"))))
 #""
 #"")
((define g (forall (list a) (= a (+ a b))))
 ((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 [b 0])"))))
 #""
 #"")
((define h (exists (list a) (forall (list a) (= a (+ a a)))))
 ((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)"))))
 #""
 #"")
