hgame
re方向的，太菜了，很多题都做不来。
week1
helloRe
ida打开，通过动调找到加密位置，也不能完全动调样，会出一些问题。
脚本如下
#include<stdio.h>
int main(void)
{
int code[23]={ 0x97, 0x99, 0x9C, 0x91, 0x9E, 0x81, 0x91, 0x9D, 0x9B, 0x9A,
0x9A, 0xAB, 0x81, 0x97, 0xAE, 0x80, 0x83, 0x8F, 0x94, 0x89, 0x99, 0x97};
int key[23]={0xff,0xfe,0xfd,0xfc,0xfb,0xfa,0xf9,0xf8,0xf7,0xf6,0xf5,0xf4,0xf3,0xf2,0xf1,
0xf0,0xef,0xee,0xed,0xec,0xeb,0xea};
int i;
for(i=0;i<22;i++)
{
printf("%c",code[i]^key[i]);
}
}得到hgame{hello_re_player}
pypy
打开网页出现的是python的字节码，了解一下字节码https://zhuanlan.zhihu.com/p/45101508
4 0 LOAD_GLOBAL 0 (input)
2 LOAD_CONST 1 ('give me your flag:\n')
4 CALL_FUNCTION 1
6 STORE_FAST 0 (raw_flag)
5 8 LOAD_GLOBAL 1 (list)
10 LOAD_FAST 0 (raw_flag)
12 LOAD_CONST 2 (6)
14 LOAD_CONST 3 (-1)
16 BUILD_SLICE 2
18 BINARY_SUBSCR
20 CALL_FUNCTION 1
22 STORE_FAST 1 (cipher)
6 24 LOAD_GLOBAL 2 (len)
26 LOAD_FAST 1 (cipher)
28 CALL_FUNCTION 1
30 STORE_FAST 2 (length)
8 32 LOAD_GLOBAL 3 (range)
34 LOAD_FAST 2 (length)
36 LOAD_CONST 4 (2)
38 BINARY_FLOOR_DIVIDE
40 CALL_FUNCTION 1
42 GET_ITER
>> 44 FOR_ITER 54 (to 100)
46 STORE_FAST 3 (i)
9 48 LOAD_FAST 1 (cipher)
50 LOAD_CONST 4 (2)
52 LOAD_FAST 3 (i)
54 BINARY_MULTIPLY
56 LOAD_CONST 5 (1)
58 BINARY_ADD
60 BINARY_SUBSCR
62 LOAD_FAST 1 (cipher)
64 LOAD_CONST 4 (2)
66 LOAD_FAST 3 (i)
68 BINARY_MULTIPLY
70 BINARY_SUBSCR
72 ROT_TWO
74 LOAD_FAST 1 (cipher)
76 LOAD_CONST 4 (2)
78 LOAD_FAST 3 (i)
80 BINARY_MULTIPLY
82 STORE_SUBSCR
84 LOAD_FAST 1 (cipher)
86 LOAD_CONST 4 (2)
88 LOAD_FAST 3 (i)
90 BINARY_MULTIPLY
92 LOAD_CONST 5 (1)
94 BINARY_ADD
96 STORE_SUBSCR
98 JUMP_ABSOLUTE 44
12 >> 100 BUILD_LIST 0
102 STORE_FAST 4 (res)
13 104 LOAD_GLOBAL 3 (range)
106 LOAD_FAST 2 (length)
108 CALL_FUNCTION 1
110 GET_ITER
>> 112 FOR_ITER 26 (to 140)
114 STORE_FAST 3 (i)
14 116 LOAD_FAST 4 (res)
118 LOAD_METHOD 4 (append)
120 LOAD_GLOBAL 5 (ord)
122 LOAD_FAST 1 (cipher)
124 LOAD_FAST 3 (i)
126 BINARY_SUBSCR
128 CALL_FUNCTION 1
130 LOAD_FAST 3 (i)
132 BINARY_XOR
134 CALL_METHOD 1
136 POP_TOP
138 JUMP_ABSOLUTE 112
15 >> 140 LOAD_GLOBAL 6 (bytes)
142 LOAD_FAST 4 (res)
144 CALL_FUNCTION 1
146 LOAD_METHOD 7 (hex)
148 CALL_METHOD 0
150 STORE_FAST 4 (res)
16 152 LOAD_GLOBAL 8 (print)
154 LOAD_CONST 6 ('your flag: ')
156 LOAD_FAST 4 (res)
158 BINARY_ADD
160 CALL_FUNCTION 1
162 POP_TOP
164 LOAD_CONST 0 (None)
166 RETURN_VALUE
# your flag: 30466633346f59213b4139794520572b45514d61583151576638643a大概翻译一下
raw_flag=input('give me your flag:\n')
cipher=list(raw_flag)[6:-1]
lenth=len(chipher)
for i in range(length/2):
chipher[i*2]==chipher[i*2+1]//交换这两个
res=''
for i in range(lenth):
res[i]=ord(cipher[i])^i
hex()写出脚本
import binascii
temp=b'30466633346f59213b4139794520572b45514d61583151576638643a'
temp2=binascii.unhexlify(temp)
code=temp2.decode('utf-8')
chipher=list(code[:-1])
flag=[chr(ord(chipher[i])^i) for i in range(len(chipher))]
for i in range(len(flag)//2):
mid=flag[i*2+1]
flag[i*2+1]=flag[i*2]
flag[i*2]=mid
res=''
for i in flag:
res += i
print('hgame{'+res+'}')得到hgame{G00dj0&H3r3-I$Y@Ur$L@G!~~}
apacha
有谁能拒接阿帕茶的诱惑呢。这道题考了一个xxtea算法，做的时候还不知道。。。。
先大致分析一下主函数
图里面讲错了，是先加密1~34，只是第35个会对第1个产生影响。
再来看看算法部分，就贴一个我自己仿照写的吧
#include<stdio.h>
int main(void)
{
int a3[4]={1,2,3,4};
unsigned int flag[36]={'h', 'g', 'a', 'm', 'e', '{', 'w', 'e', 'f', 'j', 'o', 'z', 'l', 's', 'd', 'i', 'f', 'j', 'i', 'o', 'w', 'e', 'k', 'g', 'k', 'h', 'l', 'k', 'j', 'l', 'd', 'f', 'a', 's', '}'};
// unsigned int v6=0xf1bbcdc8;
unsigned int v6=0;
unsigned int v7;
unsigned int v9=34;
int result;
int i=0;
do
{
v6=v6-0x61C88647;
v7=v6>>2;
i=0;
do
{
if(i==0)
{
flag[i]=(flag[i]+(((flag[34]>>5)^((flag[i+1])*4)) + ((flag[34]<<4)^(flag[i+1]>>3)) ^ ((a3[(i^v7)&3] ^flag[34]) + (flag[i+1]^v6))));
}
else
flag[i]=(flag[i]+(((flag[i-1]>>5)^((flag[i+1])*4)) + ((flag[i-1]<<4)^(flag[i+1]>>3)) ^ ((a3[(i^v7)&3] ^flag[i-1]) + (flag[i+1]^v6))));
i++;
}while(i!=34);
result=(flag[33]<<4)^(flag[0]>>3);
flag[34] = flag[34] + ((((a3[(v9^v7)&3]) ^ flag[33]) + (flag[0]^v6)) ^ (((flag[0]*4)^(flag[33]>>5))+result));
}while(v6!=0x5384540F);
for(i=0;i<35;i++)
{
printf("%#x ",flag[i]);
if((i+1)%4==0)
{
printf("\n");
}
}
}当时还以为反解不了(认为反解会有两个未知变量)，然后网上找了一个脚本，后头突然才想起可以反解，想错了一个地方。
然后就给一个网上的脚本来解吧，看起确实比较简洁。
#include <stdio.h>
#include <stdint.h>
#define DELTA 0x9e3779b9
#define MX (((z>>5^y<<2) + (y>>3^z<<4)) ^ ((sum^y) + (key[(p&3)^e] ^ z)))
void btea(uint32_t *v, int n, uint32_t const key[4])
{
uint32_t y, z, sum;
unsigned p, rounds, e;
if (n > 1) /* Coding Part */
{
rounds = 6 + 52/n;
sum = 0;
z = v[n-1];
do
{
sum += DELTA;
e = (sum >> 2) & 3;
for (p=0; p<n-1; p++)
{
y = v[p+1];
z = v[p] += MX;
}
y = v[0];
z = v[n-1] += MX;
}
while (--rounds);
}
else if (n < -1) /* Decoding Part */
{
n = -n;
rounds = 6 + 52/n;
sum = rounds*DELTA;
y = v[0];
do
{
e = (sum >> 2) & 3;
for (p=n-1; p>0; p--)
{
z = v[p-1];
y = v[p] -= MX;
}
z = v[n-1];
y = v[0] -= MX;
sum -= DELTA;
}
while (--rounds);
}
}
int main()
{
uint32_t v[35]= {0xE74EB323,0xB7A72836,0x59CA6Fe2,0x967CC5C1,0xE7802674,0x3D2D54E6,
0x8A9D0356,0x99DCC39C,0x7026D8ED,0x6A33FDAD,0xF496550A,0x5C9C6F9E,0x1BE5D04C,
0x6723AE17,0x5270A5C2,0xAC42130A,0x84BE67B2,0x705CC779,0x5C513D98,0xFB36DA2D,
0x22179645,0x5CE3529D,0xD189E1FB,0xE85BD489,0x73C8D11F,0x54B5C196,0xB67CB490,
0x2117E4CA,0x9DE3F994,0x2F5AA1AA,0xA7E801FD,0xC30D6EAB,0x1BADDC9C,0x3453B04A,
0x92A406F9};
uint32_t const k[4]= {1,2,3,4};
int n= 35; //n的绝对值表示v的长度，取正表示加密，取负表示解密
// v为要加密的数据是两个32位无符号整数
// k为加密解密密钥，为4个32位无符号整数，即密钥长度为128位
//printf("加密前原始数据：%u %u\n",v[0],v[1]);
//ea(v, n, k);
//printf("加密后的数据：%u %u\n",v[0],v[1]);
btea(v, -n, k);
for(int i=0;i<35;i++)
printf("%c",v[i]);
return 0;
}得到hgame{l00ks_1ike_y0u_f0Und_th3_t34}
week2
ezApk
AES的CBC模式，就是key，和iv需要转换一下，但是我用网站解密不知道为什么只有一半。。。
jeb打开，找到关键代码
在线网站解就行了,我用的这个https://the-x.cn/cryptography/Aes.aspx，其他感觉有点小毛病不支持hex
helloRe2
考察动调和windowsAPI的AES加密吧。之前没遇到过，只知道第二个加密是AES，但是找不到key，和iv。
第一个加密，看wp好像说是题出了点问题，导致简单了，动调一下就知道在这个这里的比较部分。
第二个加密就是AES加密了
1.key就是password1分别和00x0F异或，需要注意的是有一个反调试。0x0F
2.iv就是0
3.密文
然后网站解密
拼接一下得到flag{2b0c5e6a3a20b189_7a4ad6c5671fb313}
fake_debugger beta
一个端口题，没做起，不知道怎么弄。看了wp才知道，居然可以按空格一步步调试，然后环境已经关了，就没做了。
week3
FAKE
考了SMC，和z3约束器吧，倒是解决了我以前遗留的一些问题。
ida，看起很简单，于是就做错了。
下面是用z3解的，长的一批，哭了。
from z3 import *
s = Solver()
v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15,v16,v17,v18,v19,v20,v21,v22,v23,v24,v25,v26,v27,v28,v29,v30,v31,v32,v33,v34,v35,v36=Ints('v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24 v25 v26 v27 v28 v29 v30 v31 v32 v33 v34 v35 v36')
a1 = [0]*36
for i in range(36):
a1[i] = Int('a1['+str(i)+']')
s.add(v1 == -19 * a1[4]
+ 88 * a1[25]
+ -7 * a1[30]
+ a1[27]
+ -33 * a1[20]
+ -23 * a1[23]
+ 90 * a1[14]
+ -99 * a1[10]
+ 30 * a1[29]
+ -37 * a1[1]
+ -58 * a1[33]
+ 17 * a1[7]
+ 26 * a1[31]
+ -20 * a1[12]
+ -56 * a1[26]
+ 70 * a1[19]
+ 29 * a1[0]
+ -42 * a1[17]
+ 67 * a1[35]
+ 11 * a1[6]
+ 66 * a1[15]
+ 53 * a1[11]
- 53 * a1[3]
+ 63 * a1[32]
- 65 * a1[21]
+ 9 * a1[9]
- 50 * a1[28]
- 48 * a1[8]
- 70 * a1[22]
+ 48 * a1[13]
- 68 * a1[34]
- 14 * a1[5])
s.add(-35 * a1[2] + 89 * a1[24] + -49 * a1[16] + v1 - 67 * a1[18] == -874)
s.add(v2 == -41 * a1[25]
+ -47 * a1[16]
+ a1[14]
+ 67 * a1[34]
+ -20 * a1[1]
+ 47 * a1[33]
+ -79 * a1[19]
+ -17 * a1[6]
+ (30 * a1[5])
+ (a1[18] *64)
+ (-57 * a1[15])
+ 90 * a1[21]
+ 57 * a1[4]
+ -63 * a1[13]
+ 13 * a1[2]
+ 10 * a1[35]
+ -56 * a1[8]
+ 56 * a1[31]
+ -40 * a1[0]
+ -91 * a1[27]
+ 57 * a1[23]
+ 62 * a1[10]
+ 90 * a1[9]
+ -92 * a1[17]
+ -5 * a1[29]
+ 60 * a1[22]
- 13 * a1[12]
+ 5 * a1[28]
- 63 * a1[32]
+ 5 * a1[26]
+ 70 * a1[3]
+ 41 * a1[7])
s.add(v2 + 71 * a1[24] + 15 * a1[11] + 42 * a1[20] == 21163)
s.add( v3 == 50 * a1[20]
+ 88 * a1[35]
+ 49 * a1[1]
+ 34 * a1[23]
+ 58 * a1[29]
+ 69 * a1[24]
+ 28 * a1[13]
+ 77 * a1[19]
+ 2 * a1[7]
+ -53 * a1[10]
+ -61 * a1[4]
+ 12 * a1[17]
+ 93 * a1[11]
+ -13 * a1[32]
+ 53 * a1[9]
+ 29 * a1[16]
+ -77 * a1[14]
+ 77 * a1[33]
+ 74 * a1[34]
+ -100 * a1[30]
- 99 * a1[27]
- 87 * a1[25]
+ 36 * a1[6]
+ 59 * a1[3]
+ 81 * a1[21]
+ 28 * a1[28]
+ 7 * a1[0]
+ 54 * a1[22]
- 5 * a1[31]
- 41 * a1[2]
+ 5 * a1[18]
- 93 * a1[15])
s.add( 73 * a1[26] + v3 + 10 * a1[12] - 27 * a1[8] + 24 * a1[5] == 45615)
s.add(v4 == 53 * a1[21]
+ 51 * a1[13]
+ 58 * a1[17]
+ -52 * a1[10]
+ -77 * a1[7]
+ 86 * a1[11]
+ -77 * a1[16]
+ -100 * a1[18]
+ -61 * a1[2]
+ -46 * a1[20]
+ -61 * a1[6]
+ -46 * a1[19]
+ 51 * a1[4]
+ -76 * a1[34]
+ -17 * a1[31]
+ 8 * a1[28]
+ 94 * a1[30]
+ 23 * a1[8]
+ -61 * a1[29]
+ -52 * a1[35]
+ 81 * a1[33]
+ -44 * a1[1]
+ 75 * a1[32]
+ -9 * a1[24]
- 96 * a1[12]
+ 5 * a1[26]
+ 2 * a1[25]
+ 31 * a1[22]
+ 43 * a1[15]
- 2 * a1[0]
- 92 * a1[14]
+ 13 * a1[5])
s.add(-17 * a1[23] + v4 - 99 * a1[3] + 63 * a1[27] + 8 * a1[9] == -37017)
s.add(v5 == 91 * a1[0]
+ -43 * a1[32]
+ 17 * a1[13]
+ 9 * a1[15]
+ (a1[1] *64)
+ 9 * a1[16]
+ 59 * a1[3]
+ -29 * a1[14]
+ 32 * a1[18]
+ -69 * a1[26]
+ -81 * a1[33]
+ -69 * a1[9]
+ 60 * a1[19]
+ -35 * a1[21]
+ 40 * a1[11]
+ -44 * a1[7]
+ 78 * a1[22]
+ 68 * a1[28]
+ 70 * a1[29]
+ 3 * a1[2]
+ 61 * a1[6]
+ 37 * a1[35]
- 36 * a1[27]
+ 40 * a1[34]
+ 23 * a1[17]
+ 81 * a1[12]
+ 69 * a1[30]
- 9 * a1[23]
- 75 * a1[25]
- 62 * a1[20]
+ 56 * a1[31]
+ 96 * a1[5])
s.add( -25 * a1[4] + v5 + 69 * a1[8] + 80 * a1[10] + 99 * a1[24] == 72092)
s.add(v6 == -76 * a1[28]
+ 48 * a1[18]
+ 93 * a1[1]
+ 66 * a1[29]
+ -86 * a1[27]
+ -3 *a1[0]
+ -79 * a1[26]
+ -20 * a1[8]
+ 90 * a1[6]
+ 6 * a1[30]
+ 47 * a1[16]
+ 50 * a1[20]
+ 51 * a1[23]
+ -13 * a1[33]
+ -86 * a1[13]
+ 32 * a1[31]
+ -89 * a1[2]
+ 79 * a1[11]
+ -41 * a1[7]
+ -56 * a1[14]
+ 54 * a1[19]
- 96 * a1[34]
- 34 * a1[25]
- (a1[4] *64)
- 36 * a1[35]
+ 48 * a1[10]
- 39 * a1[5]
+ 20 * a1[3]
+ 61 * a1[17]
- 56 * a1[15]
- 97 * a1[22]
+ 96 * a1[9])
s.add( 51 * a1[32] + -63 * a1[21] + 78 * a1[24] + v6 - 61 * a1[12] == -27809)
s.add(v7 == -32 * a1[23]
+ -74 * a1[28]
+ 76 * a1[33]
+ 91 * a1[5]
+ 83 * a1[19]
+ 99 * a1[32]
+ 98 * a1[7]
+ 22 * a1[34]
+ 83 * a1[13]
+ -13 * a1[0]
+ -66 * a1[11]
+ -25 * a1[2]
+ -9 * a1[31]
+ 35 * a1[25]
+ 31 * a1[18]
- 95 * a1[21]
+ 37 * a1[22]
- 74 * a1[16]
+ 17 * a1[12]
- 27 * a1[24]
+ 11 * a1[3]
+ 83 * a1[9]
- 60 * a1[27]
+ 77 * a1[20]
+ 96 * a1[15]
- 23 * a1[10])
s.add(-44 * a1[35]
+ -26 * a1[30]
+ -36 * a1[4]
+ (a1[6] *64)
+ -65 * a1[26]
+ -46 * a1[8]
+ -33 * a1[14]
+ -45 * a1[1]
+ v7
- 5 * a1[29]
- 73 * a1[17] == 9604)
s.add(v8 == 82 * a1[8]
+ -88 * a1[3]
+ -26 * a1[11]
+ 76 * a1[1]
+ 69 * a1[27]
+ -51 * a1[14]
+ 78 * a1[33]
+ -11 * a1[18]
+ -83 * a1[5]
+ 70 * a1[20]
+ -36 * a1[22]
+ -57 * a1[31]
+ 32 * a1[25]
+ 55 * a1[16]
+ 42 * a1[24]
+ -93 * a1[26]
+ 69 * a1[17]
+ 84 * a1[12]
+ 9 * a1[23]
+ -34 * a1[32]
+ -84 * a1[2]
+ -18 * a1[7]
+ 60 * a1[29]
- 99 * a1[30]
- a1[0]
+ 24 * a1[21]
- 36 * a1[4]
+ 9 * a1[35]
+ 89 * a1[15]
+ 72 * a1[19]
+ 86 * a1[13]
- 8 * a1[28])
s.add( -79 * a1[10] + v8 + (a1[6] *64) + 19 * a1[9] + 71 * a1[34] == 25498)
s.add(v9 == 65 * a1[32]
+ -62 * a1[34]
+ 79 * a1[10]
+ -82 * a1[27]
+ -16 * a1[29]
+ -60 * a1[1]
+ -80 * a1[15]
+ -54 * a1[2]
+ 75 * a1[6]
+ -31 * a1[17]
+ 29 * a1[12]
+ 28 * a1[28]
+ 57 * a1[14]
+ -68 * a1[4]
+ 86 *a1[0]
+ 82 * a1[13]
+ -20 * a1[11]
+ -18 * a1[23]
+ 88 * a1[18]
+ -57 * a1[25]
+ 94 * a1[9]
- 51 * a1[5]
- 58 * a1[7]
- 2 * a1[3]
+ 94 * a1[31]
- 6 * a1[21]
- 59 * a1[19]
+ 25 * a1[20]
- 66 * a1[35]
- 62 * a1[24]
+ 89 * a1[26])
s.add(-70 * a1[8] + 50 * a1[30] + 26 * a1[16] + v9 + 12 * a1[22] - 86 * a1[33] == -10472)
s.add(v10 == 30 * a1[10]
+ 72 * a1[8]
+ 72 * a1[29]
+ -49 * a1[34]
+ 83 * a1[18]
+ -63 * a1[0]
+ -88 * a1[4]
+ -91 * a1[20]
+ -11 * a1[17]
+ 38 * a1[3]
+ 53 * a1[35]
+ 31 * a1[5]
+ -75 * a1[22]
+ 14 * a1[26]
+ -7 * a1[24]
+ -7 * a1[31]
+ 77 * a1[23]
+ -46 * a1[6]
+ 47 * a1[19]
+ 48 * a1[33]
+ 74 * a1[1]
- 24 * a1[30]
+ 87 * a1[9]
+ 33 * a1[11]
+ 86 * a1[28]
+ 37 * a1[21]
- 97 * a1[27]
- 30 * a1[13]
- 59 * a1[16]
+ 5 * a1[7]
- 3 * a1[15]
+ 13 * a1[12])
s.add(31 * a1[14] + -11 * a1[2] + v10 - 73 * a1[32] - 56 * a1[25] == 6560)
s.add(v11 == -81 * a1[8]
+ 49 * a1[0]
+ -52 * a1[3]
+ 84 * a1[2]
+ 26 * a1[25]
+ -74 * a1[20]
+ -97 * a1[6]
+ 14 * a1[15]
+ 77 * a1[30]
+ -66 * a1[28]
+ -89 * a1[12]
+ -95 * a1[13]
+ -70 * a1[10]
+ -27 * a1[1]
+ -85 * a1[22]
+ -66 * a1[34]
+ -91 * a1[4]
- 5 * a1[19]
- 94 * a1[29]
- 24 * a1[35]
- 7 * a1[32]
+ 63 * a1[5]
- 49 * a1[14]
- 96 * a1[18]
- 100 * a1[7]
+ 81 * a1[16]
+ 70 * a1[11]
+ 3 * a1[21]
+ 28 * a1[24]
- 14 * a1[9]
+ 59 * a1[17]
+ 24 * a1[31])
s.add(59 * a1[23] + v11 - 25 * a1[27] + 20 * a1[33] - 77 * a1[26] == -69431)
s.add(v12 == 2 * a1[7]
+ 70 * a1[19]
+ 53 * a1[35]
+ 34 * a1[6]
+ 30 * a1[5]
+ 55 * a1[23]
+ 69 * a1[10]
+ 60 * a1[2]
+ -69 * a1[25]
+ 33 * a1[20]
+ 55 * a1[24]
+ 69 * a1[18]
+ 83 * a1[15]
+ -19 * a1[13]
+ 22 * a1[21]
+ a1[16]
+ -53 * a1[22]
+ -58 * a1[4]
+ -63 * a1[29]
- 91 * a1[26]
+ 28 * a1[34]
+ 5 * a1[3]
+ 35 * a1[8]
+ 27 * a1[1]
- 31 * a1[27]
+ 10 * a1[12]
+ 84 * a1[33]
+ 24 * a1[14]
+ 42 * a1[11]
- 2 * a1[17]
+ 68 * a1[32]
+ 21 * a1[0])
s.add(98 * a1[28] + v12 - a1[9] + 60 * a1[31] - 60 * a1[30] == 54106)
s.add( v13 == (a1[18] *64)
+ -61 * a1[15]
+ -92 * a1[13]
+ 50 * a1[8]
+ 90 * a1[29]
+ 32 * a1[4]
+ -97 * a1[27]
+ 14 * a1[14]
+ a1[30]
+ 97 * a1[7]
+ 15 * a1[31]
+ -96 * a1[21]
+ 38 * a1[19]
+ -81 * a1[9]
+ -68 * a1[12]
+ 89 * a1[20]
+ 33 * a1[2]
+ 70 * a1[34]
+ 79 * a1[28]
+ -80 * a1[35]
+ 76 * a1[10]
- 38 * a1[5]
+ 5 * a1[6]
+ 60 * a1[11]
- 8 * a1[26]
- 59 * a1[23]
+ 9 * a1[24]
+ 34 * a1[17]
- 60 * a1[1]
+ 98 * a1[25]
+ 48 * a1[16]
- 17 * a1[32])
s.add(-88 * a1[22] + -96 * a1[3] + v13 - 96 * a1[0] + 54 * a1[33] == -8292)
s.add(v14 == -29 * a1[24]
+ -28 * a1[26]
+ -7 * a1[3]
+ 49 * a1[17]
+ 60 * a1[25]
+ -45 * a1[16]
+ -50 * a1[0]
+ -98 * a1[28]
+ -92 * a1[12]
+ -22 * a1[23]
+ 33 * a1[13]
+ 57 * a1[31]
- 15 * a1[5]
+ 36 * a1[29]
- 88 * a1[15]
+ 12 * a1[21]
+ 71 * a1[14]
- 48 * a1[35]
+ 79 * a1[34]
- 5 * a1[19]
+ 68 * a1[33]
- 2 * a1[4]
- 82 * a1[10]
- 16 * a1[18]
- 98 * a1[22]
- (a1[27] *64)
+ 32 * a1[11]
+ 73 * a1[2]
- 38 * a1[20]
+ 27 * a1[9]
- 7 * a1[7])
s.add( -58 * a1[32] + 53 * a1[8] + -57 * a1[30] + v14 - 30 * a1[1] - 35 * a1[6] == -44677)
s.add(v15 == 91 * a1[15]
+ 91 * a1[8]
+ 58 * a1[16]
+ -91 * a1[23]
+ 4 * a1[31]
+ -43 * a1[18]
+ -36 * a1[29]
+ 60 * a1[14]
+ 29 * a1[20]
+ -85 * a1[19]
+ 71 * a1[27]
+ -22 * a1[11]
+ 95 * a1[9]
+ 19 * a1[12]
+ -20 * a1[30]
+ 6 * a1[34]
+ 49 * a1[6]
+ 13 * a1[10]
- 23 * a1[13]
+ 17 * a1[7]
- 79 * a1[22]
+ 12 * a1[3]
- 7 * a1[4]
- 12 * a1[2]
- 78 * a1[17]
- 56 * a1[5]
+ 59 * a1[26]
+ 18 * a1[32]
- 87 * a1[35]
- 30 * a1[24]
+ 54 * a1[25]
- 5 * a1[1])
s.add(-86 * a1[28] + -69 * a1[33] + -31 * a1[21] + v15 - 94 * a1[0] == -17772)
s.add(v16 == 65 * a1[3]
+ -78 * a1[13]
+ -71 * a1[26]
+ -44 * a1[23]
+ 61 * a1[7]
+ 63 * a1[1]
+ 9 * a1[16]
+ -17 * a1[9]
+ -93 * a1[12]
+ -85 * a1[20]
+ -73 * a1[35]
+ -87 * a1[24]
+ -80 * a1[25]
+ -87 * a1[4]
+ 56 * a1[27]
+ -89 * a1[21]
+ 52 * a1[15]
+ 97 * a1[0]
+ -11 * a1[19]
+ -94 * a1[10]
+ -92 * a1[29]
+ -20 * a1[17]
- 95 * a1[5]
- 13 * a1[8]
+ 80 * a1[31]
- a1[33]
+ 37 * a1[30]
+ (a1[32] *64)
+ 11 * a1[22]
- 39 * a1[14]
+ 80 * a1[6]
- 33 * a1[11])
s.add(-18 * a1[18] + -76 * a1[34] + v16 - 62 * a1[2] - 74 * a1[28] == -77151)
s.add(v17 == -4 * a1[26]
+ 59 * a1[6]
+ -85 * a1[34]
+ 69 * a1[29]
+ 77 * a1[31]
+ -95 * a1[8]
+ 75 * a1[16]
+ 54 * a1[20]
+ 65 * a1[22]
+ -9 * a1[9]
+ -61 * a1[24]
+ -45 * a1[25]
+ 47 * a1[4]
+ 31 * a1[5]
+ 36 * a1[23]
+ 20 * a1[13]
- 40 * a1[2]
- (a1[12] *64)
- 40 * a1[14]
+ 81 * a1[10]
- 35 * a1[0]
- 12 * a1[27]
+ 35 * a1[30]
+ 63 * a1[15]
- 65 * a1[19]
+ 31 * a1[18]
- 42 * a1[35]
+ 33 * a1[11]
- 19 * a1[3]
+ 65 * a1[21]
- 78 * a1[7])
s.add(43 * a1[33] + 76 * a1[32] + v17 - 48 * a1[28] - 77 * a1[17] == 11531)
s.add(v18 == 33 * a1[32]
+ 96 * a1[14]
+ 47 * a1[31]
+ -92 * a1[27]
+ -51 * a1[1]
+ -25 * a1[28]
+ -12 * a1[0]
+ 55 * a1[17]
+ 35 * a1[20]
+ 76 * a1[13]
+ -73 * a1[15]
+ 84 * a1[12]
+ -72 * a1[3]
+ 71 * a1[24]
+ -41 * a1[7]
+ 28 * a1[8]
+ -93 * a1[34]
+ -63 * a1[30]
+ 35 * a1[6]
- 38 * a1[10]
- 4 * a1[16]
+ 99 * a1[11]
+ 10 * a1[4]
- 98 * a1[35]
- 9 * a1[18]
+ 22 * a1[21]
- 6 * a1[26]
+ 82 * a1[2]
- 6 * a1[33]
- 13 * a1[29])
s.add(67 * a1[23] + 95 * a1[5] + -37 * a1[9] + -71 * a1[25] + v18 + 25 * a1[22] - 35 * a1[19] == 4538)
s.add( v19 == -50 * a1[25]
+ -76 * a1[3]
+ -65 * a1[28]
+ -36 * a1[31]
+ 88 * a1[34]
+ 79 * a1[27]
+ 87 * a1[24]
+ -52 * a1[29]
+ -72 * a1[13]
+ -17 * a1[23]
+ 54 * a1[0]
+ 45 * a1[10]
+ -17 * a1[33]
+ -49 * a1[4]
+ -34 * a1[17]
+ 87 * a1[7]
+ -41 * a1[18]
+ 2 * a1[30]
+ -81 * a1[11]
+ 37 * a1[35]
- 46 * a1[9]
+ 25 * a1[32]
- 45 * a1[14]
- 30 * a1[12]
+ 83 * a1[19]
+ 24 * a1[1]
+ 77 * a1[20])
s.add(98 * a1[16]
+ (a1[21]*64)
+ 93 * a1[8]
+ 78 * a1[2]
+ 56 * a1[15]
+ -51 * a1[6]
+ -17 * a1[26]
+ v19
- 62 * a1[5]
+ 67 * a1[22] == 33735)
s.add(v20 == -71 * a1[30]
+ 61 * a1[10]
+ -25 * a1[4]
+ 82 * a1[32]
+ 62 * a1[22]
+ -40 * a1[34]
+ 90 * a1[3]
+ -36 * a1[14]
+ 37 * a1[17]
+ -21 * a1[19]
+ 55 * a1[21]
+ -70 * a1[26]
+ 92 * a1[6]
+ 75 * a1[31]
+ -35 * a1[29]
+ -50 * a1[25]
+ 8 * a1[33]
+ -74 * a1[13]
+ 34 * a1[35]
+ 29 * a1[24]
+ -10 * a1[15]
+ -75 * a1[16]
+ 24 * a1[18]
+ 98 * a1[0]
+ 41 * a1[20]
- 54 * a1[28]
- 5 * a1[23]
- 66 * a1[9]
+ 3 * a1[5]
- 66 * a1[2]
+ 15 * a1[12]
- 74 * a1[27])
s.add(30 * a1[1] + -29 * a1[7] + v20 + 31 * a1[8] - 68 * a1[11] == -7107)
s.add(v21 == -83 * a1[29]
+ 55 * a1[35]
+ -75 * a1[8]
+ 77 * a1[31]
+ 84 * a1[22]
+ -34 * a1[13]
+ -13 * a1[15]
+ -11 * a1[19]
+ 28 * a1[17]
+ 98 * a1[9]
+ -69 * a1[3]
+ (a1[25] *64)
+ -66 * a1[7]
+ -71 * a1[6]
+ 75 * a1[34]
+ 19 * a1[32]
+ -94 * a1[33]
- 72 * a1[18]
+ 35 * a1[26]
- 32 * a1[27]
+ 76 * a1[1]
+ 80 * a1[28]
+ 66 * a1[10]
+ 3 * a1[12]
- 99 * a1[14]
+ 17 * a1[30]
- 94 * a1[0]
+ 12 * a1[2]
+ 61 * a1[20]
- 24 * a1[23]
+ 62 * a1[11]
+ 37 * a1[16])
s.add(-79 * a1[24] + v21 - 65 * a1[21] - 2 * a1[4] - 90 * a1[5] == -17028)
s.add(v22 == (a1[15] *64)
+ 43 * a1[11]
+ 39 * a1[23]
+ 68 * a1[33]
+ -58 * a1[13]
+ 21 * a1[1]
+ 19 * a1[19]
+ 96 * a1[8]
+ 24 * a1[3]
+ -76 * a1[2]
+ -94 * a1[16]
+ -37 * a1[4]
+ -31 * a1[7]
+ -65 * a1[0]
+ -23 * a1[22]
+ 80 * a1[24]
+ -48 * a1[20]
+ -42 * a1[32]
+ 47 * a1[9]
- 95 * a1[6]
- 10 * a1[35]
- 30 * a1[34]
- 67 * a1[12]
+ 81 * a1[14]
- 21 * a1[27]
+ 65 * a1[18]
+ 60 * a1[25]
+ 31 * a1[17]
- 20 * a1[31]
- 32 * a1[30]
- 83 * a1[28]
+ 20 * a1[5])
s.add( -17 * a1[21] + -34 * a1[26] + v22 - 3 * a1[29] + 7 * a1[10] == -21641)
s.add(v23 == -52 * a1[7]
+ -82 * a1[23]
+ 14 * a1[27]
+ 52 * a1[6]
+ 67 * a1[11]
+ a1[3]
+ -37 * a1[30]
+ -76 * a1[0]
+ -82 * a1[22]
+ -92 * a1[24]
+ 53 * a1[20]
+ -90 * a1[5]
+ 3 * a1[34]
+ 93 * a1[2]
+ 77 * a1[25]
+ -40 * a1[16]
+ -59 * a1[26]
+ -91 * a1[15]
+ 55 * a1[9]
+ -84 * a1[35]
+ -46 * a1[12]
+ -41 * a1[31]
+ -55 * a1[8]
+ 97 * a1[32]
+ 56 * a1[19]
- 15 * a1[13]
- 93 * a1[4]
+ 37 * a1[33]
- 88 * a1[18]
- 16 * a1[10]
+ a1[14]
+ 48 * a1[17]
- 80 * a1[21])
s.add(v23 + 17 * a1[29] - 94 * a1[28] - 12 * a1[1] == -71317)
s.add( v24 == 34 * a1[32]
+ -12 * a1[29]
+ -16 * a1[7]
+ 22 * a1[18]
+ -52 * a1[31]
+ -71 * a1[21]
+ -55 * a1[5]
+ -76 * a1[4]
+ -94 * a1[10]
+ -79 * a1[26]
+ 95 * a1[28]
+ 58 * a1[3]
+ -85 * a1[13]
+ -74 * a1[27]
+ -35 * a1[16]
+ 68 * a1[2]
+ 84 * a1[11]
+ -25 * a1[23]
+ -91 * a1[33]
+ -87 * a1[14]
+ -65 * a1[34]
+ 23 * a1[20]
+ -91 * a1[15]
+ 34 * a1[12]
+ 53 * a1[1]
- 16 * a1[24]
+ 83 * a1[22]
+ 5 * a1[17]
- 71 * a1[6])
s.add(46 * a1[9] + -26 * a1[0]+ 42 * a1[30] + 22 * a1[25] + -89 * a1[19] + v24 + 41 * a1[35] + 68 * a1[8] == -41387)
s.add(v25 == -53 * a1[8]
+ -18 * a1[1]
+ 9 * a1[32]
+ -45 * a1[9]
+ -97 * a1[12]
+ -19 * a1[19]
+ -87 * a1[3]
+ 89 * a1[27]
+ 54 * a1[5]
+ 59 * a1[22]
+ 95 * a1[17]
+ 62 * a1[26]
+ 6 * a1[20]
+ (a1[14] *64)
+ -50 * a1[13]
+ -95 * a1[30]
+ -68 * a1[16]
+ 10 * a1[0]
- a1[2]
- a1[28]
+ 17 * a1[18]
- 76 * a1[6]
- 24 * a1[23]
- 76 * a1[11]
+ 33 * a1[34]
- 98 * a1[31]
- 60 * a1[29]
- 74 * a1[35]
+ 31 * a1[7]
+ 50 * a1[24]
+ 25 * a1[21]
- 83 * a1[33])
s.add(-59 * a1[10] + 35 * a1[4] + v25 + 25 * a1[25] + 52 * a1[15] == -30463)
s.add(v26 == -42 * a1[35]
+ 30 * a1[28]
+ -54 * a1[30]
+ -53 * a1[20]
+ 98 * a1[33]
+ 70 * a1[32]
+ 99 * a1[19]
+ -27 * a1[25]
+ 84 * a1[34]
+ -73 * a1[14]
+ -54 * a1[7]
+ -45 * a1[26]
+ -97 * a1[18]
+ 40 * a1[10]
+ 73 * a1[27]
+ -55 * a1[11]
+ 52 * a1[29]
+ -29 * a1[13]
+ 32 * a1[24]
+ -80 * a1[0]
+ -79 * a1[17]
+ -39 * a1[6]
+ 88 * a1[1]
+ 44 * a1[2]
- 50 * a1[3]
- 2 * a1[22]
- 44 * a1[31]
- 62 * a1[8]
- 51 * a1[4]
+ 12 * a1[16]
- 55 * a1[9])
s.add(-68 * a1[5] + 77 * a1[21] + -34 * a1[15] + v26 + 40 * a1[12] + 76 * a1[23] == -14435)
s.add(v27 == 74 * a1[30]
+ 16 * a1[16]
+ -83 * a1[33]
+ 16 * a1[2]
+ -17 * a1[17]
+ -28 * a1[8]
+ 9 * a1[7]
+ 86 * a1[20]
+ 70 * a1[13]
+ -76 * a1[19]
+ -31 * a1[28]
+ 77 * a1[14]
+ 48 * a1[15]
+ -78 * a1[31]
+ -82 * a1[26]
+ 69 * a1[3]
+ 70 * a1[5]
+ 95 * a1[6]
- 60 * a1[4]
+ 30 * a1[27]
+ 3 * a1[29]
- 29 * a1[32]
+ 5 * a1[24]
+ 55 * a1[0]
+ 36 * a1[23]
- 90 * a1[22]
+ 37 * a1[35]
+ 78 * a1[34]
- 62 * a1[10]
+ 46 * a1[9]
+ 63 * a1[21]
- 39 * a1[12])
s.add(20 * a1[11] + -64 * a1[1] + v27 - (a1[18] *64) - 27 * a1[25] == 23472)
s.add(v28 == -55 * a1[3]
+ 85 * a1[16]
+ -97 * a1[34]
+ -29 * a1[27]
+ -79 * a1[32]
+ 50 * a1[28]
+ 7 * a1[0]
+ 92 * a1[6]
+ -57 * a1[24]
+ -89 * a1[11]
+ -47 * a1[5]
+ -39 * a1[30]
+ (a1[8] *64)
+ -63 * a1[12]
+ -46 * a1[9]
+ -82 * a1[17]
+ 39 * a1[23]
+ 58 * a1[13]
- 81 * a1[1]
+ 33 * a1[29]
+ 89 * a1[7]
- 14 * a1[20]
+ 97 * a1[33]
+ 10 * a1[35]
- 46 * a1[14]
+ 81 * a1[4]
+ 89 * a1[15]
+ 81 * a1[22]
- 44 * a1[31]
- 60 * a1[10]
- 20 * a1[26]
+ 18 * a1[18])
s.add( 97 * a1[21] + -71 * a1[2] + -7 * a1[19] + v28 + 91 * a1[25] == 7913)
s.add( v29 == -22 * a1[15]
+ -79 * a1[12]
+ -18 * a1[2]
+ 23 * a1[20]
+ -20 * a1[14]
+ (a1[19] *64)
+ 91 * a1[5]
+ 49 * a1[17]
+ 52 * a1[18]
+ -89 * a1[25]
+ -93 * a1[35]
+ -70 * a1[11]
+ -45 * a1[24]
+ 88 * a1[30]
+ 92 * a1[31]
+ 44 * a1[26]
+ -5 * a1[1]
+ -48 * a1[6]
+ -16 * a1[22]
+ 88 * a1[32]
+ 91 * a1[33]
+ 82 * a1[28]
+ 98 * a1[8]
- 63 * a1[13]
- 8 * a1[9]
- a1[16]
- 4 * a1[27]
- 47 * a1[4]
- 6 * a1[7]
+ 84 * a1[3]
- 6 * a1[34]
+ 69 * a1[21])
s.add(-41 * a1[10] + 67 * a1[29] + v29 - 4 * a1[23] - 80 * a1[0] == 23824 )
s.add( v30 == -28 * a1[35]
+ -72 * a1[6]
+ -46 * a1[32]
+ 99 * a1[20]
+ -69 * a1[22]
+ -94 * a1[12]
+ -35 * a1[8]
+ -29 * a1[0]
+ 89 * a1[11]
+ 61 * a1[7]
+ -92 * a1[31]
+ 99 * a1[21]
+ 27 * a1[16]
+ -48 * a1[24]
+ -51 * a1[4]
+ -39 * a1[25]
+ 84 * a1[30]
+ 34 * a1[14]
+ -73 * a1[17]
+ -92 * a1[18]
+ 72 * a1[2]
- 14 * a1[13]
- a1[19]
+ 2 * a1[9]
+ 3 * a1[29]
- 61 * a1[33]
- 6 * a1[26]
- 57 * a1[15]
- 8 * a1[27]
- 29 * a1[10]
- 2 * a1[23]
- 23 * a1[34])
s.add(v30 + 41 * a1[3] + 42 * a1[28] == -13865)
s.add(v31 == 74 * a1[12]
+ 22 * a1[29]
+ -29 * a1[20]
+ -49 * a1[22]
+ 88 * a1[14]
+ -51 * a1[24]
+ 44 * a1[21]
+ 28 * a1[13]
+ 62 * a1[25]
+ 85 * a1[8]
+ -66 * a1[32]
+ 43 * a1[10]
+ 32 * a1[33]
+ 75 * a1[34]
+ 44 * a1[1]
+ 49 * a1[28]
+ -21 * a1[26]
+ 60 * a1[4]
+ -40 * a1[0]
+ -98 * a1[15]
+ -37 * a1[9]
+ 78 * a1[16]
+ 96 * a1[35]
- 84 * a1[18]
- 2 * a1[7]
+ 43 * a1[2]
- 28 * a1[6]
- 77 * a1[3]
- 30 * a1[17]
- 95 * a1[5]
+ 5 * a1[23]
+ 85 * a1[31])
s.add(90 * a1[19] + 58 * a1[30] + v31 + 5 * a1[27] + 47 * a1[11] == 50179)
s.add(v32 == -92 * a1[26]
+ 4 * a1[29]
+ -89 * a1[20]
+ 57 * a1[15]
+ -66 * a1[0]
+ -85 * a1[12]
+ 91 * a1[35]
+ -68 * a1[2]
+ -100 * a1[25]
+ -88 * a1[18]
+ 46 * a1[33]
+ 50 * a1[31]
+ -85 * a1[4]
+ -92 * a1[6]
+ -54 * a1[7]
+ 83 * a1[23]
+ -25 * a1[24]
+ -91 * a1[5]
+ 85 * a1[10]
+ -15 * a1[16]
- 59 * a1[27]
- 91 * a1[8]
+ 73 * a1[32]
+ 44 * a1[19]
+ 5 * a1[34]
+ 68 * a1[14]
- 32 * a1[21]
- 26 * a1[30]
- 56 * a1[17]
- 95 * a1[3]
- 16 * a1[13]
- 76 * a1[11])
s.add( 30 * a1[1] + v32 - 48 * a1[9] - 88 * a1[22] + 65 * a1[28] == -75429)
s.add(v33 == 4 * a1[17]
+ -49 * a1[20]
+ -71 * a1[13]
+ -23 * a1[23]
+ -19 * a1[21]
+ 62 * a1[2]
+ -41 * a1[19]
+ 46 * a1[15]
+ 5 * a1[1]
+ -2 * a1[5]
+ 88 * a1[9]
+ 84 * a1[16]
+ 77 * a1[6]
- 6 * a1[26]
+ 51 * a1[33]
- 96 * a1[31]
+ 59 * a1[14]
- 62 * a1[8]
- 55 * a1[25]
- 32 * a1[34]
+ 69 * a1[32]
- 48 * a1[28]
- 21 * a1[27]
+ 31 * a1[0]
- 98 * a1[10])
s.add(85 * a1[30]
+ -35 * a1[24]
+ -58 * a1[18]
+ 16 * a1[12]
+ -45 * a1[7]
+ 49 * a1[35]
+ 8 * a1[11]
+ 54 * a1[22]
+ -33 * a1[4]
+ v33
- 96 * a1[29]
- 71 * a1[3] == -18764)
s.add(v34 == -78 * a1[32]
+ -88 * a1[11]
+ -21 * a1[35]
+ 25 * a1[18]
+ -81 * a1[19]
+ 74 * a1[20]
+ -50 * a1[2]
+ -46 * a1[21]
+ 28 * a1[15]
+ -100 * a1[5]
+ 53 * a1[28]
+ -93 * a1[9]
+ -69 * a1[1]
+ -61 * a1[0]
+ 26 * a1[8]
+ -66 * a1[6]
+ -66 * a1[27]
- 42 * a1[4]
+ 89 * a1[33]
- 30 * a1[31]
- 45 * a1[22]
+ 13 * a1[14]
- 29 * a1[3]
+ 33 * a1[10]
+ 54 * a1[23]
+ 18 * a1[30]
- 39 * a1[29]
+ 15 * a1[13]
+ 83 * a1[26])
s.add( 88 * a1[12] + 84 * a1[34] + 66 * a1[24] + 99 * a1[16] + v34 - 28 * a1[7] + 2 * a1[25] == -20428)
s.add(v35 == 10 * a1[31]
+ (a1[28] *64)
+ 97 * a1[5]
+ -7 * a1[27]
+ 62 * a1[14]
+ 60 * a1[24]
+ 27 * a1[34]
+ -11 * a1[10]
+ -97 * a1[22]
+ 14 * a1[33]
+ -43 * a1[11]
+ 40 * a1[20]
+ 31 * a1[13]
+ 44 * a1[29]
+ -68 * a1[3]
+ -36 * a1[1]
+ -38 * a1[9]
+ -7 * a1[12]
+ a1[26]
+ -50 * a1[6]
+ 59 * a1[8]
+ 88 * a1[30]
+ 46 * a1[0]
- 34 * a1[15]
+ 10 * a1[4]
+ 84 * a1[18]
+ 13 * a1[7]
+ 14 * a1[25]
- 5 * a1[16]
- 31 * a1[32]
- 48 * a1[19]
- 55 * a1[35])
s.add(v35 - 96 * a1[2] - 83 * a1[23] == 11973)
s.add(v36 == 6 * a1[22]
+ 58 * a1[34]
+ 4 * a1[31]
+ 55 * a1[21]
+ -99 * a1[4]
+ -57 * a1[8]
+ 2 * a1[7]
+ 57 * a1[24]
+ -54 * a1[25]
+ 39 * a1[29]
+ -91 * a1[1]
+ -32 * a1[20]
+ -30 * a1[11]
+ 16 * a1[12]
+ 45 * a1[17]
+ 90 * a1[32]
+ 26 * a1[5]
- 59 * a1[28]
+ 7 * a1[2]
- 88 * a1[3]
+ 36 * a1[15]
- 73 * a1[6]
- 6 * a1[27]
+ 99 * a1[13]
- 96 * a1[0]
- 72 * a1[16]
+ 27 * a1[19]
+ 79 * a1[23]
- 28 * a1[18]
- 90 * a1[30])
s.add( -45 * a1[26] + -10 * a1[35] + -40 * a1[9] + 97 * a1[10] + v36 - 6 * a1[33] + 58 * a1[14] == -23186)
s.check()
print(s.model())解出来整理一下是hgame{@_FAKE_flag!-do_Y0u_know_SMC?}
根据提示去找一些函数，看看是否有smc，发现在这个函数里面。
然后写idapython脚本，还原，话说攻防世界也有一道smc的题，好像叫BABYRE，当时还不懂。
import sys
from idautils import *
from idc import *
import idaapi
if __name__ =="__main__":
start_addr=0x401216
end_addr=0x409080
for i in range(0x43e):
PatchByte(start_addr+i,Byte(start_addr+i)^Byte(end_addr+i))然后PatchByte好像只能在IDA7.0才能用，所以可以先在IDA7.0用了然后保存文件，就可以看到真正的代码了。
和这个文章差不多https://blog.csdn.net/s1054436218/article/details/78651075和矩阵有点关系。
大致过程就是，将输入的flag，和假的flag分成6*6的矩阵
然后flag的第一行分别和假flag的每一列的对应数字相乘，每相乘一列就得到一个数，第一行会得到6个数
然后flag的第二行分别和假flag的每一列的对应数字相乘，每相乘一列就得到一个数，第二行会得到6个数
然后flag的第三行分别和假flag的每一列的对应数字相乘，每相乘一列就得到一个数，第三行会得到6个数
然后flag的第四行分别和假flag的每一列的对应数字相乘，每相乘一列就得到一个数，第四行会得到6个数
然后flag的第五行分别和假flag的每一列的对应数字相乘，每相乘一列就得到一个数，第五行会得到6个数
然后flag的第六行分别和假flag的每一列的对应数字相乘，每相乘一列就得到一个数，第六行会得到6个数最后就得到了v39的36个数。
然后用z3约束写脚本
from z3 import *
s = Solver()
v38=[55030,61095,60151,57247,56780,55726,
46642,52931,53580,50437,50062,44186,
44909,46490,46024,44347,43850,44368,
54990,61884,61202,58139,57730,54964,
48849,51026,49629,48219,47904,50823,
46596,50517,48421,46143,46102,46744]
v37=[104,103,97,109,101,123,
64,95,70,65,75,69,
95,102,108,97,103,33,
45,100,111,95,89,48,
117,95,107,111,110,119,
95,83,77,67,63,125]
print(len(v37))
print(len(v38))
s = Solver()
flag=[0]*36
v39=[0 for i in range(36)]
for i in range(36):
flag[i] = Int('flag['+str(i)+']')
for i in range(6):
s.add(flag[i] == ord('hgame{'[i]))
s.add(flag[-1] == ord('}'))
for i in range(6,36):
s.add(flag[i]>=32)
s.add(flag[i]<=127)
for i in range(6):#行
for j in range(6):#列
for k in range(6):
v39[6 * i + j] = v39[6 * i + j] + v37[6 * k + j] * flag[6 * i + k]
s.add(simplify(v39[j + 6 * i] == v38[j + 6 * i]))
print(s.check())
m=s.model()
print(m)得到hgame{E@sy_Se1f-Modifying_C0oodee33}
