** 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) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (declare-fun s0 () (_ BitVec 16))
[GOOD] (define-fun s1 () (_ BitVec 16) #x0000)
[GOOD] (define-fun s3 () (_ BitVec 16) #x0001)
[GOOD] (define-fun s2 () Bool (bvsle s1 s0))
[GOOD] (define-fun s4 () Bool (bvslt s0 s3))
[GOOD] (define-fun s5 () Bool (and s2 s4))
[GOOD] (assert s5)
[GOOD] (declare-fun s6 () (_ BitVec 16))
[GOOD] (define-fun s7 () Bool (bvsle s1 s6))
[GOOD] (define-fun s8 () Bool (bvslt s6 s3))
[GOOD] (define-fun s9 () Bool (and s7 s8))
[GOOD] (assert s9)
[GOOD] (push 1)
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
                                           ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
                                                         (proj_2_SBVTuple2 T2))))))
[GOOD] (declare-datatypes ((SBVMaybe 1)) ((par (T)
                                           ((nothing_SBVMaybe)
                                            (just_SBVMaybe (get_just_SBVMaybe T))))))
[GOOD] (define-fun s13 () (_ BitVec 16) #x000a)
[GOOD] (define-fun s15 () (_ BitVec 16) (bvneg #x0001))
[GOOD] (define-fun s17 () (_ BitVec 16) #x0007)
[GOOD] (define-fun s19 () (SBVMaybe (_ BitVec 16)) ((as just_SBVMaybe (SBVMaybe (_ BitVec 16))) #x0000))
[GOOD] (define-fun s20 () (SBVMaybe (_ BitVec 16)) (as nothing_SBVMaybe (SBVMaybe (_ BitVec 16))))
[GOOD] (define-fun s28 () (_ BitVec 16) #x00ff)
[GOOD] (declare-fun table0 ((_ BitVec 16)) (_ BitVec 16))
[GOOD] (define-fun s10 () (SBVTuple2 (_ BitVec 16) (_ BitVec 16)) (mkSBVTuple2 s0 s6))
[GOOD] (define-fun s11 () (_ BitVec 16) (proj_1_SBVTuple2 s10))
[GOOD] (define-fun s12 () Bool (= s3 s11))
[GOOD] (define-fun s14 () Bool (= s11 s13))
[GOOD] (define-fun s16 () (_ BitVec 16) (proj_2_SBVTuple2 s10))
[GOOD] (define-fun s18 () Bool (= s16 s17))
[GOOD] (define-fun s21 () (SBVMaybe (_ BitVec 16)) (ite s18 s19 s20))
[GOOD] (define-fun s22 () (_ BitVec 16) (get_just_SBVMaybe s21))
[GOOD] (define-fun s23 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 16)))) s21))
[GOOD] (define-fun s24 () (_ BitVec 16) (ite s23 s15 s22))
[GOOD] (define-fun s25 () (_ BitVec 16) (ite (or (bvslt s24 #x0000) (bvsle #x0001 s24)) s15 (table0 s24)))
[GOOD] (define-fun s26 () Bool (= s1 s25))
[GOOD] (define-fun s27 () Bool (= s1 s24))
[GOOD] (define-fun s29 () (_ BitVec 16) (ite s27 s28 s3))
[GOOD] (define-fun s30 () (_ BitVec 16) (ite s26 s29 s3))
[GOOD] (define-fun s31 () (_ BitVec 16) (ite s14 s30 s3))
[GOOD] (define-fun s32 () (_ BitVec 16) (ite s12 s3 s31))
[GOOD] (define-fun s33 () Bool (= s3 s32))
[GOOD] (define-fun s34 () Bool ((_ pbeq 1 1) s33))
[GOOD] (define-fun table0_initializer_0 () Bool (= (table0 #x0000) s3))
[GOOD] (define-fun table0_initializer () Bool table0_initializer_0)
[GOOD] (assert table0_initializer)
[GOOD] (assert s34)
[SEND] (check-sat)
[RECV] sat
[GOOD] (pop 1)
[GOOD] (assert table0_initializer)
[GOOD] (declare-fun s35 () (_ BitVec 16))
[GOOD] (define-fun s36 () Bool (bvsle s1 s35))
[GOOD] (define-fun s37 () Bool (bvslt s35 s3))
[GOOD] (define-fun s38 () Bool (and s36 s37))
[GOOD] (assert s38)
[GOOD] (declare-fun s39 () (_ BitVec 16))
[GOOD] (define-fun s40 () Bool (bvsle s1 s39))
[GOOD] (define-fun s41 () Bool (bvslt s39 s3))
[GOOD] (define-fun s42 () Bool (and s40 s41))
[GOOD] (assert s42)
[GOOD] (push 1)
[GOOD] (define-fun s48 () (_ BitVec 16) #x0006)
[GOOD] (define-fun s56 () (_ BitVec 16) #x0002)
[GOOD] (declare-fun table1 ((_ BitVec 16)) (_ BitVec 16))
[GOOD] (declare-fun table2 ((_ BitVec 16)) (_ BitVec 16))
[GOOD] (define-fun s43 () (SBVTuple2 (_ BitVec 16) (_ BitVec 16)) (mkSBVTuple2 s35 s39))
[GOOD] (define-fun s44 () (_ BitVec 16) (proj_1_SBVTuple2 s43))
[GOOD] (define-fun s45 () Bool (= s3 s44))
[GOOD] (define-fun s46 () (_ BitVec 16) (proj_2_SBVTuple2 s43))
[GOOD] (define-fun s47 () Bool (bvsle s3 s46))
[GOOD] (define-fun s49 () Bool (bvsle s46 s48))
[GOOD] (define-fun s50 () Bool (and s47 s49))
[GOOD] (define-fun s51 () Bool (bvsle s3 s16))
[GOOD] (define-fun s52 () Bool (bvsle s16 s48))
[GOOD] (define-fun s53 () Bool (and s51 s52))
[GOOD] (define-fun s54 () (_ BitVec 16) (bvsub s1 s3))
[GOOD] (define-fun s55 () Bool (= s1 s54))
[GOOD] (define-fun s57 () (_ BitVec 16) (ite s55 s56 s1))
[GOOD] (define-fun s58 () (_ BitVec 16) (bvsub s46 s3))
[GOOD] (define-fun s59 () (_ BitVec 16) (ite (or (bvslt s58 #x0000) (bvsle #x0001 s58)) s1 (table1 s58)))
[GOOD] (define-fun s60 () Bool (= s1 s59))
[GOOD] (define-fun s61 () Bool (= s13 s44))
[GOOD] (define-fun s62 () Bool (= s17 s46))
[GOOD] (define-fun s63 () (SBVMaybe (_ BitVec 16)) (ite s62 s19 s20))
[GOOD] (define-fun s64 () (_ BitVec 16) (get_just_SBVMaybe s63))
[GOOD] (define-fun s65 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 16)))) s63))
[GOOD] (define-fun s66 () (_ BitVec 16) (ite s65 s15 s64))
[GOOD] (define-fun s67 () (_ BitVec 16) (ite (or (bvslt s66 #x0000) (bvsle #x0001 s66)) s15 (table2 s66)))
[GOOD] (define-fun s68 () Bool (= s1 s67))
[GOOD] (define-fun s69 () Bool (= s1 s66))
[GOOD] (define-fun s70 () (_ BitVec 16) (ite s69 s28 s32))
[GOOD] (define-fun s71 () (_ BitVec 16) (ite s68 s70 s32))
[GOOD] (define-fun s72 () (_ BitVec 16) (ite s61 s71 s32))
[GOOD] (define-fun s73 () (_ BitVec 16) (ite s45 s32 s72))
[GOOD] (define-fun s74 () Bool (= s3 s73))
[GOOD] (define-fun s75 () Bool ((_ pbeq 1 1) s74))
[GOOD] (define-fun table1_initializer_0 () Bool (= (table1 #x0000) s57))
[GOOD] (define-fun table1_initializer () Bool table1_initializer_0)
[GOOD] (assert table1_initializer)
[GOOD] (define-fun table2_initializer_0 () Bool (= (table2 #x0000) s32))
[GOOD] (define-fun table2_initializer () Bool table2_initializer_0)
[GOOD] (assert table2_initializer)
[GOOD] (assert s75)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s10))
[RECV] ((s10 (mkSBVTuple2 #x0000 #x0000)))
[SEND] (get-value (s43))
[RECV] ((s43 (mkSBVTuple2 #x0000 #x0000)))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:[(0,0),(0,0)]
DONE!