** 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] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s1 () (_ BitVec 8) #x00)
[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
[GOOD] (define-fun table0_initializer_0 () Bool (= (table0 #x00) s0))
[GOOD] (define-fun table0_initializer_1 () Bool (= (table0 #x01) s0))
[GOOD] (define-fun table0_initializer_2 () Bool (= (table0 #x02) s0))
[GOOD] (define-fun table0_initializer_3 () Bool (= (table0 #x03) s0))
[GOOD] (define-fun table0_initializer_4 () Bool (= (table0 #x04) s0))
[GOOD] (define-fun table0_initializer_5 () Bool (= (table0 #x05) s0))
[GOOD] (define-fun table0_initializer_6 () Bool (= (table0 #x06) s0))
[GOOD] (define-fun table0_initializer_7 () Bool (= (table0 #x07) s0))
[GOOD] (define-fun table0_initializer_8 () Bool (= (table0 #x08) s0))
[GOOD] (define-fun table0_initializer_9 () Bool (= (table0 #x09) s0))
[GOOD] (define-fun table0_initializer_10 () Bool (= (table0 #x0a) s0))
[GOOD] (define-fun table0_initializer_11 () Bool (= (table0 #x0b) s0))
[GOOD] (define-fun table0_initializer_12 () Bool (= (table0 #x0c) s0))
[GOOD] (define-fun table0_initializer_13 () Bool (= (table0 #x0d) s0))
[GOOD] (define-fun table0_initializer_14 () Bool (= (table0 #x0e) s0))
[GOOD] (define-fun table0_initializer_15 () Bool (= (table0 #x0f) s0))
[GOOD] (define-fun table0_initializer_16 () Bool (= (table0 #x10) s0))
[GOOD] (define-fun table0_initializer_17 () Bool (= (table0 #x11) s0))
[GOOD] (define-fun table0_initializer_18 () Bool (= (table0 #x12) s0))
[GOOD] (define-fun table0_initializer_19 () Bool (= (table0 #x13) s0))
[GOOD] (define-fun table0_initializer_20 () Bool (= (table0 #x14) s0))
[GOOD] (define-fun table0_initializer_21 () Bool (= (table0 #x15) s0))
[GOOD] (define-fun table0_initializer_22 () Bool (= (table0 #x16) s0))
[GOOD] (define-fun table0_initializer_23 () Bool (= (table0 #x17) s0))
[GOOD] (define-fun table0_initializer_24 () Bool (= (table0 #x18) s0))
[GOOD] (define-fun table0_initializer_25 () Bool (= (table0 #x19) s0))
[GOOD] (define-fun table0_initializer_26 () Bool (= (table0 #x1a) s0))
[GOOD] (define-fun table0_initializer_27 () Bool (= (table0 #x1b) s0))
[GOOD] (define-fun table0_initializer_28 () Bool (= (table0 #x1c) s0))
[GOOD] (define-fun table0_initializer_29 () Bool (= (table0 #x1d) s0))
[GOOD] (define-fun table0_initializer_30 () Bool (= (table0 #x1e) s0))
[GOOD] (define-fun table0_initializer_31 () Bool (= (table0 #x1f) s0))
[GOOD] (define-fun table0_initializer_32 () Bool (= (table0 #x20) s0))
[GOOD] (define-fun table0_initializer_33 () Bool (= (table0 #x21) s0))
[GOOD] (define-fun table0_initializer_34 () Bool (= (table0 #x22) s0))
[GOOD] (define-fun table0_initializer_35 () Bool (= (table0 #x23) s0))
[GOOD] (define-fun table0_initializer_36 () Bool (= (table0 #x24) s0))
[GOOD] (define-fun table0_initializer_37 () Bool (= (table0 #x25) s0))
[GOOD] (define-fun table0_initializer_38 () Bool (= (table0 #x26) s0))
[GOOD] (define-fun table0_initializer_39 () Bool (= (table0 #x27) s0))
[GOOD] (define-fun table0_initializer_40 () Bool (= (table0 #x28) s0))
[GOOD] (define-fun table0_initializer_41 () Bool (= (table0 #x29) s0))
[GOOD] (define-fun table0_initializer_42 () Bool (= (table0 #x2a) s0))
[GOOD] (define-fun table0_initializer_43 () Bool (= (table0 #x2b) s0))
[GOOD] (define-fun table0_initializer_44 () Bool (= (table0 #x2c) s0))
[GOOD] (define-fun table0_initializer_45 () Bool (= (table0 #x2d) s0))
[GOOD] (define-fun table0_initializer_46 () Bool (= (table0 #x2e) s0))
[GOOD] (define-fun table0_initializer_47 () Bool (= (table0 #x2f) s0))
[GOOD] (define-fun table0_initializer_48 () Bool (= (table0 #x30) s0))
[GOOD] (define-fun table0_initializer_49 () Bool (= (table0 #x31) s0))
[GOOD] (define-fun table0_initializer_50 () Bool (= (table0 #x32) s0))
[GOOD] (define-fun table0_initializer_51 () Bool (= (table0 #x33) s0))
[GOOD] (define-fun table0_initializer_52 () Bool (= (table0 #x34) s0))
[GOOD] (define-fun table0_initializer_53 () Bool (= (table0 #x35) s0))
[GOOD] (define-fun table0_initializer_54 () Bool (= (table0 #x36) s0))
[GOOD] (define-fun table0_initializer_55 () Bool (= (table0 #x37) s0))
[GOOD] (define-fun table0_initializer_56 () Bool (= (table0 #x38) s0))
[GOOD] (define-fun table0_initializer_57 () Bool (= (table0 #x39) s0))
[GOOD] (define-fun table0_initializer_58 () Bool (= (table0 #x3a) s0))
[GOOD] (define-fun table0_initializer_59 () Bool (= (table0 #x3b) s0))
[GOOD] (define-fun table0_initializer_60 () Bool (= (table0 #x3c) s0))
[GOOD] (define-fun table0_initializer_61 () Bool (= (table0 #x3d) s0))
[GOOD] (define-fun table0_initializer_62 () Bool (= (table0 #x3e) s0))
[GOOD] (define-fun table0_initializer_63 () Bool (= (table0 #x3f) s0))
[GOOD] (define-fun table0_initializer_64 () Bool (= (table0 #x40) s0))
[GOOD] (define-fun table0_initializer_65 () Bool (= (table0 #x41) s0))
[GOOD] (define-fun table0_initializer_66 () Bool (= (table0 #x42) s0))
[GOOD] (define-fun table0_initializer_67 () Bool (= (table0 #x43) s0))
[GOOD] (define-fun table0_initializer_68 () Bool (= (table0 #x44) s0))
[GOOD] (define-fun table0_initializer_69 () Bool (= (table0 #x45) s0))
[GOOD] (define-fun table0_initializer_70 () Bool (= (table0 #x46) s0))
[GOOD] (define-fun table0_initializer_71 () Bool (= (table0 #x47) s0))
[GOOD] (define-fun table0_initializer_72 () Bool (= (table0 #x48) s0))
[GOOD] (define-fun table0_initializer_73 () Bool (= (table0 #x49) s0))
[GOOD] (define-fun table0_initializer_74 () Bool (= (table0 #x4a) s0))
[GOOD] (define-fun table0_initializer_75 () Bool (= (table0 #x4b) s0))
[GOOD] (define-fun table0_initializer_76 () Bool (= (table0 #x4c) s0))
[GOOD] (define-fun table0_initializer_77 () Bool (= (table0 #x4d) s0))
[GOOD] (define-fun table0_initializer_78 () Bool (= (table0 #x4e) s0))
[GOOD] (define-fun table0_initializer_79 () Bool (= (table0 #x4f) s0))
[GOOD] (define-fun table0_initializer_80 () Bool (= (table0 #x50) s0))
[GOOD] (define-fun table0_initializer_81 () Bool (= (table0 #x51) s0))
[GOOD] (define-fun table0_initializer_82 () Bool (= (table0 #x52) s0))
[GOOD] (define-fun table0_initializer_83 () Bool (= (table0 #x53) s0))
[GOOD] (define-fun table0_initializer_84 () Bool (= (table0 #x54) s0))
[GOOD] (define-fun table0_initializer_85 () Bool (= (table0 #x55) s0))
[GOOD] (define-fun table0_initializer_86 () Bool (= (table0 #x56) s0))
[GOOD] (define-fun table0_initializer_87 () Bool (= (table0 #x57) s0))
[GOOD] (define-fun table0_initializer_88 () Bool (= (table0 #x58) s0))
[GOOD] (define-fun table0_initializer_89 () Bool (= (table0 #x59) s0))
[GOOD] (define-fun table0_initializer_90 () Bool (= (table0 #x5a) s0))
[GOOD] (define-fun table0_initializer_91 () Bool (= (table0 #x5b) s0))
[GOOD] (define-fun table0_initializer_92 () Bool (= (table0 #x5c) s0))
[GOOD] (define-fun table0_initializer_93 () Bool (= (table0 #x5d) s0))
[GOOD] (define-fun table0_initializer_94 () Bool (= (table0 #x5e) s0))
[GOOD] (define-fun table0_initializer_95 () Bool (= (table0 #x5f) s0))
[GOOD] (define-fun table0_initializer_96 () Bool (= (table0 #x60) s0))
[GOOD] (define-fun table0_initializer_97 () Bool (= (table0 #x61) s0))
[GOOD] (define-fun table0_initializer_98 () Bool (= (table0 #x62) s0))
[GOOD] (define-fun table0_initializer_99 () Bool (= (table0 #x63) s0))
[GOOD] (define-fun table0_initializer_100 () Bool (= (table0 #x64) s0))
[GOOD] (define-fun table0_initializer_101 () Bool (= (table0 #x65) s0))
[GOOD] (define-fun table0_initializer_102 () Bool (= (table0 #x66) s0))
[GOOD] (define-fun table0_initializer_103 () Bool (= (table0 #x67) s0))
[GOOD] (define-fun table0_initializer_104 () Bool (= (table0 #x68) s0))
[GOOD] (define-fun table0_initializer_105 () Bool (= (table0 #x69) s0))
[GOOD] (define-fun table0_initializer_106 () Bool (= (table0 #x6a) s0))
[GOOD] (define-fun table0_initializer_107 () Bool (= (table0 #x6b) s0))
[GOOD] (define-fun table0_initializer_108 () Bool (= (table0 #x6c) s0))
[GOOD] (define-fun table0_initializer_109 () Bool (= (table0 #x6d) s0))
[GOOD] (define-fun table0_initializer_110 () Bool (= (table0 #x6e) s0))
[GOOD] (define-fun table0_initializer_111 () Bool (= (table0 #x6f) s0))
[GOOD] (define-fun table0_initializer_112 () Bool (= (table0 #x70) s0))
[GOOD] (define-fun table0_initializer_113 () Bool (= (table0 #x71) s0))
[GOOD] (define-fun table0_initializer_114 () Bool (= (table0 #x72) s0))
[GOOD] (define-fun table0_initializer_115 () Bool (= (table0 #x73) s0))
[GOOD] (define-fun table0_initializer_116 () Bool (= (table0 #x74) s0))
[GOOD] (define-fun table0_initializer_117 () Bool (= (table0 #x75) s0))
[GOOD] (define-fun table0_initializer_118 () Bool (= (table0 #x76) s0))
[GOOD] (define-fun table0_initializer_119 () Bool (= (table0 #x77) s0))
[GOOD] (define-fun table0_initializer_120 () Bool (= (table0 #x78) s0))
[GOOD] (define-fun table0_initializer_121 () Bool (= (table0 #x79) s0))
[GOOD] (define-fun table0_initializer_122 () Bool (= (table0 #x7a) s0))
[GOOD] (define-fun table0_initializer_123 () Bool (= (table0 #x7b) s0))
[GOOD] (define-fun table0_initializer_124 () Bool (= (table0 #x7c) s0))
[GOOD] (define-fun table0_initializer_125 () Bool (= (table0 #x7d) s0))
[GOOD] (define-fun table0_initializer_126 () Bool (= (table0 #x7e) s0))
[GOOD] (define-fun table0_initializer_127 () Bool (= (table0 #x7f) s0))
[GOOD] (define-fun table0_initializer_128 () Bool (= (table0 #x80) s0))
[GOOD] (define-fun table0_initializer_129 () Bool (= (table0 #x81) s0))
[GOOD] (define-fun table0_initializer_130 () Bool (= (table0 #x82) s0))
[GOOD] (define-fun table0_initializer_131 () Bool (= (table0 #x83) s0))
[GOOD] (define-fun table0_initializer_132 () Bool (= (table0 #x84) s0))
[GOOD] (define-fun table0_initializer_133 () Bool (= (table0 #x85) s0))
[GOOD] (define-fun table0_initializer_134 () Bool (= (table0 #x86) s0))
[GOOD] (define-fun table0_initializer_135 () Bool (= (table0 #x87) s0))
[GOOD] (define-fun table0_initializer_136 () Bool (= (table0 #x88) s0))
[GOOD] (define-fun table0_initializer_137 () Bool (= (table0 #x89) s0))
[GOOD] (define-fun table0_initializer_138 () Bool (= (table0 #x8a) s0))
[GOOD] (define-fun table0_initializer_139 () Bool (= (table0 #x8b) s0))
[GOOD] (define-fun table0_initializer_140 () Bool (= (table0 #x8c) s0))
[GOOD] (define-fun table0_initializer_141 () Bool (= (table0 #x8d) s0))
[GOOD] (define-fun table0_initializer_142 () Bool (= (table0 #x8e) s0))
[GOOD] (define-fun table0_initializer_143 () Bool (= (table0 #x8f) s0))
[GOOD] (define-fun table0_initializer_144 () Bool (= (table0 #x90) s0))
[GOOD] (define-fun table0_initializer_145 () Bool (= (table0 #x91) s0))
[GOOD] (define-fun table0_initializer_146 () Bool (= (table0 #x92) s0))
[GOOD] (define-fun table0_initializer_147 () Bool (= (table0 #x93) s0))
[GOOD] (define-fun table0_initializer_148 () Bool (= (table0 #x94) s0))
[GOOD] (define-fun table0_initializer_149 () Bool (= (table0 #x95) s0))
[GOOD] (define-fun table0_initializer_150 () Bool (= (table0 #x96) s0))
[GOOD] (define-fun table0_initializer_151 () Bool (= (table0 #x97) s0))
[GOOD] (define-fun table0_initializer_152 () Bool (= (table0 #x98) s0))
[GOOD] (define-fun table0_initializer_153 () Bool (= (table0 #x99) s0))
[GOOD] (define-fun table0_initializer_154 () Bool (= (table0 #x9a) s0))
[GOOD] (define-fun table0_initializer_155 () Bool (= (table0 #x9b) s0))
[GOOD] (define-fun table0_initializer_156 () Bool (= (table0 #x9c) s0))
[GOOD] (define-fun table0_initializer_157 () Bool (= (table0 #x9d) s0))
[GOOD] (define-fun table0_initializer_158 () Bool (= (table0 #x9e) s0))
[GOOD] (define-fun table0_initializer_159 () Bool (= (table0 #x9f) s0))
[GOOD] (define-fun table0_initializer_160 () Bool (= (table0 #xa0) s0))
[GOOD] (define-fun table0_initializer_161 () Bool (= (table0 #xa1) s0))
[GOOD] (define-fun table0_initializer_162 () Bool (= (table0 #xa2) s0))
[GOOD] (define-fun table0_initializer_163 () Bool (= (table0 #xa3) s0))
[GOOD] (define-fun table0_initializer_164 () Bool (= (table0 #xa4) s0))
[GOOD] (define-fun table0_initializer_165 () Bool (= (table0 #xa5) s0))
[GOOD] (define-fun table0_initializer_166 () Bool (= (table0 #xa6) s0))
[GOOD] (define-fun table0_initializer_167 () Bool (= (table0 #xa7) s0))
[GOOD] (define-fun table0_initializer_168 () Bool (= (table0 #xa8) s0))
[GOOD] (define-fun table0_initializer_169 () Bool (= (table0 #xa9) s0))
[GOOD] (define-fun table0_initializer_170 () Bool (= (table0 #xaa) s0))
[GOOD] (define-fun table0_initializer_171 () Bool (= (table0 #xab) s0))
[GOOD] (define-fun table0_initializer_172 () Bool (= (table0 #xac) s0))
[GOOD] (define-fun table0_initializer_173 () Bool (= (table0 #xad) s0))
[GOOD] (define-fun table0_initializer_174 () Bool (= (table0 #xae) s0))
[GOOD] (define-fun table0_initializer_175 () Bool (= (table0 #xaf) s0))
[GOOD] (define-fun table0_initializer_176 () Bool (= (table0 #xb0) s0))
[GOOD] (define-fun table0_initializer_177 () Bool (= (table0 #xb1) s0))
[GOOD] (define-fun table0_initializer_178 () Bool (= (table0 #xb2) s0))
[GOOD] (define-fun table0_initializer_179 () Bool (= (table0 #xb3) s0))
[GOOD] (define-fun table0_initializer_180 () Bool (= (table0 #xb4) s0))
[GOOD] (define-fun table0_initializer_181 () Bool (= (table0 #xb5) s0))
[GOOD] (define-fun table0_initializer_182 () Bool (= (table0 #xb6) s0))
[GOOD] (define-fun table0_initializer_183 () Bool (= (table0 #xb7) s0))
[GOOD] (define-fun table0_initializer_184 () Bool (= (table0 #xb8) s0))
[GOOD] (define-fun table0_initializer_185 () Bool (= (table0 #xb9) s0))
[GOOD] (define-fun table0_initializer_186 () Bool (= (table0 #xba) s0))
[GOOD] (define-fun table0_initializer_187 () Bool (= (table0 #xbb) s0))
[GOOD] (define-fun table0_initializer_188 () Bool (= (table0 #xbc) s0))
[GOOD] (define-fun table0_initializer_189 () Bool (= (table0 #xbd) s0))
[GOOD] (define-fun table0_initializer_190 () Bool (= (table0 #xbe) s0))
[GOOD] (define-fun table0_initializer_191 () Bool (= (table0 #xbf) s0))
[GOOD] (define-fun table0_initializer_192 () Bool (= (table0 #xc0) s0))
[GOOD] (define-fun table0_initializer_193 () Bool (= (table0 #xc1) s0))
[GOOD] (define-fun table0_initializer_194 () Bool (= (table0 #xc2) s0))
[GOOD] (define-fun table0_initializer_195 () Bool (= (table0 #xc3) s0))
[GOOD] (define-fun table0_initializer_196 () Bool (= (table0 #xc4) s0))
[GOOD] (define-fun table0_initializer_197 () Bool (= (table0 #xc5) s0))
[GOOD] (define-fun table0_initializer_198 () Bool (= (table0 #xc6) s0))
[GOOD] (define-fun table0_initializer_199 () Bool (= (table0 #xc7) s0))
[GOOD] (define-fun table0_initializer_200 () Bool (= (table0 #xc8) s0))
[GOOD] (define-fun table0_initializer_201 () Bool (= (table0 #xc9) s0))
[GOOD] (define-fun table0_initializer_202 () Bool (= (table0 #xca) s0))
[GOOD] (define-fun table0_initializer_203 () Bool (= (table0 #xcb) s0))
[GOOD] (define-fun table0_initializer_204 () Bool (= (table0 #xcc) s0))
[GOOD] (define-fun table0_initializer_205 () Bool (= (table0 #xcd) s0))
[GOOD] (define-fun table0_initializer_206 () Bool (= (table0 #xce) s0))
[GOOD] (define-fun table0_initializer_207 () Bool (= (table0 #xcf) s0))
[GOOD] (define-fun table0_initializer_208 () Bool (= (table0 #xd0) s0))
[GOOD] (define-fun table0_initializer_209 () Bool (= (table0 #xd1) s0))
[GOOD] (define-fun table0_initializer_210 () Bool (= (table0 #xd2) s0))
[GOOD] (define-fun table0_initializer_211 () Bool (= (table0 #xd3) s0))
[GOOD] (define-fun table0_initializer_212 () Bool (= (table0 #xd4) s0))
[GOOD] (define-fun table0_initializer_213 () Bool (= (table0 #xd5) s0))
[GOOD] (define-fun table0_initializer_214 () Bool (= (table0 #xd6) s0))
[GOOD] (define-fun table0_initializer_215 () Bool (= (table0 #xd7) s0))
[GOOD] (define-fun table0_initializer_216 () Bool (= (table0 #xd8) s0))
[GOOD] (define-fun table0_initializer_217 () Bool (= (table0 #xd9) s0))
[GOOD] (define-fun table0_initializer_218 () Bool (= (table0 #xda) s0))
[GOOD] (define-fun table0_initializer_219 () Bool (= (table0 #xdb) s0))
[GOOD] (define-fun table0_initializer_220 () Bool (= (table0 #xdc) s0))
[GOOD] (define-fun table0_initializer_221 () Bool (= (table0 #xdd) s0))
[GOOD] (define-fun table0_initializer_222 () Bool (= (table0 #xde) s0))
[GOOD] (define-fun table0_initializer_223 () Bool (= (table0 #xdf) s0))
[GOOD] (define-fun table0_initializer_224 () Bool (= (table0 #xe0) s0))
[GOOD] (define-fun table0_initializer_225 () Bool (= (table0 #xe1) s0))
[GOOD] (define-fun table0_initializer_226 () Bool (= (table0 #xe2) s0))
[GOOD] (define-fun table0_initializer_227 () Bool (= (table0 #xe3) s0))
[GOOD] (define-fun table0_initializer_228 () Bool (= (table0 #xe4) s0))
[GOOD] (define-fun table0_initializer_229 () Bool (= (table0 #xe5) s0))
[GOOD] (define-fun table0_initializer_230 () Bool (= (table0 #xe6) s0))
[GOOD] (define-fun table0_initializer_231 () Bool (= (table0 #xe7) s0))
[GOOD] (define-fun table0_initializer_232 () Bool (= (table0 #xe8) s0))
[GOOD] (define-fun table0_initializer_233 () Bool (= (table0 #xe9) s0))
[GOOD] (define-fun table0_initializer_234 () Bool (= (table0 #xea) s0))
[GOOD] (define-fun table0_initializer_235 () Bool (= (table0 #xeb) s0))
[GOOD] (define-fun table0_initializer_236 () Bool (= (table0 #xec) s0))
[GOOD] (define-fun table0_initializer_237 () Bool (= (table0 #xed) s0))
[GOOD] (define-fun table0_initializer_238 () Bool (= (table0 #xee) s0))
[GOOD] (define-fun table0_initializer_239 () Bool (= (table0 #xef) s0))
[GOOD] (define-fun table0_initializer_240 () Bool (= (table0 #xf0) s0))
[GOOD] (define-fun table0_initializer_241 () Bool (= (table0 #xf1) s0))
[GOOD] (define-fun table0_initializer_242 () Bool (= (table0 #xf2) s0))
[GOOD] (define-fun table0_initializer_243 () Bool (= (table0 #xf3) s0))
[GOOD] (define-fun table0_initializer_244 () Bool (= (table0 #xf4) s0))
[GOOD] (define-fun table0_initializer_245 () Bool (= (table0 #xf5) s0))
[GOOD] (define-fun table0_initializer_246 () Bool (= (table0 #xf6) s0))
[GOOD] (define-fun table0_initializer_247 () Bool (= (table0 #xf7) s0))
[GOOD] (define-fun table0_initializer_248 () Bool (= (table0 #xf8) s0))
[GOOD] (define-fun table0_initializer_249 () Bool (= (table0 #xf9) s0))
[GOOD] (define-fun table0_initializer_250 () Bool (= (table0 #xfa) s0))
[GOOD] (define-fun table0_initializer_251 () Bool (= (table0 #xfb) s0))
[GOOD] (define-fun table0_initializer_252 () Bool (= (table0 #xfc) s0))
[GOOD] (define-fun table0_initializer_253 () Bool (= (table0 #xfd) s0))
[GOOD] (define-fun table0_initializer_254 () Bool (= (table0 #xfe) s0))
[GOOD] (define-fun table0_initializer_255 () Bool (= (table0 #xff) s0))
[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 s2 () (_ BitVec 8) (table0 s0))
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (assert s3)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 #x00))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:0
DONE!