HGAME 2019 week3

闲来无事吧week3的wp写一下
week3总体来说难度没有week2大？？？
// 除了那道helloweb，第一次遇见没写出来
//而且反编译后有上万行的代码实在是看不下去了。。。

Math 简单

很明显用z3去写啊
放进ida里复制一下关键函数代码就行
那个。。。因为原来题目链接挂了，这边我直接上代码

# -*- coding: UTF-8 -*-
from z3 import *
s = Solver()
v34 = [BitVec('u%d'%i,8) for i in range(32)]

s.add(v34[0]==ord('h'))
s.add(v34[1]==ord('g'))
s.add(v34[2]==ord('a'))
s.add(v34[3]==ord('m'))
s.add(v34[4]==ord('e'))
s.add(v34[5]==ord('{'))
s.add(v34[31]==ord('}'))



s.add(82 * v34[16] + 58 * v34[25] + 76 * v34[21] + 31 * v34[9] + 87 * v34[28] + 54 * v34[2] + 74 * v34[5] + 99 * v34[26]+ 94 * v34[3] + 84 * v34[19] + 32 * v34[15] + 90 * v34[27] + 16 * v34[14] + 19 * v34[8] + 33 * v34[20] + 35 * v34[31] + 65 * v34[29] + 47 * v34[12] + 3 * v34[1] + 57 * v34[7] + 5 * v34[17] + 70 * v34[13] + 28 * v34[24] + 79 * v34[11] + 63 * v34[23] + 66 * v34[30] + 28 * v34[10] + v34[4] + 81 * v34[6] + 61 * v34[18] + 31 * v34[22] + 71 * v34[0] == 145397)
s.add(55 * v34[6] + 38 * v34[9] + 39 * v34[18] + 73 * v34[24] + 86 * v34[13] + 18 * v34[11] + 40 * v34[21] + 40 * v34[26] + 54 * v34[14] + 81 * v34[10] + 71 * v34[27] + 20 * v34[8] + 16 * v34[28] + 65 * v34[30] + 87 * v34[3] + 14 * v34[16] + v34[5] + 41 * v34[0] + 58 * v34[15] + 73 * v34[2] + 46 * v34[23] + 7 * v34[19] + 89 * v34[17] + 65 * v34[25] + 43 * v34[7] + 6 * v34[20] + 60 * v34[12] + 40 * v34[31] + 57 * v34[29] + 40 * v34[4] + 30 * v34[1] + 63 * v34[22] == 127517)
s.add(28 * v34[6] + 17 * v34[21] + 18 * v34[3] + 53 * v34[10] + 82 * v34[14] + 70 * v34[5] + 84 * v34[2] + 57 * v34[19] + 92 * v34[27] + 57 * v34[11] + 77 * v34[4] + 49 * v34[8] + 62 * v34[29] + 97 * v34[22] + 47 * v34[1] + 30 * v34[16] + 45 * v34[30] + 94 * v34[28] + 6 * v34[9] + 83 * v34[20] + 18 * v34[23] + 97 * v34[15] + 11 * v34[12] + 35 * v34[7] + 81 * v34[26] + 67 * v34[13] + 11 * v34[31] + 84 * v34[24] + 63 * v34[25] + 61 * v34[18] == 141411)
s.add(86 * v34[23] + 52 * v34[1] + 14 * v34[24] + 46 * v34[6] + 56 * v34[7] + 13 * v34[2] + 82 * v34[11] + 49 * v34[30] + 97 * v34[18] + 50 * v34[14] + 83 * v34[27] + 38 * v34[13] + 49 * v34[29] + 9 * v34[4] + 91 * v34[20] + 33 * v34[25] + 4 * v34[22] + 5 * v34[17] + 61 * v34[15] + 65 * v34[3] + 68 * v34[28] + 6 * v34[16] + (v34[8] << 6) + 56 * v34[9] + 67 * v34[10] + 5 * v34[5] + v34[21] + 10 * v34[19] + 83 * v34[12] + 37 * v34[26] + 85 * v34[0] == 117383)
s.add(53 * v34[3] + 91 * v34[2] + 57 * v34[25] + 66 * v34[20] + 9 * v34[28] + 63 * v34[5] + 20 * v34[4] + 96 * v34[8] + 39 * v34[11] + 91 * v34[1] + 40 * v34[9] + 85 * v34[14] + 62 * v34[16] + 95 * v34[19] + 34 * v34[22] + 67 * v34[31] + 51 * v34[27] + 45 * v34[26] + 92 * v34[15] + 91 * v34[21] + 85 * v34[13] + 12 * v34[7] + 26 * v34[23] + 56 * v34[30] + 82 * v34[18] + 72 * v34[17] + 54 * v34[6] + 17 * v34[12] + 84 * v34[29] + 17 * v34[0] + 8 * v34[24] + 63 * v34[10] == 156152)
s.add(55 * v34[23] + 88 * v34[9] + 48 * v34[4] + 83 * v34[13] + 66 * v34[7] + 60 * v34[30] + 57 * v34[6] + 85 * v34[17] + 71 * v34[28] + 98 * v34[24] + 83 * v34[10] + 12 * v34[1] + 72 * v34[31] + 12 * v34[22] + 80 * v34[20] + 15 * v34[19] + 81 * v34[21] + 87 * v34[0] + 37 * v34[16] + 4 * v34[15] + 41 * v34[3] + 84 * v34[26] + 56 * v34[25] + 84 * v34[14] + 41 * v34[27] + 98 * v34[18] + 18 * v34[2] + 95 * v34[11] + 33 * v34[29] + 66 * v34[8] == 148963)
s.add(43 * v34[16] + 47 * v34[0] + 53 * v34[24] + 75 * v34[11] + 57 * v34[21] + 63 * v34[12] + 4 * v34[14] + 59 * v34[31] + 15 * v34[23] + 12 * v34[25] + 58 * v34[5] + 40 * v34[4] + 26 * v34[30] + 8 * v34[15] + 25 * v34[6] + 97 * v34[10] + 12 * v34[28] + 74 * v34[26] + 65 * v34[8] + 93 * v34[27] + 18 * v34[22] + 84 * v34[2] + 7 * v34[1] + 22 * v34[18] + 9 * v34[17] + 89 * v34[19] + 72 * v34[13] + 47 * v34[20] + 7 * v34[29] + 8 * v34[9] + 24 * v34[7] + 75 * v34[3] == 121517)
s.add(77 * v34[30] + 89 * v34[31] + 55 * v34[7] + 86 * v34[17] + 74 * v34[0] + 72 * v34[4] + 27 * v34[20] + 88 * v34[9] + (v34[21] << 6) + 52 * v34[15] + 4 * v34[19] + 8 * v34[1] + 16 * v34[13] + 54 * v34[25] + 8 * v34[29] + 52 * v34[23] + 14 * v34[10] + 88 * v34[18] + 33 * v34[8] + 99 * v34[27] + 65 * v34[14] + 66 * v34[5] + 36 * v34[6] + 58 * v34[16] + 63 * v34[22] + 93 * v34[3] + 96 * v34[11] + 26 * v34[26] + 65 * v34[12] + 42 * v34[28] + 14 * v34[2] + 57 * v34[24] == 151446)
s.add(53 * v34[24] + 95 * v34[27] + 51 * v34[7] + 42 * v34[4] + 78 * v34[8] + 45 * v34[25] + 63 * v34[30] + 85 * v34[26] + 30 * v34[29] + 83 * v34[14] + 62 * v34[31] + 71 * v34[22] + 45 * v34[17] + (v34[6] << 6) + 87 * v34[23] + 49 * v34[28] + 14 * v34[0] + 4 * v34[21] + 63 * v34[5] + 53 * v34[13] + 19 * v34[19] + 44 * v34[16] + 5 * v34[3] + 74 * v34[15] + 19 * v34[18] + 89 * v34[11] + 11 * v34[20] + 34 * v34[12] + 14 * v34[1] + 87 * v34[10] + 63 * v34[9] + 70 * v34[2] == 142830)
s.add(69 * v34[0] + 67 * v34[9] + 57 * v34[15] + 77 * v34[10] + 67 * v34[26] + 94 * v34[11] + 13 * v34[29] + 11 * v34[22] + 41 * v34[5] + 38 * v34[13] + 90 * v34[31] + 68 * v34[7] + 56 * v34[14] + 4 * v34[23] + 66 * v34[28] + 28 * v34[1] + 6 * v34[12] + 91 * v34[16] + 59 * v34[3] + 81 * v34[17] + 44 * v34[2] + 33 * v34[24] + 34 * v34[19] + 17 * v34[18] + 77 * v34[25] + 25 * v34[8] + 8 * v34[6] + 10 * v34[30] + 66 * v34[20] + 41 * v34[27] + 29 * v34[21] == 122585)
s.add(31 * v34[9] + 17 * v34[4] + 6 * v34[28] + 23 * v34[25] + 32 * v34[3] + 72 * v34[15] + 41 * v34[26] + 33 * v34[30] + 82 * v34[13] + 20 * v34[0] + 7 * v34[12] + 25 * v34[29] + 39 * v34[21] + 57 * v34[14] + 14 * v34[16] + 24 * v34[24] + 37 * v34[22] + 71 * v34[10] + 65 * v34[23] + 46 * v34[8] + 40 * v34[19] + 77 * v34[27] + 80 * v34[18] + 88 * v34[6] + 20 * v34[31] + 83 * v34[11] + 73 * v34[1] + 8 * v34[5] + 15 * v34[20] + 70 * v34[7] + 24 * v34[17] + 16 * v34[2] == 105293)
s.add(25 * v34[21] + 79 * v34[3] + 41 * v34[24] + 45 * v34[30] + 82 * v34[20] + 86 * v34[19] + 99 * v34[9] + 96 * v34[22] + 85 * v34[28] + 70 * v34[5] + 77 * v34[23] + 80 * v34[11] + 40 * v34[31] + 66 * v34[12] + 12 * v34[2] + 77 * v34[15] + 72 * v34[4] + 42 * v34[26] + 81 * v34[27] + 90 * v34[13] + 37 * v34[16] + 29 * v34[17] + 20 * v34[29] + 85 * v34[6] + 6 * v34[7] + 2 * v34[0] + 72 * v34[1] + 75 * v34[14] + 40 * v34[25] + 29 * v34[8] + 25 * v34[10] == 151962)
s.add(83 * v34[11] + 75 * v34[1] + 42 * v34[31] + 95 * v34[30] + 58 * v34[8] + 47 * v34[13] + 65 * v34[15] + 24 * v34[17] + 97 * v34[10] + 24 * v34[21] + 28 * v34[0] + 77 * v34[5] + 97 * v34[6] + 24 * v34[26] + 32 * v34[12] + 5 * v34[25] + 55 * v34[28] + 9 * v34[23] + 85 * v34[4] + 6 * v34[9] + 61 * v34[19] + 12 * v34[3] + 76 * v34[7] + 36 * v34[27] + 77 * v34[24] + 24 * v34[29] + 67 * v34[14] + 19 * v34[16] + 47 * v34[20] + 13 * v34[22] == 125609)
s.add(30 * v34[25] + 41 * v34[28] + 65 * v34[10] + v34[1] + 88 * v34[3] + 90 * v34[0] + 4 * v34[23] + 46 * v34[7] + 54 * v34[16] + 16 * v34[6] + 89 * v34[22] + 76 * v34[27] + 38 * v34[17] + 3 * v34[5] + 70 * v34[14] + 3 * v34[24] + 24 * v34[13] + 54 * v34[2] + 20 * v34[8] + 83 * v34[12] + 21 * v34[15] + 77 * v34[18] + 31 * v34[19] + 59 * v34[21] + 33 * v34[20] + 84 * v34[11] + 19 * v34[29] + 38 * v34[26] + 63 * v34[31] + 16 * v34[30] + 15 * v34[4] + 39 * v34[9] == 123069)
s.add(6 * v34[9] + 19 * v34[19] + 27 * v34[18] + 48 * v34[4] + 13 * v34[20] + 44 * v34[10] + 70 * v34[12] + 44 * v34[17] + 22 * v34[23] + 55 * v34[14] + 73 * v34[26] + 55 * v34[8] + 58 * v34[11] + 31 * v34[30] + 78 * v34[29] + 19 * v34[25] + 52 * v34[31] + 27 * v34[21] + 38 * v34[27] + 40 * v34[28] + 35 * v34[1] + 48 * v34[22] + 71 * v34[15] + 24 * v34[6] + 89 * v34[16] + 37 * v34[3] + 78 * v34[2] + 3 * v34[5] + 52 * v34[24] + 40 * v34[7] == 113842)
s.add(95 * v34[8] + 92 * v34[18] + 84 * v34[31] + 31 * v34[12] + 35 * v34[10] + 54 * v34[20] + 26 * v34[29] + 29 * v34[3] + 2 * v34[23] + 46 * v34[0] + 30 * v34[26] + 56 * v34[27] + 100 * v34[11] + 43 * v34[1] + 15 * v34[4] + 79 * v34[17] + 12 * v34[5] + 38 * v34[9] + 3 * v34[30] + 16 * v34[21] + 19 * v34[13] + 67 * v34[19] + 37 * v34[28] + v34[7] + 73 * v34[16] + 85 * v34[6] + 17 * v34[14] + 90 * v34[22] + 15 * v34[2] + 43 * v34[25] + 96 * v34[24] == 119824)
s.add(36 * v34[22] + 69 * v34[28] + 77 * v34[6] + 92 * v34[20] + 43 * v34[23] + 16 * v34[19] + 92 * v34[5] + 49 * v34[26] + 44 * v34[2] + 26 * v34[29] + (v34[25] << 6) + 45 * v34[24] + 99 * v34[11] + 43 * v34[4] + 75 * v34[21] + 53 * v34[31] + 18 * v34[18] + 11 * v34[13] + 52 * v34[0] + 16 * v34[8] + 9 * v34[7] + 77 * v34[16] + 33 * v34[10] + 86 * v34[1] + 33 * v34[3] + 29 * v34[9] + 6 * v34[12] + 91 * v34[14] + 36 * v34[15] + 94 * v34[27] + 13 * v34[30] + 89 * v34[17] == 135873)
s.add(16 * v34[7] + v34[15] + 82 * v34[9] + 60 * v34[29] + 68 * v34[2] + 83 * v34[10] + 47 * v34[5] + 85 * v34[13] + 22 * v34[8] + 92 * v34[27] + 75 * v34[28] + 43 * v34[3] + 29 * v34[22] + 92 * v34[0] + 54 * v34[16] + 17 * v34[30] + 78 * v34[18] + 7 * v34[23] + 69 * v34[21] + 63 * v34[31] + 71 * v34[4] + 10 * v34[6] + 66 * v34[14] + 25 * v34[26] + 32 * v34[1] + 48 * v34[19] + 86 * v34[11] + 20 * v34[25] + 78 * v34[20] + 25 * v34[17] + 76 * v34[12] + 13 * v34[24] == 142509)
s.add(88 * v34[22] + 23 * v34[13] + 18 * v34[14] + 77 * v34[9] + 56 * v34[30] + 79 * v34[2] + 71 * v34[29] + 95 * v34[28] + 87 * v34[24] + 62 * v34[16] + 85 * v34[26] + 43 * v34[20] + 67 * v34[15] + 97 * v34[8] + 80 * v34[0] + 23 * v34[3] + 95 * v34[25] + 82 * v34[21] + 66 * v34[31] + 5 * v34[4] + 66 * v34[27] + 25 * v34[12] + 4 * v34[5] + 12 * v34[7] + 85 * v34[1] + 10 * v34[6] + 45 * v34[11] + 28 * v34[18] + 26 * v34[19] + 48 * v34[23] + 45 * v34[17] == 148888)
s.add(25 * v34[8] + 81 * v34[30] + 21 * v34[6] + 72 * v34[11] + 48 * v34[18] + 2 * v34[19] + 42 * v34[10] + 22 * v34[24] + 99 * v34[2] + 78 * v34[22] + 83 * v34[12] + 60 * v34[9] + 59 * v34[13] + 15 * v34[5] + 25 * v34[20] + 43 * v34[15] + 56 * v34[28] + 33 * v34[25] + 71 * v34[23] + 31 * v34[0] + 95 * v34[3] + 73 * v34[17] + 86 * v34[14] + 15 * v34[21] + 61 * v34[7] + 12 * v34[29] + 95 * v34[26] + 13 * v34[1] + 100 * v34[16] + 11 * v34[4] + 79 * v34[27] == 138023)
s.add(37 * v34[28] + 62 * v34[25] + 42 * v34[18] + 53 * v34[27] + 52 * v34[29] + 70 * v34[22] + 35 * v34[30] + 50 * v34[16] + 59 * v34[8] + 75 * v34[10] + 55 * v34[20] + 23 * v34[0] + 52 * v34[17] + 47 * v34[3] + 91 * v34[13] + 46 * v34[7] + 42 * v34[14] + 79 * v34[26] + 87 * v34[21] + 30 * v34[6] + 26 * v34[1] + 57 * v34[31] + 33 * v34[12] + 51 * v34[9] + 56 * v34[24] + 59 * v34[11] + 36 * v34[23] + 88 * v34[4] + 28 * v34[2] + 44 * v34[15] + 19 * v34[19] + 74 * v34[5] == 142299)
s.add(80 * v34[21] + 43 * v34[31] + 67 * v34[16] + 55 * v34[13] + 95 * v34[24] + 46 * v34[28] + 93 * v34[5] + 75 * v34[20] + 14 * v34[25] + 24 * v34[26] + 50 * v34[29] + 70 * v34[15] + 63 * v34[30] + 77 * v34[23] + 96 * v34[19] + 66 * v34[11] + 72 * v34[27] + 94 * v34[4] + 63 * v34[22] + 69 * v34[3] + 73 * v34[1] + 60 * v34[7] + 9 * v34[2] + 39 * v34[17] + 25 * v34[0] + 49 * v34[14] + 48 * v34[8] + 86 * v34[9] + 72 * v34[10] + 23 * v34[18] + 21 * v34[6] == 155777)
s.add(25 * v34[24] + 11 * v34[22] + 27 * v34[11] + 40 * v34[8] + 53 * v34[15] + 40 * v34[18] + 56 * v34[3] + 2 * v34[2] + 32 * v34[4] + 90 * v34[1] + 54 * v34[16] + 20 * v34[9] + 86 * v34[17] + 82 * v34[31] + 43 * v34[25] + 43 * v34[13] + 86 * v34[21] + 17 * v34[0] + (v34[14] << 6) + 6 * v34[30] + 86 * v34[5] + 15 * v34[7] + 46 * v34[12] + 21 * v34[26] + 90 * v34[20] + 19 * v34[6] + 93 * v34[23] + 31 * v34[27] + 62 * v34[29] + 21 * v34[19] + 42 * v34[10] == 117687)
s.add(89 * v34[21] + 100 * v34[13] + v34[27] + 66 * v34[18] + 40 * v34[17] + 17 * v34[0] + 27 * v34[19] + 26 * v34[31] + 57 * v34[24] + 35 * v34[3] + 80 * v34[1] + 67 * v34[5] + 85 * v34[6] + 7 * v34[15] + 93 * v34[8] + 3 * v34[22] + 77 * v34[12] + 12 * v34[28] + 4 * v34[2] + 27 * v34[9] + 53 * v34[25] + 37 * v34[30] + 43 * v34[23] + 33 * v34[4] + 39 * v34[26] + 7 * v34[7] + 75 * v34[10] + 15 * v34[14] + 45 * v34[20] + 36 * v34[29] + 78 * v34[11] + 31 * v34[16] == 117383)
s.add(73 * v34[20] + 16 * v34[26] + 100 * v34[5] + 71 * v34[28] + 71 * v34[16] + 4 * v34[1] + 77 * v34[31] + 83 * v34[2] + 11 * v34[30] + 53 * v34[19] + 85 * v34[12] + 67 * v34[13] + 39 * v34[8] + 45 * v34[24] + 84 * v34[22] + 99 * v34[14] + 38 * v34[3] + 29 * v34[4] + 90 * v34[9] + 61 * v34[18] + 40 * v34[7] + (v34[17] << 6) + 9 * v34[25] + 86 * v34[29] + 80 * v34[21] + 4 * v34[15] + 96 * v34[23] + 99 * v34[10] + 40 * v34[27] + 4 * v34[0] + 56 * v34[11] == 155741)
s.add((v34[12] << 6) + 76 * v34[0] + 5 * v34[11] + 87 * v34[2] + 86 * v34[24] + 76 * v34[14] + 38 * v34[23] + 85 * v34[3] + 71 * v34[22] + 42 * v34[29] + 85 * v34[30] + 14 * v34[10] + 17 * v34[13] + 42 * v34[25] + 11 * v34[19] + 44 * v34[15] + 21 * v34[4] + 60 * v34[16] + 28 * v34[6] + 46 * v34[20] + 25 * v34[9] + 77 * v34[31] + 21 * v34[8] + 85 * v34[7] + 36 * v34[1] + 91 * v34[27] + 21 * v34[28] + 38 * v34[17] + 3 * v34[26] + 61 * v34[21] + 15 * v34[5] + 32 * v34[18] == 132804)
s.add(95 * v34[30] + 75 * v34[28] + 3 * v34[10] + 36 * v34[1] + 60 * v34[3] + 84 * v34[11] + 19 * v34[26] + 76 * v34[27] + 86 * v34[16] + 92 * v34[8] + 96 * v34[14] + 60 * v34[21] + 23 * v34[4] + 60 * v34[12] + 50 * v34[23] + 78 * v34[22] + 45 * v34[9] + 42 * v34[18] + 10 * v34[2] + 60 * v34[20] + 24 * v34[24] + 77 * v34[7] + 41 * v34[6] + 29 * v34[13] + 33 * v34[5] + 2 * v34[15] + 33 * v34[29] + 39 * v34[31] + 41 * v34[25] + 100 * v34[19] + 9 * v34[17] + 79 * v34[0] == 145568)
s.add(68 * v34[5] + 98 * v34[27] + 98 * v34[16] + 10 * v34[19] + 25 * v34[26] + 98 * v34[24] + 15 * v34[6] + 50 * v34[18] + 88 * v34[20] + 74 * v34[11] + 83 * v34[1] + 86 * v34[21] + 52 * v34[7] + 39 * v34[10] + 40 * v34[13] + 82 * v34[28] + 37 * v34[3] + 45 * v34[0] + 18 * v34[25] + 2 * v34[29] + 6 * v34[12] + 78 * v34[31] + 37 * v34[2] + 57 * v34[23] + 3 * v34[4] + 59 * v34[8] + 73 * v34[15] + v34[22] + 18 * v34[9] + 35 * v34[14] + 20 * v34[17] + 54 * v34[30] == 130175)
s.add(60 * v34[10] + 50 * v34[12] + 30 * v34[29] + 90 * v34[19] + 68 * v34[23] + 60 * v34[18] + 93 * v34[20] + 100 * v34[11] + 98 * v34[14] + 32 * v34[3] + 15 * v34[21] + 79 * v34[0] + 6 * v34[24] + 62 * v34[26] + 96 * v34[6] + 68 * v34[22] + 9 * v34[7] + 88 * v34[5] + 18 * v34[27] + 70 * v34[9] + 96 * v34[25] + 89 * v34[4] + 14 * v34[31] + 83 * v34[17] + 19 * v34[15] + 44 * v34[1] + 96 * v34[8] + 87 * v34[16] + 48 * v34[2] + 95 * v34[13] + 73 * v34[28] + 92 * v34[30] == 171986)
s.add(53 * v34[30] + 87 * v34[25] + 23 * v34[29] + 80 * v34[20] + 86 * v34[9] + 20 * v34[7] + 29 * v34[16] + 31 * v34[14] + 83 * v34[26] + 11 * v34[4] + 29 * v34[19] + 82 * v34[13] + 84 * v34[10] + 70 * v34[1] + 52 * v34[12] + 40 * v34[6] + 91 * v34[8] + 6 * v34[17] + 77 * v34[28] + 56 * v34[5] + 86 * v34[23] + 63 * v34[31] + 26 * v34[27] + 19 * v34[22] + 50 * v34[3] + 15 * v34[15] + 67 * v34[2] + 37 * v34[24] + 84 * v34[18] + 81 * v34[21] + 93 * v34[0] == 151676)
s.add(29 * v34[3] + 93 * v34[5] + 67 * v34[21] + 12 * v34[11] + 82 * v34[24] + 100 * v34[8] + 29 * v34[26] + 97 * v34[12] + 32 * v34[6] + 26 * v34[27] + 46 * v34[19] + 8 * (v34[25] + 9 * v34[0] + 2 * v34[17]) + 63 * v34[10] + 39 * v34[29] + 81 * v34[15] + 51 * v34[13] + 31 * v34[30] + 49 * v34[4] + 3 * v34[22] + 26 * v34[28] + 15 * v34[20] + 89 * v34[2] + 5 * v34[31] + 47 * v34[18] + 19 * v34[23] + 98 * v34[9] + 15 * v34[16] + 49 * v34[1] == 128223)
s.add(13 * v34[14] + 73 * v34[19] + 99 * v34[7] + 76 * v34[12] + 84 * v34[25] + 91 * v34[10] + 67 * v34[22] + 77 * v34[15] + 23 * v34[26] + 38 * v34[4] + 3 * v34[31] + 76 * v34[13] + 50 * v34[0] + 74 * v34[11] + 45 * v34[28] + 58 * v34[29] + 39 * v34[5] + 95 * v34[9] + 26 * v34[16] + 23 * v34[8] + 28 * v34[24] + 89 * v34[1] + 88 * v34[18] + 3 * v34[3] + 59 * v34[20] + 80 * v34[23] + 49 * v34[17] + 56 * v34[21] + 32 * v34[27] + 24 * v34[2] + 77 * v34[30] + 18 * v34[6] == 138403)

