用IDA打开，直接打开主要函数，如图

只有一个if语句，里面的判断条件是很多不等式，达到了900多行。

我在这里遇到了一个问题就是，input长度是31位，而在后面的条件判断中的不等式出现了

(char)v5
SBYTE1(v5)
SBYTE2(v5)
SHIBYTE(v5)
(char)v6
SHIBYTE(v6)
(char)v7

四个函数点击并没有反应，初始定义了input的长度是24，则索引是0到23，后面又输入了31位的input，这里可能是IDA将数组长度分析错误了，这题的hint中也有提到，如图

那剩余的应该是覆盖到v5,v6,v7去了，但是这里的函数我实在不懂啥意思，问了学长说是IDA的宏定义，可以到IDA文件中的defs.h头文件里面找，如图

但是咱也看不懂啊，也不知道这函数有什么用处，后面又问了同级的大佬，它也没解释个所以然来，但是他教我对着v5按y，再输入char[4]之后，就变成了下图这样

那我们就大概可以知道顺序,也可以猜到什么的函数代表的是谁，如图

在下面的SHIBYTE(v6)应该就是input[29]，而v7代表的应该就是input[30]。上面说的y可以改变变量的类型。满座if语句所有条件就可以得到flag，解方程组，用Python的z3求解约束器，Writeup脚本如下：

