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.8.4")
[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.8.4")
[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 (($x177 (<= s0 6)))
        (let (($x178 (not $x177)))
        (let (($x239 (or (not bey) $x178)))
        (let ((@x237 (monotonicity (rewrite (= (> s0 6) $x178)) (= (=> bey (> s0 6)) (=> bey $x178)))))
        (let ((@x243 (trans @x237 (rewrite (= (=> bey $x178) $x239)) (= (=> bey (> s0 6)) $x239))))
        (let ((@x244 (mp (asserted (=> bey (> s0 6))) @x243 $x239)))
        (let (($x256 (>= s0 6)))
        (let (($x255 (not $x256)))
        (let (($x265 (or (not hey) $x255)))
        (let ((@x258 (monotonicity (rewrite (= (<= 6 s0) $x256)) (= (not (<= 6 s0)) $x255))))
        (let ((@x260 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) @x258 (= (< s0 6) $x255))))
        (let ((@x269 (trans (monotonicity @x260 (= (=> hey (< s0 6)) (=> hey $x255))) (rewrite (= (=> hey $x255) $x265)) (= (=> hey (< s0 6)) $x265))))
        (let ((@x270 (mp (asserted (=> hey (< s0 6))) @x269 $x265)))
        (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x256 $x177)) (unit-resolution @x270 (asserted hey) $x255) (unit-resolution @x244 (asserted bey) $x178) 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!