flag = ''
print s.check()
print s.model()
if s.check() == sat:
    print s.model()
    result = s.model()
    for i in range(32):
        flag += chr(result[v34[i]].as_long().real)
    print flag

跑一下就行

Say-Muggle-Code a.k.a. SMC

自我感觉这题比上周的smc简单 //手动滑稽
拖进ida，因为是c艹，看起来有点难受

所以只能调试了
发现前面一大段程序主要是确定输入的数目是否为39
还有就是使用hgame{}开头结尾
真正的check在下面

点击check1查看，check1是比较简单的

直接解出来前半部分

a = [0xDE, 0xD1, 0xD8, 0x8C, 0x8F, 0xD9, 0xDF, 0xDE, 0xDF, 0x8C,
  0xD8, 0xDA, 0x8C, 0xDC, 0xDD, 0xD8]
flag = ''
for i in range(len(a)):
    flag += chr(a[i]^0xe9)
print flag          #781ef0676e13e541

然后就是check2了，也就是本题的难点

可以看到encrypt是一段数据，看汇编发现程序call了encrypt函数
那就很容易想到这边的代码段被加密过，调试发现是机器码与数值异或
运行时再进行解密，所以静态分析失败
只能调试了
跟进encrypt函数

这是一个魔改过的TEA
不难 //但确实折腾了我好久，c语言的有些运算很奇葩
//和17届x1c面试题目差不多，但肯定没那个难
复制下伪代码就行
代码如下
头文件ida.h啥的自己加好了