from z3 import *
s=Solver()
v4 = [BitVec('u%d' % i,8) for i in range(0, 31)]
#上面一行设置列表这里值得学习
s.add(v4[0] == ord('m'))
s.add(v4[1] == ord('o'))
s.add(v4[2] == ord('e'))
s.add(v4[3] == ord('c'))
s.add(v4[4] == ord('t'))
s.add(v4[5] == ord('f'))
s.add(334 * v4[28] + 100 * v4[27] + 369 * v4[26] + 124 * v4[25] + 278 * v4[24] + 158 * v4[23] + 162 * v4[22] + 145 * v4[19] + 27 * v4[17] + 91 * v4[15] + 195 * v4[14] + 342 * v4[13] + 391 * v4[10] + 204 * v4[9] + 302 * v4[8] + 153 * v4[7] + 292 * v4[6] + 382 * v4[5] + 221 * v4[4] + 316 * v4[3] + 118 * v4[2] + 295 * v4[1] + 247 * v4[0] + 236 *v4[11] + 27 * v4[12] + 361 * v4[16] + 81 * v4[18] + 105 * v4[20] + 65 * v4[21] + 67 * v4[29] + 41 * v4[30] == 596119)
s.add(371 * v4[29] + 338 * v4[28] + 269 * v4[27] + 312 * v4[26] + 67 * v4[25] + 299 * v4[24] + 235 * v4[23] + 294 * v4[22] + 303 * v4[21] + 211 * v4[20] + 122 * v4[19] + 333 * v4[18] + 341 * v4[15] + 111 * v4[14] + 253 * v4[13] + 68 *v4[12] + 347 * v4[11] + 44 * v4[10] + 262 * v4[9] + 357 * v4[8] + 323 * v4[5] + 141 * v4[4] + 329 * v4[3] + 378 *v4[2] + 316 * v4[1] + 235 * v4[0] + 59 * v4[6] + 37 * v4[7] + 264 * v4[16] + 73 * v4[17] + 126 * v4[30] == 634009)
s.add(337 * v4[29] + 338 * v4[28] + 118 * v4[27] + 82 * v4[26] + 239 * v4[21] + 58 * v4[20] + 304 * v4[19] + 330 * v4[18] + 377 * v4[17] + 306 * v4[16] + 221 * v4[13] + 345 * v4[12] + 124 * v4[11] + 272 * v4[10] + 270 * v4[9] + 229 *v4[8] + 377 * v4[7] + 373 * v4[6] + 297 * v4[5] + 112 * v4[4] + 386 * v4[3] + 90 * v4[2] + 361 * v4[1] + 236 * v4[0] + 386 * v4[14] + 73 * v4[15] + 315 * v4[22] + 33 * v4[23] + 141 * v4[24] + 129 * v4[25] + 123 * v4[30] == 685705)
s.add(367 * v4[29] + 55 * v4[28] + 374 * v4[27] + 150 * v4[24] + 350 * v4[23] + 141 * v4[22] + 124 * v4[21] + 366 * v4[20] + 230 * v4[19] + 307 * v4[18] + 191 * v4[17] + 153 * v4[12] + 383 * v4[11] + 145 * v4[10] + 109 * v4[9] + 209 *v4[8] + 158 * v4[7] + 221 * v4[6] + 188 * v4[5] + 22 * v4[4] + 146 * v4[3] + 306 * v4[2] + 230 * v4[1] + 13 * v4[0] + 287 * v4[13] + 257 * v4[14] + 137 * v4[15] + 7 * v4[16] + 52 * v4[25] + 31 * v4[26] + 355 * v4[30] == 557696)
s.add(100 * v4[29] + 191 * v4[28] + 362 * v4[27] + 55 * v4[26] + 210 * v4[25] + 359 * v4[24] + 348 * v4[21] + 83 * v4[20] + 395 * v4[19] + 350 * v4[16] + 291 * v4[15] + 220 * v4[12] + 196 * v4[11] + 399 * v4[8] + 68 * v4[7] + 84 * v4[6] + 281 * v4[5] + 334 * v4[4] + 53 * v4[3] + 399 * v4[2] + 338 * v4[0] + 18 * v4[1] + 148 * v4[9] + 21 * v4[10] + 174 * v4[13] + 36 * v4[14] + 2 * v4[17] + 41 * v4[18] + 137 * v4[22] + 24 * v4[23] + 368 * v4[30] == 538535)
s.add(188 * v4[29] + (v4[26] << 7) + 93 * v4[25] + 248 * v4[24] + 83 * v4[23] + 207 * v4[22] + 217 * v4[19] + 309 * v4[16] + 16 * v4[15] + 135 * v4[14] + 251 * v4[13] + 200 * v4[12] + 49 * v4[11] + 119 * v4[10] + 356 * v4[9] + 398 *v4[8] + 303 * v4[7] + 224 * v4[6] + 208 * v4[5] + 244 * v4[4] + 209 * v4[3] + 189 * v4[2] + 302 * v4[1] + 395 *v4[0] + 314 * v4[17] + 13 * v4[18] + 310 * v4[20] + 21 * v4[21] + 67 * v4[27] + 127 * v4[28] + 100 * v4[30] == 580384)
s.add(293 * v4[29] + 343 * v4[28] + 123 * v4[27] + 387 * v4[26] + 114 * v4[25] + 303 * v4[24] + 248 * v4[23] + 258 * v4[21] + 218 * v4[20] + 180 * v4[19] + 196 * v4[18] + 398 * v4[17] + 398 * v4[14] + 138 * v4[9] + 292 * v4[8] + 38 *v4[7] + 179 * v4[6] + 190 * v4[5] + 57 * v4[4] + 358 * v4[3] + 191 * v4[2] + 215 * v4[1] + 88 * v4[0] + 22 * v4[10] + 72 * v4[11] + 357 * v4[12] + 9 * v4[13] + 389 * v4[15] + 81 * v4[16] + 85 * v4[30] == 529847)
s.add(311 * v4[29] + 202 * v4[28] + 234 * v4[27] + 272 * v4[26] + 55 * v4[25] + 328 * v4[24] + 246 * v4[23] + 362 * v4[22] + 86 * v4[21] + 75 * v4[20] + 142 * v4[17] + 244 * v4[16] + 216 * v4[15] + 281 * v4[14] + 398 * v4[13] + 322 *v4[12] + 251 * v4[11] + 357 * v4[8] + 76 * v4[7] + 292 * v4[6] + 389 * v4[5] + 275 * v4[4] + 312 * v4[3] + 200 * v4[2] + 110 * v4[1] + 203 * v4[0] + 99 * v4[9] + 21 * v4[10] + 269 * v4[18] + 33 * v4[19] + 356 * v4[30] == 631652)
s.add(261 * v4[29] + 189 * v4[26] + 55 * v4[25] + 23 * v4[24] + 202 * v4[23] + 185 * v4[22] + 182 * v4[21] + 285 * v4[20] + 217 * v4[17] + 157 * v4[16] + 232 * v4[15] + 132 * v4[14] + 169 * v4[13] + 154 * v4[12] + 121 * v4[11] + 389 * v4[10] + 376 * v4[9] + 292 * v4[6] + 225 * v4[5] + 155 * v4[4] + 234 * v4[3] + 149 * v4[2] + 241 * v4[1] + 312 *v4[0] + 368 * v4[7] + 129 * v4[8] + 226 * v4[18] + 288 * v4[19] + 201 * v4[27] + 288 * v4[28] + 69 * v4[30] == 614840)
s.add(60 * v4[29] + 118 * v4[28] + 153 * v4[27] + 139 * v4[26] + 23 * v4[25] + 279 * v4[24] + 396 * v4[23] + 287 * v4[22] + 237 * v4[19] + 266 * v4[18] + 149 * v4[17] + 193 * v4[16] + 395 * v4[15] + 97 * v4[14] + 16 * v4[13] + 286 * v4[12] + 105 * v4[11] + 88 * v4[10] + 282 * v4[9] + 55 * v4[8] + 134 * v4[7] + 114 * v4[6] + 101 * v4[5] + 116 * v4[4] + 271 * v4[3] + 186 * v4[2] + 263 * v4[1] + 313 * v4[0] + 149 * v4[20] + 129 * v4[21] + 145 * v4[30] == 510398)
s.add(385 * v4[29] + 53 * v4[28] + 112 * v4[27] + 8 * v4[26] + 232 * v4[25] + 145 * v4[24] + 313 * v4[23] + 156 * v4[22] + 321 * v4[21] + 358 * v4[20] + 46 * v4[19] + 382 * v4[18] + 144 * v4[16] + 222 * v4[14] + 329 * v4[13] + 161 *v4[12] + 335 * v4[11] + 50 * v4[10] + 373 * v4[9] + 66 * v4[8] + 44 * v4[7] + 59 * v4[6] + 292 * v4[5] + 39 * v4[4] + 53 * v4[3] + 310 * v4[0] + 154 * v4[1] + 24 * v4[2] + 396 * v4[15] + 81 * v4[17] + 355 * v4[30] == 558740)
s.add(249 * v4[29] + 386 * v4[28] + 313 * v4[27] + 74 * v4[26] + 22 * v4[25] + 168 * v4[24] + 305 * v4[21] + 358 * v4[20] + 191 * v4[19] + 202 * v4[18] + 14 * v4[15] + 114 * v4[14] + 224 * v4[13] + 134 * v4[12] + 274 * v4[11] + 372 *v4[10] + 159 * v4[9] + 233 * v4[8] + 70 * v4[7] + 287 * v4[6] + 297 * v4[5] + 318 * v4[4] + 177 * v4[3] + 173 * v4[2] + 270 * v4[1] + 163 * v4[0] + 77 * v4[16] + 25 * v4[17] + 387 * v4[22] + 18 * v4[23] + 345 * v4[30] == 592365)
s.add(392 * v4[29] + 385 * v4[28] + 302 * v4[27] + 13 * v4[25] + 27 * v4[24] + 99 * v4[22] + 343 * v4[19] + 324 * v4[18] + 223 * v4[17] + 372 * v4[16] + 261 * v4[15] + 181 * v4[14] + 203 * v4[13] + 232 * v4[12] + 305 * v4[11] + 393 * v4[10] + 325 * v4[9] + 231 * v4[8] + 92 * v4[7] + 142 * v4[6] + 22 * v4[5] + 86 * v4[4] + 264 * v4[3] + 300 * v4[2] + 387 * v4[1] + 360 * v4[0] + 225 * v4[20] + 127 * v4[21] + 2 * v4[23] + 80 * v4[26] + 268 * v4[30] == 619574)
s.add(270 * v4[28] + 370 * v4[27] + 235 * v4[26] + 96 * v4[22] + 85 * v4[20] + 150 * v4[19] + 140 * v4[18] + 94 * v4[17] + 295 * v4[16] + 19 * v4[14] + 176 * v4[12] + 94 * v4[11] + 258 * v4[10] + 302 * v4[9] + 171 * v4[8] + 66 * v4[7] + 278 * v4[6] + 193 * v4[5] + 251 * v4[4] + 284 * v4[3] + 218 * v4[2] + (v4[1] << 6) + 319 * v4[0] + 125 * v4[13] + 24 * v4[15] + 267 * v4[21] + 160 * v4[23] + 111 * v4[24] + 33 * v4[25] + 174 * v4[29] + 13 * v4[30] == 480557)
s.add(87 * v4[28] + 260 * v4[27] + 326 * v4[26] + 210 * v4[25] + 357 * v4[24] + 170 * v4[23] + 315 * v4[22] + 376 * v4[21] + 227 * v4[20] + 43 * v4[19] + 358 * v4[18] + 364 * v4[17] + 309 * v4[16] + 282 * v4[15] + 286 * v4[14] + 365 *v4[13] + 287 * v4[12] + 377 * v4[11] + 74 * v4[10] + 225 * v4[9] + 328 * v4[6] + 223 * v4[5] + 120 * v4[4] + 102 * v4[3] + 162 * v4[2] + 123 * v4[1] + 196 * v4[0] + 29 * v4[7] + 27 * v4[8] + 352 * v4[30] == 666967)
s.add(61 * v4[29] + 195 * v4[28] + 125 * v4[27] + (v4[26] << 6) + 260 * v4[25] + 202 * v4[24] + 116 * v4[23] + 230 * v4[ 22] + 326 * v4[21] + 211 * v4[20] + 371 * v4[19] + 353 * v4[16] + 124 * v4[13] + 188 * v4[12] + 163 * v4[11] + 140 *v4[10] + 51 * v4[9] + 262 * v4[8] + 229 * v4[7] + 100 * v4[6] + 113 * v4[5] + 158 * v4[4] + 378 * v4[3] + 365 *v4[2] + 207 * v4[1] + 277 * v4[0] + 190 * v4[14] + 320 * v4[15] + 347 * v4[17] + 11 * v4[18] + 137 * v4[30] == 590534)
s.add(39 * v4[28] + 303 * v4[27] + 360 * v4[26] + 157 * v4[25] + 324 * v4[24] + 77 * v4[23] + 308 * v4[22] + 313 * v4[21] + 87 * v4[20] + 201 * v4[19] + 50 * v4[18] + 60 * v4[17] + 28 * v4[16] + 193 * v4[15] + 184 * v4[14] + 205 * v4[13] + 140 * v4[12] + 311 * v4[11] + 304 * v4[10] + 35 * v4[9] + 356 * v4[8] + 23 * v4[5] + 85 * v4[4] + 156 * v4[3] + 16 * v4[2] + 26 * v4[1] + 157 * v4[0] + 150 * v4[6] + 72 * v4[7] + 58 * v4[29] == 429108)
s.add(157 * v4[29] + 137 * v4[28] + 71 * v4[27] + 269 * v4[26] + 161 * v4[25] + 317 * v4[20] + 296 * v4[19] + 385 * v4[18] + 165 * v4[13] + 159 * v4[12] + 132 * v4[11] + 296 * v4[10] + 162 * v4[7] + 254 * v4[4] + 172 * v4[3] + 132 * v4[0] + 369 * v4[1] + 257 * v4[2] + 134 * v4[5] + 384 * v4[6] + 53 * v4[8] + 255 * v4[9] + 229 * v4[14] + 129 * v4[15] + 23 * v4[16] + 41 * v4[17] + 112 * v4[21] + 17 * v4[22] + 222 * v4[23] + 96 * v4[24] + 126 * v4[30] == 563521)
s.add(207 * v4[29] + 83 * v4[28] + 111 * v4[27] + 35 * v4[26] + 67 * v4[25] + 138 * v4[22] + 223 * v4[21] + 142 * v4[20] + 154 * v4[19] + 111 * v4[18] + 341 * v4[17] + 175 * v4[16] + 259 * v4[15] + 225 * v4[14] + 26 * v4[11] + 334 * v4[10] + 250 * v4[7] + 198 * v4[6] + 279 * v4[5] + 301 * v4[4] + 193 * v4[3] + 334 * v4[2] + 134 * v4[0] + 37 * v4[1] + 183 * v4[8] + 5 * v4[9] + 270 * v4[12] + 21 * v4[13] + 275 * v4[23] + 48 * v4[24] + 163 * v4[30] == 493999)
s.add(393 * v4[29] + 176 * v4[28] + 105 * v4[27] + 162 * v4[26] + 148 * v4[25] + 281 * v4[24] + 300 * v4[23] + 342 * v4[18] + 262 * v4[17] + 152 * v4[12] + 43 * v4[11] + 296 * v4[10] + 273 * v4[9] + 75 * v4[6] + 18 * v4[4] + 217 * v4[2] + 132 * v4[1] + 112 * v4[0] + 210 * v4[3] + 72 * v4[5] + 113 * v4[7] + 40 * v4[8] + 278 * v4[13] + 24 * v4[14] + 77 * v4[15] + 11 * v4[16] + 55 * v4[19] + 255 * v4[20] + 241 * v4[21] + 13 * v4[22] + 356 * v4[30] == 470065)
s.add(369 * v4[29] + 231 * v4[28] + 285 * v4[25] + 290 * v4[24] + 297 * v4[23] + 189 * v4[22] + 390 * v4[21] + 345 * v4[20] + 153 * v4[19] + 114 * v4[18] + 251 * v4[17] + 340 * v4[16] + 44 * v4[15] + 58 * v4[14] + 335 * v4[13] + 359 * v4[12] + 392 * v4[11] + 181 * v4[8] + 103 * v4[7] + 229 * v4[6] + 175 * v4[5] + 208 * v4[4] + 92 * v4[3] + 397 * v4[2] + 349 * v4[1] + 356 * v4[0] + (v4[9] << 6) + 5 * v4[10] + 88 * v4[26] + 40 * v4[27] + 295 * v4[30] == 661276)
s.add(341 * v4[27] + 40 * v4[25] + 374 * v4[23] + 201 * v4[22] + 77 * v4[21] + 215 * v4[20] + 283 * v4[19] + 213 * v4[18] + 392 * v4[17] + 224 * v4[16] + v4[15] + 270 * v4[12] + 28 * v4[11] + 75 * v4[8] + 386 * v4[7] + 298 * v4[6] + 170 * v4[5] + 287 * v4[4] + 247 * v4[3] + 204 * v4[2] + 103 * v4[1] + 21 * v4[0] + 84 * v4[9] + 27 * v4[10] + 159 * v4[13] + 192 * v4[14] + 213 * v4[24] + 129 * v4[26] + 67 * v4[28] + 27 * v4[29] + 361 * v4[30] == 555288)
s.add(106 * v4[29] + 363 * v4[28] + 210 * v4[27] + 171 * v4[26] + 289 * v4[25] + 240 * v4[24] + 164 * v4[23] + 342 * v4[22] + 391 * v4[19] + 304 * v4[18] + 218 * v4[17] + 32 * v4[16] + 350 * v4[15] + 339 * v4[12] + 303 * v4[11] + 222 * v4[10] + 298 * v4[9] + 47 * v4[8] + 48 * v4[6] + 264 * v4[4] + 113 * v4[3] + 275 * v4[2] + 345 * v4[1] + 312 * v4[0] + 171 * v4[5] + 384 * v4[7] + 175 * v4[13] + 5 * v4[14] + 113 * v4[20] + 19 * v4[21] + 263 * v4[30] == 637650)
s.add(278 * v4[29] + 169 * v4[28] + 62 * v4[27] + 119 * v4[26] + 385 * v4[25] + 289 * v4[24] + 344 * v4[23] + 45 * v4[20] + 308 * v4[19] + 318 * v4[18] + 270 * v4[17] + v4[16] + 323 * v4[15] + 332 * v4[14] + 287 * v4[11] + 170 * v4[10] + 163 * v4[9] + 301 * v4[8] + 303 * v4[7] + 23 * v4[6] + 327 * v4[5] + 169 * v4[3] + 28 * v4[0] + 365 * v4[1] + 15 * v4[2] + 352 * v4[12] + 72 * v4[13] + 140 * v4[21] + 65 * v4[22] + 346 * v4[30] == 572609)
s.add(147 * v4[29] + 88 * v4[28] + 143 * v4[27] + 237 * v4[26] + 63 * v4[24] + 281 * v4[22] + 388 * v4[21] + 142 * v4[20] + 208 * v4[19] + 60 * v4[18] + 354 * v4[15] + 88 * v4[14] + 146 * v4[13] + 290 * v4[12] + 349 * v4[11] + 43 * v4[10] + 230 * v4[9] + 267 * v4[6] + 136 * v4[5] + 383 * v4[4] + 35 * v4[3] + 226 * v4[2] + 385 * v4[1] + 238 * v4[0] + 348 * v4[7] + 20 * v4[8] + 158 * v4[16] + 21 * v4[17] + 249 * v4[23] + 9 * v4[25] + 343 * v4[30] == 603481)
s.add(29 * v4[29] + 323 * v4[26] + 159 * v4[25] + 118 * v4[20] + 326 * v4[19] + 211 * v4[18] + 225 * v4[17] + 355 * v4[16] + 201 * v4[15] + 149 * v4[14] + 296 * v4[13] + 184 * v4[12] + 315 * v4[11] + 364 * v4[10] + 142 * v4[9] + 75 * v4[8] + 313 * v4[7] + 142 * v4[6] + 396 * v4[5] + 348 * v4[4] + 272 * v4[3] + 26 * v4[2] + 206 * v4[1] + 173 * v4[0] + 155 * v4[21] + 144 * v4[22] + 366 * v4[23] + 257 * v4[24] + 148 * v4[27] + 24 * v4[28] + 253 * v4[30] == 664504)
s.add(4 * v4[29] + 305 * v4[28] + 226 * v4[27] + 212 * v4[26] + 175 * v4[25] + 93 * v4[24] + 165 * v4[23] + 341 * v4[20] + 14 * v4[19] + 394 * v4[18] + (v4[17] << 8) + 252 * v4[16] + 336 * v4[15] + 38 * v4[14] + 82 * v4[13] + 155 * v4[12] + 215 * v4[11] + 331 * v4[10] + 230 * v4[9] + 241 * v4[8] + 225 * v4[7] + 186 * v4[4] + 90 * v4[3] + 50 * v4[2] + 62 * v4[1] + 34 * v4[0] + 237 * v4[5] + 11 * v4[6] + 336 * v4[21] + 36 * v4[22] + 29 * v4[30] == 473092)
s.add(353 * v4[29] + 216 * v4[28] + 252 * v4[27] + 8 * v4[26] + 62 * v4[25] + 233 * v4[24] + 254 * v4[23] + 303 * v4[22] + 234 * v4[21] + 303 * v4[20] + (v4[19] << 8) + 148 * v4[18] + 324 * v4[17] + 317 * v4[16] + 213 * v4[15] + 309 * v4[14] + 28 * v4[13] + 280 * v4[11] + 118 * v4[10] + 58 * v4[9] + 50 * v4[8] + 155 * v4[7] + 161 * v4[6] + (v4[5] << 6) + 303 * v4[4] + 76 * v4[3] + 43 * v4[2] + 109 * v4[1] + 102 * v4[0] + 93 * v4[30] == 497492)
s.add(89 * v4[29] + 148 * v4[28] + 82 * v4[27] + 53 * v4[26] + 274 * v4[25] + 220 * v4[24] + 202 * v4[23] + 123 * v4[22] + 231 * v4[21] + 169 * v4[20] + 278 * v4[19] + 259 * v4[18] + 208 * v4[17] + 219 * v4[16] + 371 * v4[15] + 181 * v4[12] + 104 * v4[11] + 392 * v4[10] + 285 * v4[9] + 113 * v4[8] + 298 * v4[7] + 389 * v4[6] + 322 * v4[5] + 338 * v4[4] + 237 * v4[3] + 234 * v4[0] + 261 * v4[1] + 10 * v4[2] + 345 * v4[13] + 3 * v4[14] + 361 * v4[30] == 659149)
s.add(361 * v4[29] + 359 * v4[28] + 93 * v4[27] + 315 * v4[26] + 69 * v4[25] + 137 * v4[24] + 69 * v4[23] + 58 * v4[22] + 300 * v4[21] + 371 * v4[20] + 264 * v4[19] + 317 * v4[18] + 215 * v4[17] + 155 * v4[16] + 215 * v4[15] + 330 * v4[14] + 239 * v4[13] + 212 * v4[12] + 88 * v4[11] + 82 * v4[10] + 354 * v4[9] + 85 * v4[8] + 310 * v4[7] + 84 * v4[6] + 374 * v4[5] + 380 * v4[4] + 215 * v4[3] + 351 * v4[2] + 141 * v4[1] + 115 * v4[0] + 108 * v4[30] == 629123)
if s.check() == sat:
	ans = s.model()
	print(ans)
