** 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 QF_UFBV) ; NB. User specified.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "i"
[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "j"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s2 () (_ BitVec 8) #x00)
[GOOD] (define-fun s3 () (_ BitVec 8) #x01)
[GOOD] (define-fun s4 () (_ BitVec 8) #x02)
[GOOD] (define-fun s5 () (_ BitVec 8) #x03)
[GOOD] (define-fun s6 () (_ BitVec 8) #x04)
[GOOD] (define-fun s7 () (_ BitVec 8) #x05)
[GOOD] (define-fun s8 () (_ BitVec 8) #x06)
[GOOD] (define-fun s9 () (_ BitVec 8) #x07)
[GOOD] (define-fun s10 () (_ BitVec 8) #x08)
[GOOD] (define-fun s11 () (_ BitVec 8) #x09)
[GOOD] (define-fun s12 () (_ BitVec 8) #x0a)
[GOOD] (define-fun s13 () (_ BitVec 8) #x0b)
[GOOD] (define-fun s14 () (_ BitVec 8) #x0c)
[GOOD] (define-fun s15 () (_ BitVec 8) #x0d)
[GOOD] (define-fun s16 () (_ BitVec 8) #x0e)
[GOOD] (define-fun s17 () (_ BitVec 8) #x0f)
[GOOD] (define-fun s18 () (_ BitVec 8) #x10)
[GOOD] (define-fun s19 () (_ BitVec 8) #x11)
[GOOD] (define-fun s20 () (_ BitVec 8) #x12)
[GOOD] (define-fun s21 () (_ BitVec 8) #x13)
[GOOD] (define-fun s22 () (_ BitVec 8) #x14)
[GOOD] (define-fun s23 () (_ BitVec 8) #x15)
[GOOD] (define-fun s24 () (_ BitVec 8) #x16)
[GOOD] (define-fun s25 () (_ BitVec 8) #x17)
[GOOD] (define-fun s26 () (_ BitVec 8) #x18)
[GOOD] (define-fun s27 () (_ BitVec 8) #x19)
[GOOD] (define-fun s28 () (_ BitVec 8) #x1a)
[GOOD] (define-fun s29 () (_ BitVec 8) #x1b)
[GOOD] (define-fun s30 () (_ BitVec 8) #x1c)
[GOOD] (define-fun s31 () (_ BitVec 8) #x1d)
[GOOD] (define-fun s32 () (_ BitVec 8) #x1e)
[GOOD] (define-fun s33 () (_ BitVec 8) #x1f)
[GOOD] (define-fun s34 () (_ BitVec 8) #x20)
[GOOD] (define-fun s35 () (_ BitVec 8) #x21)
[GOOD] (define-fun s36 () (_ BitVec 8) #x22)
[GOOD] (define-fun s37 () (_ BitVec 8) #x23)
[GOOD] (define-fun s38 () (_ BitVec 8) #x24)
[GOOD] (define-fun s39 () (_ BitVec 8) #x25)
[GOOD] (define-fun s40 () (_ BitVec 8) #x26)
[GOOD] (define-fun s41 () (_ BitVec 8) #x27)
[GOOD] (define-fun s42 () (_ BitVec 8) #x28)
[GOOD] (define-fun s43 () (_ BitVec 8) #x29)
[GOOD] (define-fun s44 () (_ BitVec 8) #x2a)
[GOOD] (define-fun s45 () (_ BitVec 8) #x2b)
[GOOD] (define-fun s46 () (_ BitVec 8) #x2c)
[GOOD] (define-fun s47 () (_ BitVec 8) #x2d)
[GOOD] (define-fun s48 () (_ BitVec 8) #x2e)
[GOOD] (define-fun s49 () (_ BitVec 8) #x2f)
[GOOD] (define-fun s50 () (_ BitVec 8) #x30)
[GOOD] (define-fun s51 () (_ BitVec 8) #x31)
[GOOD] (define-fun s52 () (_ BitVec 8) #x32)
[GOOD] (define-fun s53 () (_ BitVec 8) #x33)
[GOOD] (define-fun s54 () (_ BitVec 8) #x34)
[GOOD] (define-fun s55 () (_ BitVec 8) #x35)
[GOOD] (define-fun s56 () (_ BitVec 8) #x36)
[GOOD] (define-fun s57 () (_ BitVec 8) #x37)
[GOOD] (define-fun s58 () (_ BitVec 8) #x38)
[GOOD] (define-fun s59 () (_ BitVec 8) #x39)
[GOOD] (define-fun s60 () (_ BitVec 8) #x3a)
[GOOD] (define-fun s61 () (_ BitVec 8) #x3b)
[GOOD] (define-fun s62 () (_ BitVec 8) #x3c)
[GOOD] (define-fun s63 () (_ BitVec 8) #x3d)
[GOOD] (define-fun s64 () (_ BitVec 8) #x3e)
[GOOD] (define-fun s65 () (_ BitVec 8) #x3f)
[GOOD] (define-fun s66 () (_ BitVec 8) #x40)
[GOOD] (define-fun s67 () (_ BitVec 8) #x41)
[GOOD] (define-fun s68 () (_ BitVec 8) #x42)
[GOOD] (define-fun s69 () (_ BitVec 8) #x43)
[GOOD] (define-fun s70 () (_ BitVec 8) #x44)
[GOOD] (define-fun s71 () (_ BitVec 8) #x45)
[GOOD] (define-fun s72 () (_ BitVec 8) #x46)
[GOOD] (define-fun s73 () (_ BitVec 8) #x47)
[GOOD] (define-fun s74 () (_ BitVec 8) #x48)
[GOOD] (define-fun s75 () (_ BitVec 8) #x49)
[GOOD] (define-fun s76 () (_ BitVec 8) #x4a)
[GOOD] (define-fun s77 () (_ BitVec 8) #x4b)
[GOOD] (define-fun s78 () (_ BitVec 8) #x4c)
[GOOD] (define-fun s79 () (_ BitVec 8) #x4d)
[GOOD] (define-fun s80 () (_ BitVec 8) #x4e)
[GOOD] (define-fun s81 () (_ BitVec 8) #x4f)
[GOOD] (define-fun s82 () (_ BitVec 8) #x50)
[GOOD] (define-fun s83 () (_ BitVec 8) #x51)
[GOOD] (define-fun s84 () (_ BitVec 8) #x52)
[GOOD] (define-fun s85 () (_ BitVec 8) #x53)
[GOOD] (define-fun s86 () (_ BitVec 8) #x54)
[GOOD] (define-fun s87 () (_ BitVec 8) #x55)
[GOOD] (define-fun s88 () (_ BitVec 8) #x56)
[GOOD] (define-fun s89 () (_ BitVec 8) #x57)
[GOOD] (define-fun s90 () (_ BitVec 8) #x58)
[GOOD] (define-fun s91 () (_ BitVec 8) #x59)
[GOOD] (define-fun s92 () (_ BitVec 8) #x5a)
[GOOD] (define-fun s93 () (_ BitVec 8) #x5b)
[GOOD] (define-fun s94 () (_ BitVec 8) #x5c)
[GOOD] (define-fun s95 () (_ BitVec 8) #x5d)
[GOOD] (define-fun s96 () (_ BitVec 8) #x5e)
[GOOD] (define-fun s97 () (_ BitVec 8) #x5f)
[GOOD] (define-fun s98 () (_ BitVec 8) #x60)
[GOOD] (define-fun s99 () (_ BitVec 8) #x61)
[GOOD] (define-fun s100 () (_ BitVec 8) #x62)
[GOOD] (define-fun s101 () (_ BitVec 8) #x63)
[GOOD] (define-fun s102 () (_ BitVec 8) #x64)
[GOOD] (define-fun s103 () (_ BitVec 8) #x65)
[GOOD] (define-fun s104 () (_ BitVec 8) #x66)
[GOOD] (define-fun s105 () (_ BitVec 8) #x67)
[GOOD] (define-fun s106 () (_ BitVec 8) #x68)
[GOOD] (define-fun s107 () (_ BitVec 8) #x69)
[GOOD] (define-fun s108 () (_ BitVec 8) #x6a)
[GOOD] (define-fun s109 () (_ BitVec 8) #x6b)
[GOOD] (define-fun s110 () (_ BitVec 8) #x6c)
[GOOD] (define-fun s111 () (_ BitVec 8) #x6d)
[GOOD] (define-fun s112 () (_ BitVec 8) #x6e)
[GOOD] (define-fun s113 () (_ BitVec 8) #x6f)
[GOOD] (define-fun s114 () (_ BitVec 8) #x70)
[GOOD] (define-fun s115 () (_ BitVec 8) #x71)
[GOOD] (define-fun s116 () (_ BitVec 8) #x72)
[GOOD] (define-fun s117 () (_ BitVec 8) #x73)
[GOOD] (define-fun s118 () (_ BitVec 8) #x74)
[GOOD] (define-fun s119 () (_ BitVec 8) #x75)
[GOOD] (define-fun s120 () (_ BitVec 8) #x76)
[GOOD] (define-fun s121 () (_ BitVec 8) #x77)
[GOOD] (define-fun s122 () (_ BitVec 8) #x78)
[GOOD] (define-fun s123 () (_ BitVec 8) #x79)
[GOOD] (define-fun s124 () (_ BitVec 8) #x7a)
[GOOD] (define-fun s125 () (_ BitVec 8) #x7b)
[GOOD] (define-fun s126 () (_ BitVec 8) #x7c)
[GOOD] (define-fun s127 () (_ BitVec 8) #x7d)
[GOOD] (define-fun s128 () (_ BitVec 8) #x7e)
[GOOD] (define-fun s129 () (_ BitVec 8) #x7f)
[GOOD] (define-fun s130 () (_ BitVec 8) #x80)
[GOOD] (define-fun s131 () (_ BitVec 8) #x81)
[GOOD] (define-fun s132 () (_ BitVec 8) #x82)
[GOOD] (define-fun s133 () (_ BitVec 8) #x83)
[GOOD] (define-fun s134 () (_ BitVec 8) #x84)
[GOOD] (define-fun s135 () (_ BitVec 8) #x85)
[GOOD] (define-fun s136 () (_ BitVec 8) #x86)
[GOOD] (define-fun s137 () (_ BitVec 8) #x87)
[GOOD] (define-fun s138 () (_ BitVec 8) #x88)
[GOOD] (define-fun s139 () (_ BitVec 8) #x89)
[GOOD] (define-fun s140 () (_ BitVec 8) #x8a)
[GOOD] (define-fun s141 () (_ BitVec 8) #x8b)
[GOOD] (define-fun s142 () (_ BitVec 8) #x8c)
[GOOD] (define-fun s143 () (_ BitVec 8) #x8d)
[GOOD] (define-fun s144 () (_ BitVec 8) #x8e)
[GOOD] (define-fun s145 () (_ BitVec 8) #x8f)
[GOOD] (define-fun s146 () (_ BitVec 8) #x90)
[GOOD] (define-fun s147 () (_ BitVec 8) #x91)
[GOOD] (define-fun s148 () (_ BitVec 8) #x92)
[GOOD] (define-fun s149 () (_ BitVec 8) #x93)
[GOOD] (define-fun s150 () (_ BitVec 8) #x94)
[GOOD] (define-fun s151 () (_ BitVec 8) #x95)
[GOOD] (define-fun s152 () (_ BitVec 8) #x96)
[GOOD] (define-fun s153 () (_ BitVec 8) #x97)
[GOOD] (define-fun s154 () (_ BitVec 8) #x98)
[GOOD] (define-fun s155 () (_ BitVec 8) #x99)
[GOOD] (define-fun s156 () (_ BitVec 8) #x9a)
[GOOD] (define-fun s157 () (_ BitVec 8) #x9b)
[GOOD] (define-fun s158 () (_ BitVec 8) #x9c)
[GOOD] (define-fun s159 () (_ BitVec 8) #x9d)
[GOOD] (define-fun s160 () (_ BitVec 8) #x9e)
[GOOD] (define-fun s161 () (_ BitVec 8) #x9f)
[GOOD] (define-fun s162 () (_ BitVec 8) #xa0)
[GOOD] (define-fun s163 () (_ BitVec 8) #xa1)
[GOOD] (define-fun s164 () (_ BitVec 8) #xa2)
[GOOD] (define-fun s165 () (_ BitVec 8) #xa3)
[GOOD] (define-fun s166 () (_ BitVec 8) #xa4)
[GOOD] (define-fun s167 () (_ BitVec 8) #xa5)
[GOOD] (define-fun s168 () (_ BitVec 8) #xa6)
[GOOD] (define-fun s169 () (_ BitVec 8) #xa7)
[GOOD] (define-fun s170 () (_ BitVec 8) #xa8)
[GOOD] (define-fun s171 () (_ BitVec 8) #xa9)
[GOOD] (define-fun s172 () (_ BitVec 8) #xaa)
[GOOD] (define-fun s173 () (_ BitVec 8) #xab)
[GOOD] (define-fun s174 () (_ BitVec 8) #xac)
[GOOD] (define-fun s175 () (_ BitVec 8) #xad)
[GOOD] (define-fun s176 () (_ BitVec 8) #xae)
[GOOD] (define-fun s177 () (_ BitVec 8) #xaf)
[GOOD] (define-fun s178 () (_ BitVec 8) #xb0)
[GOOD] (define-fun s179 () (_ BitVec 8) #xb1)
[GOOD] (define-fun s180 () (_ BitVec 8) #xb2)
[GOOD] (define-fun s181 () (_ BitVec 8) #xb3)
[GOOD] (define-fun s182 () (_ BitVec 8) #xb4)
[GOOD] (define-fun s183 () (_ BitVec 8) #xb5)
[GOOD] (define-fun s184 () (_ BitVec 8) #xb6)
[GOOD] (define-fun s185 () (_ BitVec 8) #xb7)
[GOOD] (define-fun s186 () (_ BitVec 8) #xb8)
[GOOD] (define-fun s187 () (_ BitVec 8) #xb9)
[GOOD] (define-fun s188 () (_ BitVec 8) #xba)
[GOOD] (define-fun s189 () (_ BitVec 8) #xbb)
[GOOD] (define-fun s190 () (_ BitVec 8) #xbc)
[GOOD] (define-fun s191 () (_ BitVec 8) #xbd)
[GOOD] (define-fun s192 () (_ BitVec 8) #xbe)
[GOOD] (define-fun s193 () (_ BitVec 8) #xbf)
[GOOD] (define-fun s194 () (_ BitVec 8) #xc0)
[GOOD] (define-fun s195 () (_ BitVec 8) #xc1)
[GOOD] (define-fun s196 () (_ BitVec 8) #xc2)
[GOOD] (define-fun s197 () (_ BitVec 8) #xc3)
[GOOD] (define-fun s198 () (_ BitVec 8) #xc4)
[GOOD] (define-fun s199 () (_ BitVec 8) #xc5)
[GOOD] (define-fun s200 () (_ BitVec 8) #xc6)
[GOOD] (define-fun s201 () (_ BitVec 8) #xc7)
[GOOD] (define-fun s202 () (_ BitVec 8) #xc8)
[GOOD] (define-fun s203 () (_ BitVec 8) #xc9)
[GOOD] (define-fun s204 () (_ BitVec 8) #xca)
[GOOD] (define-fun s205 () (_ BitVec 8) #xcb)
[GOOD] (define-fun s206 () (_ BitVec 8) #xcc)
[GOOD] (define-fun s207 () (_ BitVec 8) #xcd)
[GOOD] (define-fun s208 () (_ BitVec 8) #xce)
[GOOD] (define-fun s209 () (_ BitVec 8) #xcf)
[GOOD] (define-fun s210 () (_ BitVec 8) #xd0)
[GOOD] (define-fun s211 () (_ BitVec 8) #xd1)
[GOOD] (define-fun s212 () (_ BitVec 8) #xd2)
[GOOD] (define-fun s213 () (_ BitVec 8) #xd3)
[GOOD] (define-fun s214 () (_ BitVec 8) #xd4)
[GOOD] (define-fun s215 () (_ BitVec 8) #xd5)
[GOOD] (define-fun s216 () (_ BitVec 8) #xd6)
[GOOD] (define-fun s217 () (_ BitVec 8) #xd7)
[GOOD] (define-fun s218 () (_ BitVec 8) #xd8)
[GOOD] (define-fun s219 () (_ BitVec 8) #xd9)
[GOOD] (define-fun s220 () (_ BitVec 8) #xda)
[GOOD] (define-fun s221 () (_ BitVec 8) #xdb)
[GOOD] (define-fun s222 () (_ BitVec 8) #xdc)
[GOOD] (define-fun s223 () (_ BitVec 8) #xdd)
[GOOD] (define-fun s224 () (_ BitVec 8) #xde)
[GOOD] (define-fun s225 () (_ BitVec 8) #xdf)
[GOOD] (define-fun s226 () (_ BitVec 8) #xe0)
[GOOD] (define-fun s227 () (_ BitVec 8) #xe1)
[GOOD] (define-fun s228 () (_ BitVec 8) #xe2)
[GOOD] (define-fun s229 () (_ BitVec 8) #xe3)
[GOOD] (define-fun s230 () (_ BitVec 8) #xe4)
[GOOD] (define-fun s231 () (_ BitVec 8) #xe5)
[GOOD] (define-fun s232 () (_ BitVec 8) #xe6)
[GOOD] (define-fun s233 () (_ BitVec 8) #xe7)
[GOOD] (define-fun s234 () (_ BitVec 8) #xe8)
[GOOD] (define-fun s235 () (_ BitVec 8) #xe9)
[GOOD] (define-fun s236 () (_ BitVec 8) #xea)
[GOOD] (define-fun s237 () (_ BitVec 8) #xeb)
[GOOD] (define-fun s238 () (_ BitVec 8) #xec)
[GOOD] (define-fun s239 () (_ BitVec 8) #xed)
[GOOD] (define-fun s240 () (_ BitVec 8) #xee)
[GOOD] (define-fun s241 () (_ BitVec 8) #xef)
[GOOD] (define-fun s242 () (_ BitVec 8) #xf0)
[GOOD] (define-fun s243 () (_ BitVec 8) #xf1)
[GOOD] (define-fun s244 () (_ BitVec 8) #xf2)
[GOOD] (define-fun s245 () (_ BitVec 8) #xf3)
[GOOD] (define-fun s246 () (_ BitVec 8) #xf4)
[GOOD] (define-fun s247 () (_ BitVec 8) #xf5)
[GOOD] (define-fun s248 () (_ BitVec 8) #xf6)
[GOOD] (define-fun s249 () (_ BitVec 8) #xf7)
[GOOD] (define-fun s250 () (_ BitVec 8) #xf8)
[GOOD] (define-fun s251 () (_ BitVec 8) #xf9)
[GOOD] (define-fun s252 () (_ BitVec 8) #xfa)
[GOOD] (define-fun s253 () (_ BitVec 8) #xfb)
[GOOD] (define-fun s254 () (_ BitVec 8) #xfc)
[GOOD] (define-fun s255 () (_ BitVec 8) #xfd)
[GOOD] (define-fun s256 () (_ BitVec 8) #xfe)
[GOOD] (define-fun s257 () (_ BitVec 8) #xff)
[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
[GOOD] (define-fun table0_initializer_0 () Bool (= (table0 #x00) s2))
[GOOD] (define-fun table0_initializer_1 () Bool (= (table0 #x01) s3))
[GOOD] (define-fun table0_initializer_2 () Bool (= (table0 #x02) s4))
[GOOD] (define-fun table0_initializer_3 () Bool (= (table0 #x03) s5))
[GOOD] (define-fun table0_initializer_4 () Bool (= (table0 #x04) s6))
[GOOD] (define-fun table0_initializer_5 () Bool (= (table0 #x05) s7))
[GOOD] (define-fun table0_initializer_6 () Bool (= (table0 #x06) s8))
[GOOD] (define-fun table0_initializer_7 () Bool (= (table0 #x07) s9))
[GOOD] (define-fun table0_initializer_8 () Bool (= (table0 #x08) s10))
[GOOD] (define-fun table0_initializer_9 () Bool (= (table0 #x09) s11))
[GOOD] (define-fun table0_initializer_10 () Bool (= (table0 #x0a) s12))
[GOOD] (define-fun table0_initializer_11 () Bool (= (table0 #x0b) s13))
[GOOD] (define-fun table0_initializer_12 () Bool (= (table0 #x0c) s14))
[GOOD] (define-fun table0_initializer_13 () Bool (= (table0 #x0d) s15))
[GOOD] (define-fun table0_initializer_14 () Bool (= (table0 #x0e) s16))
[GOOD] (define-fun table0_initializer_15 () Bool (= (table0 #x0f) s17))
[GOOD] (define-fun table0_initializer_16 () Bool (= (table0 #x10) s18))
[GOOD] (define-fun table0_initializer_17 () Bool (= (table0 #x11) s19))
[GOOD] (define-fun table0_initializer_18 () Bool (= (table0 #x12) s20))
[GOOD] (define-fun table0_initializer_19 () Bool (= (table0 #x13) s21))
[GOOD] (define-fun table0_initializer_20 () Bool (= (table0 #x14) s22))
[GOOD] (define-fun table0_initializer_21 () Bool (= (table0 #x15) s23))
[GOOD] (define-fun table0_initializer_22 () Bool (= (table0 #x16) s24))
[GOOD] (define-fun table0_initializer_23 () Bool (= (table0 #x17) s25))
[GOOD] (define-fun table0_initializer_24 () Bool (= (table0 #x18) s26))
[GOOD] (define-fun table0_initializer_25 () Bool (= (table0 #x19) s27))
[GOOD] (define-fun table0_initializer_26 () Bool (= (table0 #x1a) s28))
[GOOD] (define-fun table0_initializer_27 () Bool (= (table0 #x1b) s29))
[GOOD] (define-fun table0_initializer_28 () Bool (= (table0 #x1c) s30))
[GOOD] (define-fun table0_initializer_29 () Bool (= (table0 #x1d) s31))
[GOOD] (define-fun table0_initializer_30 () Bool (= (table0 #x1e) s32))
[GOOD] (define-fun table0_initializer_31 () Bool (= (table0 #x1f) s33))
[GOOD] (define-fun table0_initializer_32 () Bool (= (table0 #x20) s34))
[GOOD] (define-fun table0_initializer_33 () Bool (= (table0 #x21) s35))
[GOOD] (define-fun table0_initializer_34 () Bool (= (table0 #x22) s36))
[GOOD] (define-fun table0_initializer_35 () Bool (= (table0 #x23) s37))
[GOOD] (define-fun table0_initializer_36 () Bool (= (table0 #x24) s38))
[GOOD] (define-fun table0_initializer_37 () Bool (= (table0 #x25) s39))
[GOOD] (define-fun table0_initializer_38 () Bool (= (table0 #x26) s40))
[GOOD] (define-fun table0_initializer_39 () Bool (= (table0 #x27) s41))
[GOOD] (define-fun table0_initializer_40 () Bool (= (table0 #x28) s42))
[GOOD] (define-fun table0_initializer_41 () Bool (= (table0 #x29) s43))
[GOOD] (define-fun table0_initializer_42 () Bool (= (table0 #x2a) s44))
[GOOD] (define-fun table0_initializer_43 () Bool (= (table0 #x2b) s45))
[GOOD] (define-fun table0_initializer_44 () Bool (= (table0 #x2c) s46))
[GOOD] (define-fun table0_initializer_45 () Bool (= (table0 #x2d) s47))
[GOOD] (define-fun table0_initializer_46 () Bool (= (table0 #x2e) s48))
[GOOD] (define-fun table0_initializer_47 () Bool (= (table0 #x2f) s49))
[GOOD] (define-fun table0_initializer_48 () Bool (= (table0 #x30) s50))
[GOOD] (define-fun table0_initializer_49 () Bool (= (table0 #x31) s51))
[GOOD] (define-fun table0_initializer_50 () Bool (= (table0 #x32) s52))
[GOOD] (define-fun table0_initializer_51 () Bool (= (table0 #x33) s53))
[GOOD] (define-fun table0_initializer_52 () Bool (= (table0 #x34) s54))
[GOOD] (define-fun table0_initializer_53 () Bool (= (table0 #x35) s55))
[GOOD] (define-fun table0_initializer_54 () Bool (= (table0 #x36) s56))
[GOOD] (define-fun table0_initializer_55 () Bool (= (table0 #x37) s57))
[GOOD] (define-fun table0_initializer_56 () Bool (= (table0 #x38) s58))
[GOOD] (define-fun table0_initializer_57 () Bool (= (table0 #x39) s59))
[GOOD] (define-fun table0_initializer_58 () Bool (= (table0 #x3a) s60))
[GOOD] (define-fun table0_initializer_59 () Bool (= (table0 #x3b) s61))
[GOOD] (define-fun table0_initializer_60 () Bool (= (table0 #x3c) s62))
[GOOD] (define-fun table0_initializer_61 () Bool (= (table0 #x3d) s63))
[GOOD] (define-fun table0_initializer_62 () Bool (= (table0 #x3e) s64))
[GOOD] (define-fun table0_initializer_63 () Bool (= (table0 #x3f) s65))
[GOOD] (define-fun table0_initializer_64 () Bool (= (table0 #x40) s66))
[GOOD] (define-fun table0_initializer_65 () Bool (= (table0 #x41) s67))
[GOOD] (define-fun table0_initializer_66 () Bool (= (table0 #x42) s68))
[GOOD] (define-fun table0_initializer_67 () Bool (= (table0 #x43) s69))
[GOOD] (define-fun table0_initializer_68 () Bool (= (table0 #x44) s70))
[GOOD] (define-fun table0_initializer_69 () Bool (= (table0 #x45) s71))
[GOOD] (define-fun table0_initializer_70 () Bool (= (table0 #x46) s72))
[GOOD] (define-fun table0_initializer_71 () Bool (= (table0 #x47) s73))
[GOOD] (define-fun table0_initializer_72 () Bool (= (table0 #x48) s74))
[GOOD] (define-fun table0_initializer_73 () Bool (= (table0 #x49) s75))
[GOOD] (define-fun table0_initializer_74 () Bool (= (table0 #x4a) s76))
[GOOD] (define-fun table0_initializer_75 () Bool (= (table0 #x4b) s77))
[GOOD] (define-fun table0_initializer_76 () Bool (= (table0 #x4c) s78))
[GOOD] (define-fun table0_initializer_77 () Bool (= (table0 #x4d) s79))
[GOOD] (define-fun table0_initializer_78 () Bool (= (table0 #x4e) s80))
[GOOD] (define-fun table0_initializer_79 () Bool (= (table0 #x4f) s81))
[GOOD] (define-fun table0_initializer_80 () Bool (= (table0 #x50) s82))
[GOOD] (define-fun table0_initializer_81 () Bool (= (table0 #x51) s83))
[GOOD] (define-fun table0_initializer_82 () Bool (= (table0 #x52) s84))
[GOOD] (define-fun table0_initializer_83 () Bool (= (table0 #x53) s85))
[GOOD] (define-fun table0_initializer_84 () Bool (= (table0 #x54) s86))
[GOOD] (define-fun table0_initializer_85 () Bool (= (table0 #x55) s87))
[GOOD] (define-fun table0_initializer_86 () Bool (= (table0 #x56) s88))
[GOOD] (define-fun table0_initializer_87 () Bool (= (table0 #x57) s89))
[GOOD] (define-fun table0_initializer_88 () Bool (= (table0 #x58) s90))
[GOOD] (define-fun table0_initializer_89 () Bool (= (table0 #x59) s91))
[GOOD] (define-fun table0_initializer_90 () Bool (= (table0 #x5a) s92))
[GOOD] (define-fun table0_initializer_91 () Bool (= (table0 #x5b) s93))
[GOOD] (define-fun table0_initializer_92 () Bool (= (table0 #x5c) s94))
[GOOD] (define-fun table0_initializer_93 () Bool (= (table0 #x5d) s95))
[GOOD] (define-fun table0_initializer_94 () Bool (= (table0 #x5e) s96))
[GOOD] (define-fun table0_initializer_95 () Bool (= (table0 #x5f) s97))
[GOOD] (define-fun table0_initializer_96 () Bool (= (table0 #x60) s98))
[GOOD] (define-fun table0_initializer_97 () Bool (= (table0 #x61) s99))
[GOOD] (define-fun table0_initializer_98 () Bool (= (table0 #x62) s100))
[GOOD] (define-fun table0_initializer_99 () Bool (= (table0 #x63) s101))
[GOOD] (define-fun table0_initializer_100 () Bool (= (table0 #x64) s102))
[GOOD] (define-fun table0_initializer_101 () Bool (= (table0 #x65) s103))
[GOOD] (define-fun table0_initializer_102 () Bool (= (table0 #x66) s104))
[GOOD] (define-fun table0_initializer_103 () Bool (= (table0 #x67) s105))
[GOOD] (define-fun table0_initializer_104 () Bool (= (table0 #x68) s106))
[GOOD] (define-fun table0_initializer_105 () Bool (= (table0 #x69) s107))
[GOOD] (define-fun table0_initializer_106 () Bool (= (table0 #x6a) s108))
[GOOD] (define-fun table0_initializer_107 () Bool (= (table0 #x6b) s109))
[GOOD] (define-fun table0_initializer_108 () Bool (= (table0 #x6c) s110))
[GOOD] (define-fun table0_initializer_109 () Bool (= (table0 #x6d) s111))
[GOOD] (define-fun table0_initializer_110 () Bool (= (table0 #x6e) s112))
[GOOD] (define-fun table0_initializer_111 () Bool (= (table0 #x6f) s113))
[GOOD] (define-fun table0_initializer_112 () Bool (= (table0 #x70) s114))
[GOOD] (define-fun table0_initializer_113 () Bool (= (table0 #x71) s115))
[GOOD] (define-fun table0_initializer_114 () Bool (= (table0 #x72) s116))
[GOOD] (define-fun table0_initializer_115 () Bool (= (table0 #x73) s117))
[GOOD] (define-fun table0_initializer_116 () Bool (= (table0 #x74) s118))
[GOOD] (define-fun table0_initializer_117 () Bool (= (table0 #x75) s119))
[GOOD] (define-fun table0_initializer_118 () Bool (= (table0 #x76) s120))
[GOOD] (define-fun table0_initializer_119 () Bool (= (table0 #x77) s121))
[GOOD] (define-fun table0_initializer_120 () Bool (= (table0 #x78) s122))
[GOOD] (define-fun table0_initializer_121 () Bool (= (table0 #x79) s123))
[GOOD] (define-fun table0_initializer_122 () Bool (= (table0 #x7a) s124))
[GOOD] (define-fun table0_initializer_123 () Bool (= (table0 #x7b) s125))
[GOOD] (define-fun table0_initializer_124 () Bool (= (table0 #x7c) s126))
[GOOD] (define-fun table0_initializer_125 () Bool (= (table0 #x7d) s127))
[GOOD] (define-fun table0_initializer_126 () Bool (= (table0 #x7e) s128))
[GOOD] (define-fun table0_initializer_127 () Bool (= (table0 #x7f) s129))
[GOOD] (define-fun table0_initializer_128 () Bool (= (table0 #x80) s130))
[GOOD] (define-fun table0_initializer_129 () Bool (= (table0 #x81) s131))
[GOOD] (define-fun table0_initializer_130 () Bool (= (table0 #x82) s132))
[GOOD] (define-fun table0_initializer_131 () Bool (= (table0 #x83) s133))
[GOOD] (define-fun table0_initializer_132 () Bool (= (table0 #x84) s134))
[GOOD] (define-fun table0_initializer_133 () Bool (= (table0 #x85) s135))
[GOOD] (define-fun table0_initializer_134 () Bool (= (table0 #x86) s136))
[GOOD] (define-fun table0_initializer_135 () Bool (= (table0 #x87) s137))
[GOOD] (define-fun table0_initializer_136 () Bool (= (table0 #x88) s138))
[GOOD] (define-fun table0_initializer_137 () Bool (= (table0 #x89) s139))
[GOOD] (define-fun table0_initializer_138 () Bool (= (table0 #x8a) s140))
[GOOD] (define-fun table0_initializer_139 () Bool (= (table0 #x8b) s141))
[GOOD] (define-fun table0_initializer_140 () Bool (= (table0 #x8c) s142))
[GOOD] (define-fun table0_initializer_141 () Bool (= (table0 #x8d) s143))
[GOOD] (define-fun table0_initializer_142 () Bool (= (table0 #x8e) s144))
[GOOD] (define-fun table0_initializer_143 () Bool (= (table0 #x8f) s145))
[GOOD] (define-fun table0_initializer_144 () Bool (= (table0 #x90) s146))
[GOOD] (define-fun table0_initializer_145 () Bool (= (table0 #x91) s147))
[GOOD] (define-fun table0_initializer_146 () Bool (= (table0 #x92) s148))
[GOOD] (define-fun table0_initializer_147 () Bool (= (table0 #x93) s149))
[GOOD] (define-fun table0_initializer_148 () Bool (= (table0 #x94) s150))
[GOOD] (define-fun table0_initializer_149 () Bool (= (table0 #x95) s151))
[GOOD] (define-fun table0_initializer_150 () Bool (= (table0 #x96) s152))
[GOOD] (define-fun table0_initializer_151 () Bool (= (table0 #x97) s153))
[GOOD] (define-fun table0_initializer_152 () Bool (= (table0 #x98) s154))
[GOOD] (define-fun table0_initializer_153 () Bool (= (table0 #x99) s155))
[GOOD] (define-fun table0_initializer_154 () Bool (= (table0 #x9a) s156))
[GOOD] (define-fun table0_initializer_155 () Bool (= (table0 #x9b) s157))
[GOOD] (define-fun table0_initializer_156 () Bool (= (table0 #x9c) s158))
[GOOD] (define-fun table0_initializer_157 () Bool (= (table0 #x9d) s159))
[GOOD] (define-fun table0_initializer_158 () Bool (= (table0 #x9e) s160))
[GOOD] (define-fun table0_initializer_159 () Bool (= (table0 #x9f) s161))
[GOOD] (define-fun table0_initializer_160 () Bool (= (table0 #xa0) s162))
[GOOD] (define-fun table0_initializer_161 () Bool (= (table0 #xa1) s163))
[GOOD] (define-fun table0_initializer_162 () Bool (= (table0 #xa2) s164))
[GOOD] (define-fun table0_initializer_163 () Bool (= (table0 #xa3) s165))
[GOOD] (define-fun table0_initializer_164 () Bool (= (table0 #xa4) s166))
[GOOD] (define-fun table0_initializer_165 () Bool (= (table0 #xa5) s167))
[GOOD] (define-fun table0_initializer_166 () Bool (= (table0 #xa6) s168))
[GOOD] (define-fun table0_initializer_167 () Bool (= (table0 #xa7) s169))
[GOOD] (define-fun table0_initializer_168 () Bool (= (table0 #xa8) s170))
[GOOD] (define-fun table0_initializer_169 () Bool (= (table0 #xa9) s171))
[GOOD] (define-fun table0_initializer_170 () Bool (= (table0 #xaa) s172))
[GOOD] (define-fun table0_initializer_171 () Bool (= (table0 #xab) s173))
[GOOD] (define-fun table0_initializer_172 () Bool (= (table0 #xac) s174))
[GOOD] (define-fun table0_initializer_173 () Bool (= (table0 #xad) s175))
[GOOD] (define-fun table0_initializer_174 () Bool (= (table0 #xae) s176))
[GOOD] (define-fun table0_initializer_175 () Bool (= (table0 #xaf) s177))
[GOOD] (define-fun table0_initializer_176 () Bool (= (table0 #xb0) s178))
[GOOD] (define-fun table0_initializer_177 () Bool (= (table0 #xb1) s179))
[GOOD] (define-fun table0_initializer_178 () Bool (= (table0 #xb2) s180))
[GOOD] (define-fun table0_initializer_179 () Bool (= (table0 #xb3) s181))
[GOOD] (define-fun table0_initializer_180 () Bool (= (table0 #xb4) s182))
[GOOD] (define-fun table0_initializer_181 () Bool (= (table0 #xb5) s183))
[GOOD] (define-fun table0_initializer_182 () Bool (= (table0 #xb6) s184))
[GOOD] (define-fun table0_initializer_183 () Bool (= (table0 #xb7) s185))
[GOOD] (define-fun table0_initializer_184 () Bool (= (table0 #xb8) s186))
[GOOD] (define-fun table0_initializer_185 () Bool (= (table0 #xb9) s187))
[GOOD] (define-fun table0_initializer_186 () Bool (= (table0 #xba) s188))
[GOOD] (define-fun table0_initializer_187 () Bool (= (table0 #xbb) s189))
[GOOD] (define-fun table0_initializer_188 () Bool (= (table0 #xbc) s190))
[GOOD] (define-fun table0_initializer_189 () Bool (= (table0 #xbd) s191))
[GOOD] (define-fun table0_initializer_190 () Bool (= (table0 #xbe) s192))
[GOOD] (define-fun table0_initializer_191 () Bool (= (table0 #xbf) s193))
[GOOD] (define-fun table0_initializer_192 () Bool (= (table0 #xc0) s194))
[GOOD] (define-fun table0_initializer_193 () Bool (= (table0 #xc1) s195))
[GOOD] (define-fun table0_initializer_194 () Bool (= (table0 #xc2) s196))
[GOOD] (define-fun table0_initializer_195 () Bool (= (table0 #xc3) s197))
[GOOD] (define-fun table0_initializer_196 () Bool (= (table0 #xc4) s198))
[GOOD] (define-fun table0_initializer_197 () Bool (= (table0 #xc5) s199))
[GOOD] (define-fun table0_initializer_198 () Bool (= (table0 #xc6) s200))
[GOOD] (define-fun table0_initializer_199 () Bool (= (table0 #xc7) s201))
[GOOD] (define-fun table0_initializer_200 () Bool (= (table0 #xc8) s202))
[GOOD] (define-fun table0_initializer_201 () Bool (= (table0 #xc9) s203))
[GOOD] (define-fun table0_initializer_202 () Bool (= (table0 #xca) s204))
[GOOD] (define-fun table0_initializer_203 () Bool (= (table0 #xcb) s205))
[GOOD] (define-fun table0_initializer_204 () Bool (= (table0 #xcc) s206))
[GOOD] (define-fun table0_initializer_205 () Bool (= (table0 #xcd) s207))
[GOOD] (define-fun table0_initializer_206 () Bool (= (table0 #xce) s208))
[GOOD] (define-fun table0_initializer_207 () Bool (= (table0 #xcf) s209))
[GOOD] (define-fun table0_initializer_208 () Bool (= (table0 #xd0) s210))
[GOOD] (define-fun table0_initializer_209 () Bool (= (table0 #xd1) s211))
[GOOD] (define-fun table0_initializer_210 () Bool (= (table0 #xd2) s212))
[GOOD] (define-fun table0_initializer_211 () Bool (= (table0 #xd3) s213))
[GOOD] (define-fun table0_initializer_212 () Bool (= (table0 #xd4) s214))
[GOOD] (define-fun table0_initializer_213 () Bool (= (table0 #xd5) s215))
[GOOD] (define-fun table0_initializer_214 () Bool (= (table0 #xd6) s216))
[GOOD] (define-fun table0_initializer_215 () Bool (= (table0 #xd7) s217))
[GOOD] (define-fun table0_initializer_216 () Bool (= (table0 #xd8) s218))
[GOOD] (define-fun table0_initializer_217 () Bool (= (table0 #xd9) s219))
[GOOD] (define-fun table0_initializer_218 () Bool (= (table0 #xda) s220))
[GOOD] (define-fun table0_initializer_219 () Bool (= (table0 #xdb) s221))
[GOOD] (define-fun table0_initializer_220 () Bool (= (table0 #xdc) s222))
[GOOD] (define-fun table0_initializer_221 () Bool (= (table0 #xdd) s223))
[GOOD] (define-fun table0_initializer_222 () Bool (= (table0 #xde) s224))
[GOOD] (define-fun table0_initializer_223 () Bool (= (table0 #xdf) s225))
[GOOD] (define-fun table0_initializer_224 () Bool (= (table0 #xe0) s226))
[GOOD] (define-fun table0_initializer_225 () Bool (= (table0 #xe1) s227))
[GOOD] (define-fun table0_initializer_226 () Bool (= (table0 #xe2) s228))
[GOOD] (define-fun table0_initializer_227 () Bool (= (table0 #xe3) s229))
[GOOD] (define-fun table0_initializer_228 () Bool (= (table0 #xe4) s230))
[GOOD] (define-fun table0_initializer_229 () Bool (= (table0 #xe5) s231))
[GOOD] (define-fun table0_initializer_230 () Bool (= (table0 #xe6) s232))
[GOOD] (define-fun table0_initializer_231 () Bool (= (table0 #xe7) s233))
[GOOD] (define-fun table0_initializer_232 () Bool (= (table0 #xe8) s234))
[GOOD] (define-fun table0_initializer_233 () Bool (= (table0 #xe9) s235))
[GOOD] (define-fun table0_initializer_234 () Bool (= (table0 #xea) s236))
[GOOD] (define-fun table0_initializer_235 () Bool (= (table0 #xeb) s237))
[GOOD] (define-fun table0_initializer_236 () Bool (= (table0 #xec) s238))
[GOOD] (define-fun table0_initializer_237 () Bool (= (table0 #xed) s239))
[GOOD] (define-fun table0_initializer_238 () Bool (= (table0 #xee) s240))
[GOOD] (define-fun table0_initializer_239 () Bool (= (table0 #xef) s241))
[GOOD] (define-fun table0_initializer_240 () Bool (= (table0 #xf0) s242))
[GOOD] (define-fun table0_initializer_241 () Bool (= (table0 #xf1) s243))
[GOOD] (define-fun table0_initializer_242 () Bool (= (table0 #xf2) s244))
[GOOD] (define-fun table0_initializer_243 () Bool (= (table0 #xf3) s245))
[GOOD] (define-fun table0_initializer_244 () Bool (= (table0 #xf4) s246))
[GOOD] (define-fun table0_initializer_245 () Bool (= (table0 #xf5) s247))
[GOOD] (define-fun table0_initializer_246 () Bool (= (table0 #xf6) s248))
[GOOD] (define-fun table0_initializer_247 () Bool (= (table0 #xf7) s249))
[GOOD] (define-fun table0_initializer_248 () Bool (= (table0 #xf8) s250))
[GOOD] (define-fun table0_initializer_249 () Bool (= (table0 #xf9) s251))
[GOOD] (define-fun table0_initializer_250 () Bool (= (table0 #xfa) s252))
[GOOD] (define-fun table0_initializer_251 () Bool (= (table0 #xfb) s253))
[GOOD] (define-fun table0_initializer_252 () Bool (= (table0 #xfc) s254))
[GOOD] (define-fun table0_initializer_253 () Bool (= (table0 #xfd) s255))
[GOOD] (define-fun table0_initializer_254 () Bool (= (table0 #xfe) s256))
[GOOD] (define-fun table0_initializer_255 () Bool (= (table0 #xff) s257))
[GOOD] (define-fun table0_initializer () Bool (and table0_initializer_0 table0_initializer_1 table0_initializer_2 table0_initializer_3 table0_initializer_4 table0_initializer_5 table0_initializer_6 table0_initializer_7 table0_initializer_8 table0_initializer_9 table0_initializer_10 table0_initializer_11 table0_initializer_12 table0_initializer_13 table0_initializer_14 table0_initializer_15 table0_initializer_16 table0_initializer_17 table0_initializer_18 table0_initializer_19 table0_initializer_20 table0_initializer_21 table0_initializer_22 table0_initializer_23 table0_initializer_24 table0_initializer_25 table0_initializer_26 table0_initializer_27 table0_initializer_28 table0_initializer_29 table0_initializer_30 table0_initializer_31 table0_initializer_32 table0_initializer_33 table0_initializer_34 table0_initializer_35 table0_initializer_36 table0_initializer_37 table0_initializer_38 table0_initializer_39 table0_initializer_40 table0_initializer_41 table0_initializer_42 table0_initializer_43 table0_initializer_44 table0_initializer_45 table0_initializer_46 table0_initializer_47 table0_initializer_48 table0_initializer_49 table0_initializer_50 table0_initializer_51 table0_initializer_52 table0_initializer_53 table0_initializer_54 table0_initializer_55 table0_initializer_56 table0_initializer_57 table0_initializer_58 table0_initializer_59 table0_initializer_60 table0_initializer_61 table0_initializer_62 table0_initializer_63 table0_initializer_64 table0_initializer_65 table0_initializer_66 table0_initializer_67 table0_initializer_68 table0_initializer_69 table0_initializer_70 table0_initializer_71 table0_initializer_72 table0_initializer_73 table0_initializer_74 table0_initializer_75 table0_initializer_76 table0_initializer_77 table0_initializer_78 table0_initializer_79 table0_initializer_80 table0_initializer_81 table0_initializer_82 table0_initializer_83 table0_initializer_84 table0_initializer_85 table0_initializer_86 table0_initializer_87 table0_initializer_88 table0_initializer_89 table0_initializer_90 table0_initializer_91 table0_initializer_92 table0_initializer_93 table0_initializer_94 table0_initializer_95 table0_initializer_96 table0_initializer_97 table0_initializer_98 table0_initializer_99 table0_initializer_100 table0_initializer_101 table0_initializer_102 table0_initializer_103 table0_initializer_104 table0_initializer_105 table0_initializer_106 table0_initializer_107 table0_initializer_108 table0_initializer_109 table0_initializer_110 table0_initializer_111 table0_initializer_112 table0_initializer_113 table0_initializer_114 table0_initializer_115 table0_initializer_116 table0_initializer_117 table0_initializer_118 table0_initializer_119 table0_initializer_120 table0_initializer_121 table0_initializer_122 table0_initializer_123 table0_initializer_124 table0_initializer_125 table0_initializer_126 table0_initializer_127 table0_initializer_128 table0_initializer_129 table0_initializer_130 table0_initializer_131 table0_initializer_132 table0_initializer_133 table0_initializer_134 table0_initializer_135 table0_initializer_136 table0_initializer_137 table0_initializer_138 table0_initializer_139 table0_initializer_140 table0_initializer_141 table0_initializer_142 table0_initializer_143 table0_initializer_144 table0_initializer_145 table0_initializer_146 table0_initializer_147 table0_initializer_148 table0_initializer_149 table0_initializer_150 table0_initializer_151 table0_initializer_152 table0_initializer_153 table0_initializer_154 table0_initializer_155 table0_initializer_156 table0_initializer_157 table0_initializer_158 table0_initializer_159 table0_initializer_160 table0_initializer_161 table0_initializer_162 table0_initializer_163 table0_initializer_164 table0_initializer_165 table0_initializer_166 table0_initializer_167 table0_initializer_168 table0_initializer_169 table0_initializer_170 table0_initializer_171 table0_initializer_172 table0_initializer_173 table0_initializer_174 table0_initializer_175 table0_initializer_176 table0_initializer_177 table0_initializer_178 table0_initializer_179 table0_initializer_180 table0_initializer_181 table0_initializer_182 table0_initializer_183 table0_initializer_184 table0_initializer_185 table0_initializer_186 table0_initializer_187 table0_initializer_188 table0_initializer_189 table0_initializer_190 table0_initializer_191 table0_initializer_192 table0_initializer_193 table0_initializer_194 table0_initializer_195 table0_initializer_196 table0_initializer_197 table0_initializer_198 table0_initializer_199 table0_initializer_200 table0_initializer_201 table0_initializer_202 table0_initializer_203 table0_initializer_204 table0_initializer_205 table0_initializer_206 table0_initializer_207 table0_initializer_208 table0_initializer_209 table0_initializer_210 table0_initializer_211 table0_initializer_212 table0_initializer_213 table0_initializer_214 table0_initializer_215 table0_initializer_216 table0_initializer_217 table0_initializer_218 table0_initializer_219 table0_initializer_220 table0_initializer_221 table0_initializer_222 table0_initializer_223 table0_initializer_224 table0_initializer_225 table0_initializer_226 table0_initializer_227 table0_initializer_228 table0_initializer_229 table0_initializer_230 table0_initializer_231 table0_initializer_232 table0_initializer_233 table0_initializer_234 table0_initializer_235 table0_initializer_236 table0_initializer_237 table0_initializer_238 table0_initializer_239 table0_initializer_240 table0_initializer_241 table0_initializer_242 table0_initializer_243 table0_initializer_244 table0_initializer_245 table0_initializer_246 table0_initializer_247 table0_initializer_248 table0_initializer_249 table0_initializer_250 table0_initializer_251 table0_initializer_252 table0_initializer_253 table0_initializer_254 table0_initializer_255))
[GOOD] (assert table0_initializer)
[GOOD] (define-fun s258 () (_ BitVec 8) (table0 s0))
[GOOD] (define-fun s259 () Bool (= s0 s258))
[GOOD] (assert s259)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 #x00))
[GOOD] (define-fun s260 () (_ BitVec 8) (table0 s1))
[GOOD] (define-fun s261 () Bool (= s1 s260))
[GOOD] (assert s261)
[GOOD] (define-fun s262 () (_ BitVec 8) (bvadd s0 s3))
[GOOD] (define-fun s263 () Bool (= s1 s262))
[GOOD] (assert s263)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s1))
[RECV] ((s1 #x01))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:(0,1)
DONE!