1** Calling: z3 -nw -in -smt2 2[GOOD] ; Automatically generated by SBV. Do not edit. 3[GOOD] (set-option :print-success true) 4[GOOD] (set-option :global-declarations true) 5[GOOD] (set-option :smtlib2_compliant true) 6[GOOD] (set-option :diagnostic-output-channel "stdout") 7[GOOD] (set-option :produce-models true) 8[GOOD] (set-logic ALL) ; external query, using all logics. 9[GOOD] ; --- uninterpreted sorts --- 10[GOOD] ; --- tuples --- 11[GOOD] ; --- sums --- 12[GOOD] ; --- literal constants --- 13[GOOD] (define-fun s2 () (_ BitVec 32) #x00000000) 14[GOOD] ; --- skolem constants --- 15[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a" 16[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b" 17[GOOD] ; --- constant tables --- 18[GOOD] ; --- skolemized tables --- 19[GOOD] ; --- arrays --- 20[GOOD] ; --- uninterpreted constants --- 21[GOOD] ; --- user given axioms --- 22[GOOD] ; --- formula --- 23[GOOD] (define-fun s3 () Bool (bvsgt s0 s2)) 24[GOOD] (define-fun s4 () Bool (bvsgt s1 s2)) 25[GOOD] (assert (! s3 :named |a > 0|)) 26[GOOD] (assert s4) 27[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002) 28[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f) 29[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5)) 30[GOOD] (define-fun s8 () Bool (bvsle s6 s7)) 31[GOOD] (assert s8) 32[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003) 33[GOOD] (define-fun s10 () Bool (bvslt s0 s9)) 34[GOOD] (assert s10) 35[GOOD] (define-fun s11 () Bool (bvslt s1 s5)) 36[GOOD] (assert s11) 37[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c) 38[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1)) 39[GOOD] (define-fun s14 () Bool (bvslt s12 s13)) 40[GOOD] (assert (! s14 :named |a+b_<_12|)) 41[GOOD] (push 1) 42[GOOD] (define-fun s15 () Bool (bvslt s0 s5)) 43[GOOD] (assert s15) 44[SEND] (check-sat) 45[RECV] sat 46[SEND] (get-value (s0)) 47[RECV] ((s0 #x00000001)) 48[GOOD] (pop 1) 49[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001) 50[GOOD] (define-fun s17 () Bool (bvsgt s0 s16)) 51[GOOD] (assert (! s17 :named |extra|)) 52[GOOD] (assert s11) 53[SEND] (check-sat) 54[RECV] sat 55[SEND] (get-value (s0)) 56[RECV] ((s0 #x00000002)) 57[SEND] (get-value (s1)) 58[RECV] ((s1 #x00000001)) 59*** Solver : Z3 60*** Exit code: ExitSuccess 61