#此处输出[u15 = 51,u30 = 125,u8 = 48,u7 = 121,u6 = 123,u9 = 117,u10 = 95,u11 = 115,u12 = 48,u13 = 108,u14 = 118,u16 = 100,u17 = 95,u18 = 69,u19 = 113,u20 = 117,u21 = 97,u22 = 116,u23 = 105,u24 = 48,u26 = 115,u25 = 110,u27 = 33,u4 = 116,u0 = 109,u5 = 102,u3 = 99,u29 = 33,u2 = 101,u28 = 33,u1 = 111]，这样乱序的，我也不知道怎么处理了，可以手动处理
flag = []
enc = [109, 111, 101, 99, 116, 102, 123, 121, 48, 117, 95, 115, 48, 108, 118, 51, 100, 95, 69, 117, 97, 116, 105, 48, 110, 115, 33, 33, 33, 125 ]
for i in range(len(enc)):
	flag.append(chr(enc[i]))
print("".join(flag))

v4 = [BitVec(‘u%d’ % i,8) for i in range(0, 31)] 这一行代码中的”%i”好像应该是一个字符串格式化操作符，用于将整数插入到字符串中，z3里面设置列表的我还是第一次见到的

输出moectf{y0u_s0lv3d_Euati0ns!!!}

还看到其他大佬的脚本更简洁的，如下

