;; This file was created by make-log-based-eval
((define (always-same) (define-symbolic x integer?) x)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((always-same)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "x\n"))))
 #""
 #"")
((always-same)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "x\n"))))
 #""
 #"")
((equal? (always-same) (always-same)) ((3) 0 () 0 () () (q values #t)) #"" #"")
((define (always-same-3) (define-symbolic y integer? #:length (+ 1 2)) y)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((always-same-3)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(list y$0 y$1 y$2)\n"))))
 #""
 #"")
((always-same-3)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(list y$0 y$1 y$2)\n"))))
 #""
 #"")
((equal? (always-same-3) (always-same-3))
 ((3) 0 () 0 () () (q values #t))
 #""
 #"")
((lambda (n) (define-symbolic y integer? #:length n) y)
 ((3)
  0
  ()
  0
  ()
  ()
  (q
   exn
   "eval:9.0: define-symbolic: expected a natural? for #:length\n  at: (define-symbolic y integer? #:length n)\n  in: (define-symbolic y integer? #:length n)"))
 #""
 #"")
((define (always-different) (define-symbolic* x integer?) x)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((always-different)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "x$0\n"))))
 #""
 #"")
((always-different)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "x$1\n"))))
 #""
 #"")
((eq? (always-different) (always-different))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(= x$2 x$3)\n"))))
 #""
 #"")
((define (always-different-n n) (define-symbolic* y integer? #:length n) y)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((always-different-n 2)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(list y$4 y$5)\n"))))
 #""
 #"")
((always-different-n 3)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(list y$6 y$7 y$8)\n"))))
 #""
 #"")
((equal? (always-different-n 4) (always-different-n 4))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c
   values
   c
   (0 (u . "(&& (= y$9 y$13) (= y$10 y$14) (= y$11 y$15) (= y$12 y$16))\n"))))
 #""
 #"")
((assert #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assert 1) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((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 boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assert x) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t x)\n"))))
 #""
 #"")
((assert #f "bad value")
 ((3) 0 () 0 () () (q exn "[assert] bad value"))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #f)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\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"))))
 #""
 #"")
((assume #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assume 1) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((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 boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assume x) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc x #t)\n"))))
 #""
 #"")
((assume #f "bad value")
 ((3) 0 () 0 () () (q exn "[assume] bad value"))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #f #t)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((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 a b c d boolean?)
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\n"))))
 #""
 #"")
((verify (assert a))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [a #f])\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"))))
 #""
 #"")
((assume a) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assert b) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc a (|| b (! a)))\n"))))
 #""
 #"")
((verify (begin (assume c) (assert d)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [a #t]\n [b #t]\n [c #t]\n [d #f])\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc a (|| b (! a)))\n"))))
 #""
 #"")
((verify (assert a))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\n"))))
 #""
 #"")
((verify (assert a))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [a #f])\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x c integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\n"))))
 #""
 #"")
((synthesize
  #:forall
  (list x)
  #:guarantee
  (begin (assume (even? x)) (assert (odd? (+ x c)))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [c 1])\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"))))
 #""
 #"")
((assume (odd? x)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc (! (= 0 (remainder x 2))) #t)\n"))))
 #""
 #"")
((synthesize #:forall (list x) #:guarantee (assert (odd? (+ x c))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [c 0])\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc (! (= 0 (remainder x 2))) #t)\n"))))
 #""
 #"")
((synthesize
  #:forall
  (list x)
  #:guarantee
  (begin (assume (even? x)) (assert (odd? (+ x c)))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\n"))))
 #""
 #"")
((synthesize
  #:forall
  (list x)
  #:guarantee
  (begin (assume (even? x)) (assert (odd? (+ x c)))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [c 1])\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x y boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((assume x) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc x #t)\n"))))
 #""
 #"")
((solve (assert y))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x #t]\n [y #t])\n"))))
 #""
 #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc x #t)\n"))))
 #""
 #"")
((solve (assert (not x)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((vc)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(vc #t #t)\n"))))
 #""
 #"")
((solve (assert (not x)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x #f])\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x y integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define inc (solve+)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((inc (< x y))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 0]\n [y 1])\n"))))
 #""
 #"")
((inc (> x 5))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 6]\n [y 7])\n"))))
 #""
 #"")
((inc (< y 4))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((inc 1)
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 6]\n [y 7])\n"))))
 #""
 #"")
((inc (< y 9))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 6]\n [y 7])\n"))))
 #""
 #"")
((inc 'shutdown) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((inc (> y 4))
 ((3)
  0
  ()
  0
  ()
  ()
  (q
   exn
   "solver-push: contract violation:\n  expected: solver?\n  given: #f\n  argument position: 1st"))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x y integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((optimize
  #:maximize
  (list (+ x y))
  #:guarantee
  (begin (assume (< x 2)) (assert (< (- y x) 1))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 1]\n [y 1])\n"))))
 #""
 #"")
((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((current-bitwidth 5) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic x y real?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((define-symbolic f (~> real? real?))
 ((3) 0 () 0 () () (c values c (void)))
 #""
 #"")
((current-bitwidth 5) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((solve (assert (= x 3.5)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 3])\n"))))
 #""
 #"")
((solve (assert (= x 64)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 0])\n"))))
 #""
 #"")
((solve (assert (and (= x 64) (= x 0))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 0])\n"))))
 #""
 #"")
((solve (assert (forall (list x) (= x (+ x y)))))
 ((3)
  0
  ()
  0
  ()
  ()
  (q
   exn
   "finitize: cannot use (current-bitwidth 5) with a quantified formula (forall (x) (= x (+ x y))); use (current-bitwidth #f) instead"))
 #""
 #"")
((solve (assert (= x (f x))))
 ((3)
  0
  ()
  0
  ()
  ()
  (q
   exn
   "finitize: cannot use (current-bitwidth 5) with an uninterpreted function f; use (current-bitwidth #f) instead"))
 #""
 #"")
((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((solve (assert (= x 3.5)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 7/2])\n"))))
 #""
 #"")
((solve (assert (= x 64)))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 64])\n"))))
 #""
 #"")
((solve (assert (and (= x 64) (= x 0))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unsat)\n"))))
 #""
 #"")
((solve (assert (forall (list x) (= x (+ x y)))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [y 0])\n"))))
 #""
 #"")
((solve (assert (= x (f x))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(model\n [x 0]\n [f (fv real?~>real?)])\n"))))
 #""
 #"")
((define-symbolic i j integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
((solve
  (begin
    (assert (> i 0))
    (assert (> j 0))
    (assert (or (= (/ i j) 2) (= (/ j i) 2)))))
 ((3)
  1
  (((lib "rosette/guide/scribble/util/lifted.rkt")
    .
    deserialize-info:opaque-v0))
  0
  ()
  ()
  (c values c (0 (u . "(unknown)\n"))))
 #""
 #"")
