query1.gold

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-unsat-cores true)
[GOOD] (set-option :produce-unsat-assumptions true)
[GOOD] (set-option :produce-proofs true)
[GOOD] (set-option :produce-interpolants true)
[GOOD] (set-option :random-seed 123)
[GOOD] (set-option :produce-assertions true)
[GOOD] (set-option :smt.mbqi true)
[GOOD] (set-option :produce-assignments true)
[GOOD] (set-info :status sat)
[GOOD] (set-info :bad what)
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL)
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)
[GOOD] (define-fun s_1 () Bool true)
[GOOD] (define-fun s6 () Int 0)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"
[GOOD] (declare-fun s1 () Int) ; tracks user variable "b"
[GOOD] (declare-fun s2 () (_ FloatingPoint  8 24)) ; tracks user variable "c"
[GOOD] (declare-fun s3 () Bool) ; tracks user variable "d"
[GOOD] (declare-fun s4 () Real) ; tracks user variable "e"
[GOOD] (declare-fun s5 () (_ BitVec 8))
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s7 () Bool (> s0 s6))
[GOOD] (define-fun s8 () Bool (> s1 s6))
[GOOD] (assert (! s7 :named |a > 0|))
[GOOD] (assert s8)
[GOOD] (define-fun s9 () Int 2)
[GOOD] (define-fun s11 () Int 5)
[GOOD] (define-fun s10 () Int (+ s0 s9))
[GOOD] (define-fun s12 () Bool (>= s10 s11))
[GOOD] (assert s12)
[GOOD] (define-fun s14 () Int 12)
[GOOD] (define-fun s13 () Int (+ s0 s1))
[GOOD] (define-fun s15 () Bool (< s13 s14))
[GOOD] (assert (! s15 :named |a+b_<_12|))
[SEND] (get-option :diagnostic-output-channel)
[RECV] stdout
[SEND] (get-option :produce-assertions)
[RECV] true
[SEND] (get-option :produce-assignments)
[RECV] true
[SEND] (get-option :produce-proofs)
[RECV] true
[SEND] (get-option :produce-interpolants)
[RECV] true
[SEND] (get-option :produce-unsat-assumptions)
[RECV] unsupported
[SEND] (get-option :produce-unsat-cores)
[SKIP] ; :produce-unsat-assumptions line: 44 position: 0
[RECV] true
[SEND] (get-option :random-seed)
[RECV] 123
[SEND] (get-option :reproducible-resource-limit)
[RECV] unsupported
[SEND] (get-option :verbosity)
[SKIP] ; :reproducible-resource-limit line: 47 position: 0
[RECV] 0
[SEND] (get-option :smt.mbqi)
[RECV] true
[SEND] (get-option :smt.mbqi)
[RECV] true
[SEND] (get-info :reason-unknown)
[RECV] (:reason-unknown "state of the most recent check-sat command is not known")
[SEND] (get-info :version)
[RECV] (:version "4.5.1")
[SEND] (get-info :status)
[RECV] (:status sat)
[GOOD] (define-fun s16 () Int 4)
[GOOD] (define-fun s17 () Bool (> s0 s16))
[GOOD] (assert (! s17 :named |later, a > 4|))
[SEND] (check-sat)
[RECV] sat
[GOOD] (set-info :status unknown)
[GOOD] (define-fun s18 () Bool (> s0 s9))
[GOOD] (declare-const __assumption_proxy_s18_19 Bool)
[GOOD] (assert (= __assumption_proxy_s18_19 s18))
[SEND] (check-sat-assuming (__assumption_proxy_s18_19))
[RECV] sat
[GOOD] (declare-const __assumption_proxy_s18_20 Bool)
[GOOD] (assert (= __assumption_proxy_s18_20 s18))
[SEND] (check-sat-assuming (__assumption_proxy_s18_20))
[RECV] sat
[SEND] (get-assignment)
[RECV] ((s_1 true) (s7 true) (|a > 0| true) (s15 true) (s_2 false) (s8 true) (a+b_<_12 true) (s17 true) (|later, a > 4| true) (s18 true) (s12 true))
[SEND] (get-info :assertion-stack-levels)
[RECV] (:assertion-stack-levels 0)
[SEND] (get-info :authors)
[RECV] (:authors "Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger")
[SEND] (get-info :error-behavior)
[RECV] (:error-behavior continued-execution)
[SEND] (get-info :name)
[RECV] (:name "Z3")
[SEND] (get-info :reason-unknown)
[RECV] (:reason-unknown "unknown")
[SEND] (get-info :version)
[RECV] (:version "4.5.1")
[SEND] (get-info :memory)
[RECV] unsupported
[SEND] (get-info :time)
[SKIP] ; :memory line: 73 position: 0
[RECV] unsupported
[SEND] (get-value (s0))
[SKIP] ; :time line: 74 position: 0
[RECV] ((s0 5))
[SEND] (get-value (s1))
[RECV] ((s1 1))
[GOOD] (define-fun s21 () Int 100)
[GOOD] (define-fun s23 () Int 9)
[GOOD] (define-fun s22 () Bool (> s0 s21))
[GOOD] (define-fun s24 () Bool (> s0 s23))
[GOOD] (declare-const __assumption_proxy_s22_25 Bool)
[GOOD] (assert (= __assumption_proxy_s22_25 s22))
[GOOD] (declare-const __assumption_proxy_s24_26 Bool)
[GOOD] (assert (= __assumption_proxy_s24_26 s24))
[SEND] (check-sat-assuming (__assumption_proxy_s22_25 __assumption_proxy_s24_26))
[RECV] unsat
[SEND] (get-unsat-assumptions)
[RECV] (a+b_<_12 __assumption_proxy_s22_25)
*** In call to 'getUnsatAssumptions'
***
***    Unexpected assumption named: "a+b_<_12"
***    Was expecting one of       : ["s22","s24"]
***
*** This can happen if unsat-cores are also enabled. Ignoring.
[GOOD] (push 5)
[GOOD] (pop 3)
[GOOD] (define-fun s27 () Int 6)
[GOOD] (define-fun s28 () Bool (> s0 s27))
[GOOD] (assert (! s28 :named |bey|))
[GOOD] (define-fun s29 () Bool (< s0 s27))
[GOOD] (assert (! s29 :named |hey|))
[SEND] (check-sat)
[RECV] unsat
[SEND, TimeOut: 80000ms] (get-unsat-core)
[RECV] (bey hey)
[SEND] (get-proof)
[RECV] ((set-logic ALL)
       (declare-fun bey () Bool)
       (declare-fun hey () Bool)
       (proof
       (let (($x232 (<= s0 6)))
       (let (($x233 (not $x232)))
       (let (($x236 (or (not bey) $x233)))
       (let ((@x238 (monotonicity (rewrite (= (> s0 6) $x233)) (= (or (not bey) (> s0 6)) $x236))))
       (let ((@x231 (rewrite (= (=> bey (> s0 6)) (or (not bey) (> s0 6))))))
       (let ((@x241 (mp (asserted (=> bey (> s0 6))) (trans @x231 @x238 (= (=> bey (> s0 6)) $x236)) $x236)))
       (let (($x252 (>= s0 6)))
       (let (($x250 (not $x252)))
       (let (($x254 (or (not hey) $x250)))
       (let ((@x256 (monotonicity (rewrite (= (< s0 6) $x250)) (= (or (not hey) (< s0 6)) $x254))))
       (let ((@x249 (rewrite (= (=> hey (< s0 6)) (or (not hey) (< s0 6))))))
       (let ((@x259 (mp (asserted (=> hey (< s0 6))) (trans @x249 @x256 (= (=> hey (< s0 6)) $x254)) $x254)))
       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x252 $x232)) (unit-resolution @x259 (asserted hey) $x250) (unit-resolution @x241 (asserted bey) $x233) false)))))))))))))))
[SEND, TimeOut: 90000ms] (get-assertions)

[RECV] ((! s7 :named |a > 0|)
        s8
        s12
        (! s15 :named |a+b_<_12|)
        (! s17 :named |later, a > 4|)
        (= __assumption_proxy_s18_19 s18)
        (= __assumption_proxy_s18_20 s18)
        (= __assumption_proxy_s22_25 s22)
        (= __assumption_proxy_s24_26 s24)
        (! s28 :named |bey|)
        (! s29 :named |hey|))
[SEND] (echo "there we go")
[RECV] "there we go"
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:Satisfiable. Model:
  a  =  332 :: Integer
  b  =    3 :: Integer
  c  =  2.3 :: Float
  d  = True :: Bool
  e  = 3.12 :: Real
  s5 =  -12 :: Int8
DONE!