_DWORD *__fastcall encrypt(__int64 a1, _DWORD *a2);
int main()
{
    int i;
    char a[]={0xDB, 0xAA, 0x8E, 0x1E, 0x3A, 0xC6, 0xA9, 0x11, 0xF0, 0xA4,
  0xB8, 0x71, 0x03, 0x71, 0x55, 0x3E};
  char a2[]={0x37, 0x0F, 0x09, 0x54, 0x03, 0x56, 0x06, 0x01, 0x01, 0x53,
  0x54, 0x02, 0x56, 0x50, 0x01, 0x05};
  encrypt((__int64)a, (_DWORD *)a2);
  for(i=0;i<16;i++)
  {
      printf("%c",a[i]);            //63930b609a7da803
  }
    return 0;
}
_DWORD *__fastcall encrypt(__int64 a1, _DWORD *a2)
{
  _DWORD *result; // rax
  int v3; // [rsp+10h] [rbp-10h]
  signed int i; // [rsp+14h] [rbp-Ch]
  signed int j; // [rsp+18h] [rbp-8h]

  v3 = 0;
  for ( i = 0; i <= 31; ++i )
    v3 -= 1640531527;
  for ( i = 0; i <= 31; ++i )
  {
    result = (_DWORD *)2654435769LL;
    for ( j = 0; j <= 3; j += 2 )
    {
        result = (_DWORD *)(4 * (j + 1LL) + a1);
      *result -= (*(_DWORD *)(4LL * j + a1) + v3) ^ (16 * *(_DWORD *)(4LL * j + a1) + a2[2]) ^ ((*(_DWORD *)(4LL * j + a1) >> 5)
                                                                                              + a2[3]);
      *(_DWORD *)(a1 + 4LL * j) = *(_DWORD *)(4LL * j + a1)
                                - ((*(_DWORD *)(4 * (j + 1LL) + a1) + v3) ^ (16 * *(_DWORD *)(4 * (j + 1LL) + a1) + *a2) ^ ((*(_DWORD *)(4 * (j + 1LL) + a1) >> 5) + a2[1]));
    }
  v3 += 1640531527;
  }
  return result;
}

hgame{781ef0676e13e54163930b609a7da803}
题目出的挺好的，加深了对smc的理解
还有一些加密算法也能复习一下