** 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-models true) [GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s11 () (_ BitVec 32) #x00000001) [GOOD] (define-fun s12 () (_ BitVec 32) #x00000000) [GOOD] (define-fun s32 () (_ BitVec 32) #x00000008) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Bool) ; tracks user variable "b0" [GOOD] (declare-fun s1 () Bool) ; tracks user variable "b1" [GOOD] (declare-fun s2 () Bool) ; tracks user variable "b2" [GOOD] (declare-fun s3 () Bool) ; tracks user variable "b3" [GOOD] (declare-fun s4 () Bool) ; tracks user variable "b4" [GOOD] (declare-fun s5 () Bool) ; tracks user variable "b5" [GOOD] (declare-fun s6 () Bool) ; tracks user variable "b6" [GOOD] (declare-fun s7 () Bool) ; tracks user variable "b7" [GOOD] (declare-fun s8 () Bool) ; tracks user variable "b8" [GOOD] (declare-fun s9 () Bool) ; tracks user variable "b9" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- [GOOD] (define-fun s10 () Bool ((_ at-most 8) s0 s1 s2 s3 s4 s5 s6 s7 s8 s9)) [GOOD] (define-fun s13 () (_ BitVec 32) (ite s0 s11 s12)) [GOOD] (define-fun s14 () (_ BitVec 32) (ite s1 s11 s12)) [GOOD] (define-fun s15 () (_ BitVec 32) (bvadd s13 s14)) [GOOD] (define-fun s16 () (_ BitVec 32) (ite s2 s11 s12)) [GOOD] (define-fun s17 () (_ BitVec 32) (bvadd s15 s16)) [GOOD] (define-fun s18 () (_ BitVec 32) (ite s3 s11 s12)) [GOOD] (define-fun s19 () (_ BitVec 32) (bvadd s17 s18)) [GOOD] (define-fun s20 () (_ BitVec 32) (ite s4 s11 s12)) [GOOD] (define-fun s21 () (_ BitVec 32) (bvadd s19 s20)) [GOOD] (define-fun s22 () (_ BitVec 32) (ite s5 s11 s12)) [GOOD] (define-fun s23 () (_ BitVec 32) (bvadd s21 s22)) [GOOD] (define-fun s24 () (_ BitVec 32) (ite s6 s11 s12)) [GOOD] (define-fun s25 () (_ BitVec 32) (bvadd s23 s24)) [GOOD] (define-fun s26 () (_ BitVec 32) (ite s7 s11 s12)) [GOOD] (define-fun s27 () (_ BitVec 32) (bvadd s25 s26)) [GOOD] (define-fun s28 () (_ BitVec 32) (ite s8 s11 s12)) [GOOD] (define-fun s29 () (_ BitVec 32) (bvadd s27 s28)) [GOOD] (define-fun s30 () (_ BitVec 32) (ite s9 s11 s12)) [GOOD] (define-fun s31 () (_ BitVec 32) (bvadd s29 s30)) [GOOD] (define-fun s33 () Bool (bvule s31 s32)) [GOOD] (define-fun s34 () Bool (= s10 s33)) [GOOD] (define-fun s35 () Bool (not s34)) [GOOD] (assert s35) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 *** Exit code: ExitSuccess