from z3 import *
s=Solver()
flag = [Int("flag[%d]"%i) for i in range(31)]
x=[flag[0]*247+flag[1]*295+flag[2]*118+flag[3]*316+flag[4]*221+flag[5]*382+flag[6]*292+flag[7]*153+flag[8]*302+flag[9]*204+flag[10]*391+flag[11]*236+flag[12]*27+flag[13]*342+flag[14]*195+flag[15]*91+flag[16]*361+flag[17]*27+flag[18]*81+flag[19]*145+flag[20]*105+flag[21]*64+flag[22]*162+flag[23]*158+flag[24]*278+flag[25]*124+flag[26]*369+flag[27]*100+flag[28]*334+flag[29]*67+flag[30]*41==596022,
flag[0]*235+flag[1]*316+flag[2]*378+flag[3]*329+flag[4]*141+flag[5]*323+flag[6]*59+flag[7]*37+flag[8]*357+flag[9]*262+flag[10]*44+flag[11]*347+flag[12]*68+flag[13]*253+flag[14]*111+flag[15]*341+flag[16]*264+flag[17]*73+flag[18]*333+flag[19]*122+flag[20]*211+flag[21]*303+flag[22]*294+flag[23]*235+flag[24]*299+flag[25]*67+flag[26]*312+flag[27]*269+flag[28]*338+flag[29]*371+flag[30]*126==634009,
flag[0]*236+flag[1]*361+flag[2]*90+flag[3]*386+flag[4]*112+flag[5]*297+flag[6]*373+flag[7]*377+flag[8]*229+flag[9]*270+flag[10]*272+flag[11]*124+flag[12]*345+flag[13]*221+flag[14]*386+flag[15]*73+flag[16]*306+flag[17]*377+flag[18]*330+flag[19]*304+flag[20]*58+flag[21]*239+flag[22]*315+flag[23]*33+flag[24]*141+flag[25]*129+flag[26]*82+flag[27]*118+flag[28]*338+flag[29]*337+flag[30]*123==685705,
flag[0]*13+flag[1]*230+flag[2]*306+flag[3]*146+flag[4]*22+flag[5]*188+flag[6]*221+flag[7]*158+flag[8]*209+flag[9]*109+flag[10]*145+flag[11]*383+flag[12]*153+flag[13]*287+flag[14]*257+flag[15]*137+flag[16]*7+flag[17]*191+flag[18]*307+flag[19]*230+flag[20]*366+flag[21]*124+flag[22]*141+flag[23]*350+flag[24]*150+flag[25]*52+flag[26]*31+flag[27]*374+flag[28]*55+flag[29]*367+flag[30]*355==557696,
flag[0]*338+flag[1]*18+flag[2]*399+flag[3]*53+flag[4]*334+flag[5]*281+flag[6]*84+flag[7]*68+flag[8]*399+flag[9]*148+flag[10]*21+flag[11]*196+flag[12]*220+flag[13]*174+flag[14]*36+flag[15]*291+flag[16]*350+flag[17]*2+flag[18]*41+flag[19]*395+flag[20]*83+flag[21]*348+flag[22]*137+flag[23]*24+flag[24]*359+flag[25]*210+flag[26]*55+flag[27]*362+flag[28]*191+flag[29]*100+flag[30]*368==538535,
flag[0]*395+flag[1]*302+flag[2]*189+flag[3]*209+flag[4]*244+flag[5]*208+flag[6]*224+flag[7]*303+flag[8]*398+flag[9]*356+flag[10]*119+flag[11]*49+flag[12]*200+flag[13]*251+flag[14]*135+flag[15]*16+flag[16]*309+flag[17]*314+flag[18]*13+flag[19]*217+flag[20]*310+flag[21]*21+flag[22]*207+flag[23]*83+flag[24]*248+flag[25]*93+flag[26]*128+flag[27]*67+flag[28]*127+flag[29]*188+flag[30]*100==580384,
flag[0]*88+flag[1]*215+flag[2]*191+flag[3]*358+flag[4]*57+flag[5]*190+flag[6]*179+flag[7]*38+flag[8]*292+flag[9]*138+flag[10]*22+flag[11]*72+flag[12]*357+flag[13]*9+flag[14]*398+flag[15]*389+flag[16]*81+flag[17]*398+flag[18]*196+flag[19]*180+flag[20]*218+flag[21]*258+flag[22]*0+flag[23]*248+flag[24]*303+flag[25]*114+flag[26]*387+flag[27]*123+flag[28]*343+flag[29]*293+flag[30]*85==529847,
flag[0]*203+flag[1]*110+flag[2]*200+flag[3]*312+flag[4]*275+flag[5]*389+flag[6]*292+flag[7]*76+flag[8]*357+flag[9]*99+flag[10]*21+flag[11]*251+flag[12]*322+flag[13]*398+flag[14]*281+flag[15]*216+flag[16]*244+flag[17]*142+flag[18]*269+flag[19]*33+flag[20]*75+flag[21]*86+flag[22]*362+flag[23]*246+flag[24]*328+flag[25]*55+flag[26]*272+flag[27]*234+flag[28]*202+flag[29]*311+flag[30]*356==631652,
flag[0]*312+flag[1]*241+flag[2]*149+flag[3]*234+flag[4]*155+flag[5]*225+flag[6]*292+flag[7]*368+flag[8]*129+flag[9]*376+flag[10]*389+flag[11]*121+flag[12]*154+flag[13]*169+flag[14]*132+flag[15]*232+flag[16]*157+flag[17]*217+flag[18]*226+flag[19]*288+flag[20]*285+flag[21]*182+flag[22]*185+flag[23]*202+flag[24]*23+flag[25]*55+flag[26]*189+flag[27]*201+flag[28]*288+flag[29]*261+flag[30]*69==614840,
flag[0]*313+flag[1]*263+flag[2]*186+flag[3]*271+flag[4]*116+flag[5]*101+flag[6]*114+flag[7]*134+flag[8]*55+flag[9]*282+flag[10]*88+flag[11]*105+flag[12]*286+flag[13]*16+flag[14]*97+flag[15]*395+flag[16]*193+flag[17]*149+flag[18]*266+flag[19]*237+flag[20]*149+flag[21]*129+flag[22]*287+flag[23]*396+flag[24]*279+flag[25]*23+flag[26]*139+flag[27]*153+flag[28]*118+flag[29]*60+flag[30]*145==510398,
flag[0]*310+flag[1]*154+flag[2]*24+flag[3]*53+flag[4]*39+flag[5]*292+flag[6]*59+flag[7]*44+flag[8]*66+flag[9]*373+flag[10]*50+flag[11]*335+flag[12]*161+flag[13]*329+flag[14]*222+flag[15]*396+flag[16]*144+flag[17]*81+flag[18]*382+flag[19]*46+flag[20]*358+flag[21]*321+flag[22]*156+flag[23]*313+flag[24]*145+flag[25]*232+flag[26]*8+flag[27]*112+flag[28]*53+flag[29]*385+flag[30]*355==558740,
flag[0]*163+flag[1]*270+flag[2]*173+flag[3]*177+flag[4]*318+flag[5]*297+flag[6]*287+flag[7]*70+flag[8]*233+flag[9]*159+flag[10]*372+flag[11]*274+flag[12]*134+flag[13]*224+flag[14]*114+flag[15]*14+flag[16]*77+flag[17]*25+flag[18]*202+flag[19]*191+flag[20]*358+flag[21]*305+flag[22]*387+flag[23]*18+flag[24]*168+flag[25]*22+flag[26]*74+flag[27]*313+flag[28]*386+flag[29]*249+flag[30]*345==592365,
flag[0]*360+flag[1]*387+flag[2]*300+flag[3]*264+flag[4]*86+flag[5]*22+flag[6]*142+flag[7]*92+flag[8]*231+flag[9]*325+flag[10]*393+flag[11]*305+flag[12]*232+flag[13]*203+flag[14]*181+flag[15]*261+flag[16]*372+flag[17]*223+flag[18]*324+flag[19]*343+flag[20]*225+flag[21]*127+flag[22]*99+flag[23]*2+flag[24]*27+flag[25]*13+flag[26]*80+flag[27]*302+flag[28]*385+flag[29]*392+flag[30]*268==619574,
flag[0]*319+flag[1]*64+flag[2]*218+flag[3]*284+flag[4]*251+flag[5]*193+flag[6]*278+flag[7]*66+flag[8]*171+flag[9]*302+flag[10]*258+flag[11]*94+flag[12]*176+flag[13]*125+flag[14]*19+flag[15]*24+flag[16]*295+flag[17]*94+flag[18]*140+flag[19]*150+flag[20]*85+flag[21]*267+flag[22]*96+flag[23]*160+flag[24]*111+flag[25]*33+flag[26]*235+flag[27]*370+flag[28]*270+flag[29]*174+flag[30]*13==480557,
flag[0]*196+flag[1]*123+flag[2]*162+flag[3]*102+flag[4]*120+flag[5]*223+flag[6]*328+flag[7]*29+flag[8]*27+flag[9]*225+flag[10]*74+flag[11]*377+flag[12]*287+flag[13]*365+flag[14]*286+flag[15]*282+flag[16]*309+flag[17]*364+flag[18]*358+flag[19]*43+flag[20]*227+flag[21]*376+flag[22]*315+flag[23]*170+flag[24]*357+flag[25]*210+flag[26]*326+flag[27]*260+flag[28]*87+flag[29]*0+flag[30]*352==666967,
flag[0]*277+flag[1]*207+flag[2]*365+flag[3]*378+flag[4]*158+flag[5]*113+flag[6]*100+flag[7]*229+flag[8]*262+flag[9]*51+flag[10]*140+flag[11]*163+flag[12]*188+flag[13]*124+flag[14]*190+flag[15]*320+flag[16]*353+flag[17]*347+flag[18]*11+flag[19]*371+flag[20]*211+flag[21]*326+flag[22]*230+flag[23]*116+flag[24]*202+flag[25]*260+flag[26]*64+flag[27]*125+flag[28]*195+flag[29]*61+flag[30]*137==590534,
flag[0]*157+flag[1]*26+flag[2]*16+flag[3]*156+flag[4]*85+flag[5]*23+flag[6]*150+flag[7]*72+flag[8]*356+flag[9]*35+flag[10]*304+flag[11]*311+flag[12]*140+flag[13]*205+flag[14]*184+flag[15]*193+flag[16]*28+flag[17]*60+flag[18]*50+flag[19]*201+flag[20]*87+flag[21]*313+flag[22]*308+flag[23]*77+flag[24]*324+flag[25]*157+flag[26]*360+flag[27]*303+flag[28]*39+flag[29]*58+flag[30]*0==429108,
flag[0]*132+flag[1]*369+flag[2]*257+flag[3]*172+flag[4]*254+flag[5]*134+flag[6]*384+flag[7]*162+flag[8]*53+flag[9]*255+flag[10]*296+flag[11]*132+flag[12]*159+flag[13]*165+flag[14]*229+flag[15]*129+flag[16]*23+flag[17]*41+flag[18]*385+flag[19]*296+flag[20]*317+flag[21]*112+flag[22]*17+flag[23]*222+flag[24]*96+flag[25]*161+flag[26]*269+flag[27]*71+flag[28]*137+flag[29]*157+flag[30]*126==563521,
flag[0]*134+flag[1]*37+flag[2]*334+flag[3]*193+flag[4]*301+flag[5]*279+flag[6]*198+flag[7]*250+flag[8]*183+flag[9]*5+flag[10]*334+flag[11]*26+flag[12]*270+flag[13]*21+flag[14]*225+flag[15]*259+flag[16]*175+flag[17]*341+flag[18]*111+flag[19]*154+flag[20]*142+flag[21]*223+flag[22]*138+flag[23]*275+flag[24]*48+flag[25]*67+flag[26]*35+flag[27]*111+flag[28]*83+flag[29]*207+flag[30]*163==493999,
flag[0]*112+flag[1]*132+flag[2]*217+flag[3]*210+flag[4]*18+flag[5]*72+flag[6]*75+flag[7]*113+flag[8]*40+flag[9]*273+flag[10]*296+flag[11]*43+flag[12]*152+flag[13]*278+flag[14]*24+flag[15]*77+flag[16]*11+flag[17]*262+flag[18]*342+flag[19]*55+flag[20]*255+flag[21]*241+flag[22]*13+flag[23]*300+flag[24]*281+flag[25]*148+flag[26]*162+flag[27]*105+flag[28]*176+flag[29]*393+flag[30]*356==470065,
flag[0]*356+flag[1]*349+flag[2]*397+flag[3]*92+flag[4]*208+flag[5]*175+flag[6]*229+flag[7]*103+flag[8]*181+flag[9]*64+flag[10]*5+flag[11]*392+flag[12]*359+flag[13]*335+flag[14]*58+flag[15]*44+flag[16]*340+flag[17]*251+flag[18]*114+flag[19]*153+flag[20]*345+flag[21]*390+flag[22]*189+flag[23]*297+flag[24]*290+flag[25]*285+flag[26]*88+flag[27]*40+flag[28]*231+flag[29]*369+flag[30]*295==661276,
flag[0]*21+flag[1]*103+flag[2]*204+flag[3]*247+flag[4]*287+flag[5]*170+flag[6]*298+flag[7]*386+flag[8]*75+flag[9]*84+flag[10]*27+flag[11]*28+flag[12]*270+flag[13]*159+flag[14]*192+flag[15]*1+flag[16]*224+flag[17]*392+flag[18]*213+flag[19]*283+flag[20]*215+flag[21]*77+flag[22]*201+flag[23]*374+flag[24]*213+flag[25]*40+flag[26]*129+flag[27]*341+flag[28]*67+flag[29]*27+flag[30]*361==555288,
flag[0]*312+flag[1]*345+flag[2]*275+flag[3]*113+flag[4]*264+flag[5]*171+flag[6]*48+flag[7]*384+flag[8]*47+flag[9]*298+flag[10]*222+flag[11]*303+flag[12]*339+flag[13]*175+flag[14]*5+flag[15]*350+flag[16]*32+flag[17]*218+flag[18]*304+flag[19]*391+flag[20]*113+flag[21]*19+flag[22]*342+flag[23]*164+flag[24]*240+flag[25]*289+flag[26]*171+flag[27]*210+flag[28]*363+flag[29]*106+flag[30]*263==637650,
flag[0]*28+flag[1]*365+flag[2]*15+flag[3]*169+flag[4]*0+flag[5]*327+flag[6]*23+flag[7]*303+flag[8]*301+flag[9]*163+flag[10]*170+flag[11]*287+flag[12]*352+flag[13]*72+flag[14]*332+flag[15]*323+flag[16]*1+flag[17]*270+flag[18]*318+flag[19]*308+flag[20]*45+flag[21]*140+flag[22]*65+flag[23]*344+flag[24]*289+flag[25]*385+flag[26]*119+flag[27]*62+flag[28]*169+flag[29]*278+flag[30]*346==572609,
flag[0]*238+flag[1]*385+flag[2]*226+flag[3]*35+flag[4]*383+flag[5]*136+flag[6]*267+flag[7]*348+flag[8]*20+flag[9]*230+flag[10]*43+flag[11]*349+flag[12]*290+flag[13]*146+flag[14]*88+flag[15]*354+flag[16]*158+flag[17]*21+flag[18]*60+flag[19]*208+flag[20]*142+flag[21]*388+flag[22]*281+flag[23]*249+flag[24]*63+flag[25]*9+flag[26]*237+flag[27]*143+flag[28]*88+flag[29]*147+flag[30]*343==603481,
flag[0]*173+flag[1]*206+flag[2]*26+flag[3]*272+flag[4]*348+flag[5]*396+flag[6]*142+flag[7]*313+flag[8]*75+flag[9]*142+flag[10]*364+flag[11]*315+flag[12]*184+flag[13]*296+flag[14]*149+flag[15]*201+flag[16]*355+flag[17]*225+flag[18]*211+flag[19]*326+flag[20]*118+flag[21]*155+flag[22]*144+flag[23]*366+flag[24]*257+flag[25]*159+flag[26]*323+flag[27]*148+flag[28]*24+flag[29]*29+flag[30]*253==664504,
flag[0]*34+flag[1]*62+flag[2]*50+flag[3]*90+flag[4]*186+flag[5]*237+flag[6]*11+flag[7]*225+flag[8]*241+flag[9]*230+flag[10]*331+flag[11]*215+flag[12]*155+flag[13]*82+flag[14]*38+flag[15]*336+flag[16]*252+flag[17]*256+flag[18]*394+flag[19]*14+flag[20]*341+flag[21]*336+flag[22]*36+flag[23]*165+flag[24]*93+flag[25]*175+flag[26]*212+flag[27]*226+flag[28]*305+flag[29]*4+flag[30]*29==473092,
flag[0]*102+flag[1]*109+flag[2]*43+flag[3]*76+flag[4]*303+flag[5]*64+flag[6]*161+flag[7]*155+flag[8]*50+flag[9]*58+flag[10]*118+flag[11]*280+flag[12]*0+flag[13]*28+flag[14]*309+flag[15]*213+flag[16]*317+flag[17]*324+flag[18]*148+flag[19]*256+flag[20]*303+flag[21]*234+flag[22]*303+flag[23]*254+flag[24]*233+flag[25]*62+flag[26]*8+flag[27]*252+flag[28]*216+flag[29]*353+flag[30]*93==497492,
flag[0]*234+flag[1]*261+flag[2]*10+flag[3]*237+flag[4]*338+flag[5]*322+flag[6]*389+flag[7]*298+flag[8]*113+flag[9]*285+flag[10]*392+flag[11]*104+flag[12]*181+flag[13]*345+flag[14]*3+flag[15]*371+flag[16]*219+flag[17]*208+flag[18]*259+flag[19]*278+flag[20]*169+flag[21]*231+flag[22]*123+flag[23]*202+flag[24]*220+flag[25]*274+flag[26]*53+flag[27]*82+flag[28]*148+flag[29]*89+flag[30]*361==659149,
flag[0]*115+flag[1]*141+flag[2]*351+flag[3]*215+flag[4]*380+flag[5]*374+flag[6]*84+flag[7]*310+flag[8]*85+flag[9]*354+flag[10]*82+flag[11]*88+flag[12]*212+flag[13]*239+flag[14]*330+flag[15]*215+flag[16]*155+flag[17]*215+flag[18]*317+flag[19]*264+flag[20]*371+flag[21]*300+flag[22]*58+flag[23]*69+flag[24]*137+flag[25]*69+flag[26]*315+flag[27]*93+flag[28]*359+flag[29]*361+flag[30]*108==629123]
s.add(x)
s.add(flag[0]==ord("m"))
s.check()
m=s.model()
m = s.model()
for i in range(len(m)):
    print(chr(int(str(m[flag[i]]))),end="")

这里的脚本设置未知列表是用Int类型的数据，而且等式的数据跟IDA中的有些不一样，前面的脚本应该更符合正常做法，后面这个脚本等式数据应该被处理过了。