BUUCTF Reverse equation
下载下来一般明显就是jsFuck的加密，仔细看一下这个js，看的出来就是一系列的公式的排列。l[jsfuck]+l[jsfuck]....l[jsfuck] = int && l[jsfuck]+l[jsfuck]....l[jsfuck] = int$
这里我看大神写正则直接匹配，我觉得还是比较困难的。我使用的是Google Closure Compiler直接对js进行了压缩。
flag="xxx";
42==flag.length&&(l=flag.split("").map(function(a){return a.charCodeAt()}),861==l["40"]+l["35"]+l["34"]-l[0]-l["15"]-l["37"]+l[7]+l[6]-l["26"]+l["20"]+l["19"]+l[8]-l["17"]-l["14"]-l["38"]+l[1]-l[9]+l["22"]+l["41"]+l[3]-l["29"]-l["36"]-l["25"]+l[5]+l["32"]-l["16"]+l["12"]-l["24"]+l["30"]+l["39"]+l["10"]+l[2]+l["27"]+l["28"]+l["21"]+l["33"]-l["18"]+l[4]&&-448==l["31"]+l["26"]+l["11"]-l["33"]+l["27"]-l[3]+l["12"]+l["30"]+l[1]+l["32"]-l["16"]+l[7]+l["10"]-l["25"]+l["38"]-l["41"]-l["14"]-l["19"]+l["29"]+
l["36"]-l[9]-l["28"]-l[6]-l[0]-l["22"]-l["18"]+l["20"]-l["37"]+l[4]-l["24"]+l["34"]-l["21"]-l["39"]-l["23"]-l[8]-l["40"]+l["15"]-l["35"]&&1244==l["26"]+l["14"]+l["15"]+l[9]+l["13"]+l["30"]-l["11"]+l["18"]+l["23"]+l[7]+l[3]+l["12"]+l["25"]-l["24"]-l["39"]-l["35"]-l["20"]+l["40"]-l[8]+l["10"]-l[5]-l["33"]-l["31"]+l["32"]+l["19"]+l["21"]-l[6]+l[1]+l["16"]+l["17"]+l["29"]+l["22"]-l[4]-l["36"]+l["41"]+l["38"]+l[2]+l[0]&&-39==l[5]+l["22"]+l["15"]+l[2]-l["28"]-l["10"]-l[3]-l["13"]-l["18"]+l["30"]-l[9]+l["32"]+
l["19"]+l["34"]+l["23"]-l["17"]+l["16"]-l[7]+l["24"]-l["39"]+l[8]-l["12"]-l["40"]-l["25"]+l["37"]-l["35"]+l["11"]-l["14"]+l["20"]-l["27"]+l[4]-l["33"]-l["21"]+l["31"]-l[6]+l[1]+l["38"]-l["29"]&&485==l["41"]-l["29"]+l["23"]-l[4]+l["20"]-l["33"]+l["35"]+l[3]-l["19"]-l["21"]+l["11"]+l["26"]-l["24"]-l["17"]+l["37"]+l[1]+l["16"]-l[0]-l["13"]+l[7]+l["10"]+l["14"]+l["22"]+l["39"]-l["40"]+l["34"]-l["38"]+l["32"]+l["25"]
略
我们将这里整理一下可以得到所有的公式
861 == l[40] + l[35] + l[34] - l[0] - l[15] - l[37] + l[7] + l[6] - l[26] + l[20] + l[19] + l[8] - l[17] - l[14] - l[38] + l[1] - l[9] + l[22] + l[41] + l[3] - l[29] - l[36] - l[25] + l[5] + l[32] - l[16] + l[12] - l[24] + l[30] + l[39] + l[10] + l[2] + l[27] + l[28] + l[21] + l[33] - l[18] + l[4]
-448 == l[31] + l[26] + l[11] - l[33] + l[27] - l[3] + l[12] + l[30] + l[1] + l[32] - l[16] + l[7] + l[10] - l[25] + l[38] - l[41] - l[14] - l[19] + l[29] +l[36] - l[9] - l[28] - l[6] - l[0] - l[22] - l[18] + l[20] - l[37] + l[4] - l[24] + l[34] - l[21] - l[39] - l[23] - l[8] - l[40] + l[15] - l[35]
1244 == l[26] + l[14] + l[15] + l[9] + l[13] + l[30] - l[11] + l[18] + l[23] + l[7] + l[3] + l[12] + l[25] - l[24] - l[39] - l[35] - l[20] + l[40] - l[8] + l[10] - l[5] - l[33] - l[31] + l[32] + l[19] + l[21] - l[6] + l[1] + l[16] + l[17] + l[29] + l[22] - l[4] - l[36] + l[41] + l[38] + l[2] + l[0
-39 == l[5] + l[22] + l[15] + l[2] - l[28] - l[10] - l[3] - l[13] - l[18] + l[30] - l[9] + l[32] +l[19] + l[34] + l[23] - l[17] + l[16] - l[7] + l[24] - l[39] + l[8] - l[12] - l[40] - l[25] + l[37] - l[35] + l[11] - l[14] + l[20] - l[27] + l[4] - l[33] - l[21] + l[31] - l[6] + l[1] + l[38] - l[29]
485 == l[41] - l[29] + l[23] - l[4] + l[20] - l[33] + l[35] + l[3] - l[19] - l[21] + l[11] + l[26] - l[24] - l[17] + l[37] + l[1] + l[16] - l[0] - l[13] + l[7] + l[10] + l[14] + l[22] + l[39] - l[40] + l[34] - l[38] + l[32] + l[25] - l[2] + l[15] + l[6] + l[28] - l[8] - l[5] - l[31] - l[30] - l[27]
略
到这里很显然我们需要的就是解方程。解出来的结果就是flag。这里我们使用一个很好的python库：Z3。
z3安装的时候最好还是使用pip安装，命令：python pip install z3-solver 因为我是python2和3都安装了，所以命令是python3 -m pip install z3-solver。
我一开始通过pychram安装的时候，发现Solver()函数不能使用。
from z3 import *
if __name__ == "__main__":
s = Solver()
l = [Int('l[%d]' % i) for i in range(42)] #定义l[0] - l[41]都是int类型
#以下都是公式
s.add(861 == l[40] + l[35] + l[34] - l[0] - l[15] - l[37] + l[7] + l[6] - l[26] + l[20] + l[19] + l[8] - l[17] - l[
14] - l[38] + l[1] - l[9] + l[22] + l[41] + l[3] - l[29] - l[36] - l[25] + l[5] + l[32] - l[16] + l[12] - l[
24] + l[30] + l[39] + l[10] + l[2] + l[27] + l[28] + l[21] + l[33] - l[18] + l[4])
s.add(
-448 == l[31] + l[26] + l[11] - l[33] + l[27] - l[3] + l[12] + l[30] + l[1] + l[32] - l[16] + l[7] + l[10] - l[
25] + l[38] - l[41] - l[14] - l[19] + l[29] + l[36] - l[9] - l[28] - l[6] - l[0] - l[22] - l[18] + l[20] -
l[37] + l[4] - l[24] + l[34] - l[21] - l[39] - l[23] - l[8] - l[40] + l[15] - l[35])
s.add(
1244 == l[26] + l[14] + l[15] + l[9] + l[13] + l[30] - l[11] + l[18] + l[23] + l[7] + l[3] + l[12] + l[25] - l[
24] - l[39] - l[35] - l[20] + l[40] - l[8] + l[10] - l[5] - l[33] - l[31] + l[32] + l[19] + l[21] - l[6] +
l[1] + l[16] + l[17] + l[29] + l[22] - l[4] - l[36] + l[41] + l[38] + l[2] + l[0])
s.add(-39 == l[5] + l[22] + l[15] + l[2] - l[28] - l[10] - l[3] - l[13] - l[18] + l[30] - l[9] + l[32] + l[19] + l[
34] + l[23] - l[17] + l[16] - l[7] + l[24] - l[39] + l[8] - l[12] - l[40] - l[25] + l[37] - l[35] + l[11] - l[
14] + l[20] - l[27] + l[4] - l[33] - l[21] + l[31] - l[6] + l[1] + l[38] - l[29])
s.add(
485 == l[41] - l[29] + l[23] - l[4] + l[20] - l[33] + l[35] + l[3] - l[19] - l[21] + l[11] + l[26] - l[24] - l[
17] + l[37] + l[1] + l[16] - l[0] - l[13] + l[7] + l[10] + l[14] + l[22] + l[39] - l[40] + l[34] - l[38] +
l[32] + l[25] - l[2] + l[15] + l[6] + l[28] - l[8] - l[5] - l[31] - l[30] - l[27])
s.add(
-1068 == l[13] + l[19] + l[21] -
l[2] - l[33] - l[0] + l[39] + l[31] - l[23] - l[41] + l[38] - l[29] + l[36] + l[24] - l[20] - l[9] - l[32] + l[
37] - l[35] + l[40] + l[7] - l[26] + l[15] - l[10] - l[6] - l[16] - l[4] - l[5] - l[30] - l[14] - l[22] - l[
25] - l[34] - l[17] - l[11] - l[27] + l[1] - l[28])
s.add(939 == l[32] + l[0] + l[9] + l[14] + l[11] + l[18] - l[13] + l[24] - l[2] - l[15] + l[19] - l[21] + l[1] + l[
39] - l[8] - l[3] + l[33] + l[6] - l[5] - l[35] - l[28] + l[25] - l[41] + l[22] - l[17] + l[10] + l[40] + l[
34] + l[27] - l[20] + l[23] + l[31] - l[16] +
l[7] + l[12] - l[30] + l[29] - l[4])
s.add(
413 == l[19] + l[11] + l[20] - l[16] + l[40] + l[25] + l[1] - l[31] + l[28] - l[23] + l[14] - l[9] - l[27] + l[
35] + l[39] - l[37] - l[8] - l[22] + l[5] - l[6] + l[0] - l[32] + l[24] + l[33] + l[29] + l[38] + l[15] - l[
2] + l[30] + l[7] + l[12] - l[3] - l[17] + l[34] + l[41] - l[4] - l[13] - l[26])
s.add(117 == l[22] + l[4] - l[9] + l[34] + l[35] + l[17] + l[3] - l[24] + l[38] - l[5] - l[41] - l[31] - l[0] - l[
25] + l[33] + l[15] - l[1] - l[10] + l[16] - l[29] - l[12] + l[26] - l[39] - l[21] - l[18] - l[6] - l[40] - l[
13] + l[8] + l[37] + l[19] + l[14] + l[32] + l[28] - l[11] + l[23] + l[36] + l[7])
s.add(
-313 == l[32] + l[16] + l[3] + l[11] + l[34] - l[31] + l[14] + l[25] + l[1] - l[30] - l[33] - l[40] - l[4] - l[
29] + l[18] - l[27] + l[13] - l[19] - l[12] + l[23] - l[39] - l[41] - l[8] + l[22] - l[5] - l[38] - l[9] -
l[37] + l[17] - l[36] + l[24] - l[21] + l[2] - l[26] + l[20] - l[7] + l[35] - l[0])
s.add(
-42 == l[40] - l[1] + l[5] + l[7] + l[33] + l[29] + l[12] + l[38] - l[31] + l[2] + l[14] - l[35] - l[8] - l[
24] - l[39] - l[9] - l[28] + l[23] - l[17] - l[22] - l[26] + l[32] - l[11] + l[4] - l[36] + l[10] + l[20] -
l[18] - l[16] + l[6] - l[0] + l[3] - l[30] + l[37] - l[19] + l[21] + l[25] - l[15])
s.add(
289 == l[21] + l[26] - l[17] - l[25] + l[27] - l[22] - l[39] - l[23] - l[15] - l[20] - l[32] + l[12] + l[3] - l[
6] + l[28] + l[31] + l[13] - l[16] - l[37] - l[30] - l[5] + l[41] + l[29] + l[36] + l[1] + l[11] + l[24] +
l[18] - l[40] + l[19] - l[35] + l[2] - l[38] + l[14] - l[9] + l[4] + l[0] - l[33])
s.add(-117 == l[29] + l[31] + l[32] - l[17] - l[7] + l[34] + l[2] + l[14] + l[23] - l[4] + l[3] + l[35] - l[33] - l[
9] - l[20] - l[37] + l[24] - l[27] + l[36] + l[15] - l[18] - l[0] + l[12] + l[11] - l[38] + l[6] + l[22] + l[
39] - l[25] - l[10] - l[19] - l[1] + l[13] - l[41] + l[30] - l[16] + l[28] - l[26])
s.add(-252 == l[5] + l[37] - l[39] + l[0] - l[27] + l[12] + l[41] - l[22] + l[8] - l[16] - l[38] + l[9] + l[15] - l[
35] - l[29] + l[18] + l[6] - l[25] - l[28] + l[36] + l[34] + l[32] - l[14] - l[1] + l[20] + l[40] - l[19] - l[
4] - l[7] + l[26] + l[30] - l[10] + l[13] - l[21] + l[2] - l[23] - l[3] - l[33])
s.add(
-183 == l[29] + l[10] - l[41] - l[9] + l[12] - l[28] + l[11] + l[40] - l[27] - l[8] + l[32] - l[25] - l[23] + l[
39] - l[1] - l[36] - l[15] + l[33] - l[20] + l[18] + l[22] - l[3] + l[6] - l[34] - l[21] + l[19] + l[26] +
l[13] - l[4] + l[7] - l[37] + l[38] - l[2] - l[30] - l[0] - l[35] + l[5] + l[17])
s.add(188 == l[6] - l[8] - l[20] + l[34] - l[33] - l[25] - l[4] + l[3] + l[17] - l[13] - l[15] - l[40] + l[1] - l[
30] - l[14] - l[28] - l[35] + l[38] - l[22] + l[2] + l[24] - l[29] + l[5] + l[9] + l[37] + l[23] - l[18] + l[
19] - l[21] + l[11] + l[36] + l[41] - l[7] - l[32] + l[10] + l[26] - l[0] + l[31]
)
s.add(1036 == l[3] + l[6] - l[41] + l[10] + l[39] + l[37] + l[1] + l[8] + l[21] + l[24] + l[29] + l[12] + l[27] - l[
38] + l[11] + l[23] + l[28] + l[33] - l[31] + l[14] - l[5] + l[32] - l[17] + l[40] - l[34] + l[20] - l[22] - l[
16] + l[19] + l[2] - l[36] - l[7] + l[18] + l[15] + l[26] - l[0] - l[4] + l[35])
s.add(328 == l[28] - l[33] + l[2] + l[37] - l[12] - l[9] - l[39] + l[16] - l[32] + l[8] - l[36] + l[31] + l[10] - l[
4] + l[21] - l[25] + l[18] + l[24] - l[0] + l[29] - l[26] + l[35] - l[22] - l[41] - l[6] + l[15] + l[19] + l[
40] + l[7] + l[34] + l[17] - l[3] - l[13] + l[5] + l[23] + l[11] - l[27] + l[1])
s.add(
-196 == l[22] - l[32] + l[17] - l[9] + l[20] - l[18] - l[34] + l[23] + l[36] - l[35] - l[38] + l[27] + l[4] - l[
5] - l[41] + l[29] + l[33] + l[0] - l[37] + l[28] - l[40] - l[11] - l[12] + l[7] + l[1] + l[2] - l[26] - l[
16] - l[8] + l[24] - l[25] + l[3] - l[6] - l[19] - l[39] - l[14] - l[31] + l[10])
s.add(
7 == l[11] + l[13] + l[14] - l[15] - l[29] - l[2] + l[7] + l[20] + l[30] - l[36] - l[33] - l[19] + l[31] + l[
0] - l[39] - l[4] - l[6] + l[38] + l[35] - l[28] + l[34] - l[9] - l[23] - l[26] + l[37] - l[8] - l[27] + l[
5] - l[41] + l[3] + l[17] + l[40] - l[10] + l[25] + l[12] - l[24] + l[18] + l[32])
s.add(
-945 == l[34] - l[37] - l[40] + l[4] - l[22] - l[31] - l[6] + l[38] + l[13] - l[28] + l[8] + l[30] - l[20] - l[
7] - l[32] + l[26] + l[1] - l[18] + l[5] + l[35] - l[24] - l[41] + l[9] - l[0] - l[2] - l[15] - l[10] + l[
12] - l[36] + l[33] - l[16] - l[14] - l[25] - l[29] - l[21] + l[27] + l[3] - l[17])
s.add(-480 == l[12] - l[30] - l[8] + l[20] - l[2] -
l[36] - l[25] - l[0] - l[19] - l[28] - l[7] - l[11] - l[33] + l[4] - l[23] + l[10] - l[41] + l[39] - l[32] +
l[27] + l[18] + l[15] + l[34] + l[13] - l[40] + l[29] - l[6] + l[37] - l[14] - l[16] + l[38] - l[26] + l[17] +
l[31] - l[22] - l[35] + l[5] - l[1])
s.add(
-213 == l[36] - l[11] - l[34] + l[8] + l[0] + l[15] + l[28] - l[39] - l[32] - l[2] - l[27] + l[22] + l[16] - l[
30] - l[3] + l[31] - l[26] + l[20] + l[17] - l[29] - l[18] + l[19] - l[10] + l[6] - l[5] - l[38] - l[25] -
l[24] + l[4] + l[23] + l[9] + l[14] + l[21] - l[37] + l[13] - l[41] - l[12] + l[35])
s.add(
-386 == l[19] - l[36] - l[12] + l[33] - l[27] - l[37] - l[25] + l[38] + l[16] - l[18] + l[22] - l[39] + l[13] -
l[7] - l[31] - l[26] + l[15] - l[10] - l[9] - l[2] - l[30] - l[11] + l[41] - l[4] + l[24] + l[34] + l[5] + l[
17] + l[14] + l[6] + l[8] - l[21] - l[23] + l[32] - l[1] - l[29] - l[0] + l[3])
s.add(l[0] + l[7] - l[28] - l[38] + l[19] + l[31] - l[5] + l[24] - l[3] + l[33] - l[12] - l[29] + l[32] + l[1] - l[
34] - l[9] - l[25] + l[26] - l[8] + l[4] - l[10] + l[40] - l[15] - l[11] - l[27] + l[36] + l[14] + l[41] - l[
35] - l[13] - l[17] - l[21] - l[18] + l[39] - l[2] + l[20] - l[23] - l[22] == -349)
s.add(
98 == l[10] + l[22] + l[21] - l[0] + l[15] - l[6] + l[20] - l[29] - l[30] - l[33] + l[19] + l[23] - l[28] + l[
41] - l[
27] - l[12] - l[37] - l[32] + l[34] - l[36] + l[3] + l[1] - l[13] + l[18] + l[14] + l[9] + l[7] - l[39] + l[
8] + l[2] - l[31] - l[5] - l[40] + l[38] - l[26] - l[4] + l[16] - l[25])
s.add(
-412 == l[28] + l[38] + l[20] + l[0] - l[5] - l[34] - l[41] + l[22] - l[26] + l[11] + l[29] + l[31] - l[3] - l[
16] + l[
23] + l[17] - l[18] + l[9] - l[4] - l[12] - l[19] - l[40] - l[27] + l[33] + l[8] - l[37] + l[2] + l[15] - l[
24] - l[39] + l[10] + l[35] - l[1] + l[30] - l[36] - l[25] - l[14] - l[32])
s.add(-95 == l[1] - l[24] - l[29] + l[39] + l[41] + l[0] + l[9] - l[19] + l[6] - l[37] - l[22] + l[32] + l[21] + l[
28] + l[
36] + l[4] - l[17] + l[20] - l[13] - l[35] - l[5] + l[33] - l[27] - l[30] + l[40] + l[25] - l[18] + l[
34] - l[
3] - l[10] - l[16] - l[23] - l[38] + l[8] - l[14] - l[11] - l[7] + l[12])
s.add(
-379 == l[2] - l[24] + l[31] + l[0] + l[9] - l[6] + l[7] - l[1] - l[22] + l[8] - l[23] + l[40] + l[20] - l[38] -
l[11] -
l[14] + l[18] - l[36] + l[15] - l[4] - l[41] - l[12] - l[34] + l[32] - l[35] + l[17] - l[21] - l[10] - l[29] +
l[39] - l[16] + l[27] + l[26] - l[3] - l[5] + l[13] + l[25] - l[28])
s.add(861 == l[19] - l[17] + l[31] + l[14] + l[6] - l[12] + l[16] - l[8] + l[27] - l[13] + l[41] + l[2] - l[7] + l[
32] + l[
1] + l[25] - l[9] + l[37] + l[34] - l[18] - l[40] - l[11] - l[10] + l[38] + l[21] + l[3] - l[0] + l[24] +
l[
15] + l[23] - l[20] + l[26] + l[22] - l[4] - l[28] - l[5] + l[39] + l[35])
s.add(
1169 == l[35] + l[36] - l[16] - l[26] - l[31] + l[0] + l[21] - l[13] + l[14] + l[39] + l[7] + l[4] + l[34] + l[
38] + l[
17] + l[22] + l[32] + l[5] + l[15] + l[8] - l[29] + l[40] + l[24] + l[6] + l[30] - l[2] + l[25] + l[23] + l[
1] + l[12] + l[9] - l[10] - l[3] - l[19] + l[20] - l[37] - l[33] - l[18] == 1169)
s.add(
-1236 == l[13] + l[0] - l[25] - l[32] - l[21] - l[34] - l[14] - l[9] - l[8] - l[15] - l[16] + l[38] - l[35] - l[
30] - l[
40] - l[12] + l[3] - l[19] + l[4] - l[41] + l[2] - l[36] + l[37] + l[17] - l[1] + l[26] - l[39] - l[10] - l[
33] + l[5] - l[27] - l[23] - l[24] - l[7] + l[31] - l[28] - l[18] + l[6])
s.add(
-114 == l[20] + l[27] - l[29] - l[25] - l[3] + l[28] - l[32] - l[11] + l[10] + l[31] + l[16] + l[21] - l[7] + l[
4] - l[24] - l[35] + l[26] + l[12] - l[37] + l[6] + l[23] + l[41] - l[39] - l[38] + l[40] - l[36] + l[8] -
l[9] - l[5] - l[1] - l[13] - l[14] + l[19] + l[0] - l[34] - l[15] + l[17] + l[22])
s.add(
659 == l[12] - l[28] - l[13] - l[23] - l[33] + l[18] + l[10] + l[11] + l[2] - l[36] + l[41] - l[16] + l[39] + l[
34] +
l[32] + l[37] - l[38] + l[20] + l[6] + l[7] + l[31] + l[5] + l[22] - l[4] - l[15] - l[24] + l[17] - l[3] + l[
1] - l[35] - l[9] + l[30] + l[25] - l[0] - l[8] - l[14] + l[26] + l[21])
s.add(-430 == l[21] - l[3] + l[7] - l[27] + l[0] - l[32] - l[24] - l[37] + l[4] - l[22] + l[20] - l[5] - l[30] - l[
31] - l[1] + l[15] + l[41] + l[12] + l[40] + l[38] - l[17] - l[39] + l[19] - l[13] + l[23] + l[18] - l[2] + l[
6] - l[33] - l[9] + l[28] + l[8] - l[16] - l[10] - l[14] + l[34] + l[35] - l[11])
s.add(
-513 == l[11] - l[23] - l[9] - l[19] + l[17] + l[38] - l[36] - l[22] - l[10] + l[27] - l[14] - l[4] + l[5] + l[
31] +
l[2] + l[0] - l[16] - l[8] - l[28] + l[3] + l[40] + l[25] - l[33] + l[13] - l[32] - l[35] + l[26] - l[20] - l[
41] - l[30] - l[12] - l[7] + l[37] - l[39] + l[15] + l[18] - l[29] - l[21])
s.add(
-502 == l[32] + l[19] + l[4] - l[13] - l[17] - l[30] + l[5] - l[33] - l[37] - l[15] - l[18] + l[7] + l[25] - l[
14] + l[35] + l[40] + l[16] + l[1] + l[2] + l[26] - l[3] - l[39] - l[22] + l[23] - l[36] - l[27] - l[9] + l[
6] - l[41] - l[0] - l[31] - l[20] + l[12] - l[8] + l[29] - l[11] - l[34] + l[21])
s.add(
853 == l[30] - l[31] - l[36] + l[3] + l[9] - l[40] -
l[33] + l[25] + l[39] - l[26] + l[23] - l[0] - l[29] - l[32] - l[4] + l[37] + l[28] + l[21] + l[17] + l[2] + l[
24] + l[6] + l[5] + l[8] + l[16] + l[27] + l[19] + l[12] + l[20] + l[41] - l[22] + l[15] - l[11] + l[34] -
l[18] - l[38] + l[1] - l[14])
s.add(
-28 == l[38] - l[10] + l[16] + l[8] + l[21] - l[25] + l[36] - l[30] + l[31] - l[3] + l[5] - l[15] + l[23] - l[
28] + l[7] + l[12] - l[29] + l[22] - l[0] - l[37] - l[14] - l[11] + l[32] + l[33] - l[9] + l[39] + l[41] -
l[19] - l[1] + l[18] - l[4] - l[6] + l[13] + l[20] - l[2] - l[35] - l[26] +
l[27])
s.add(
-529 == l[11] + l[18] - l[26] + l[15] - l[14] - l[33] + l[7] - l[23] - l[25] + l[0] - l[6] - l[21] - l[16] + l[
17] - l[19] - l[28] - l[38] - l[37] + l[9] + l[20] - l[8] - l[3] + l[22] - l[35] - l[10] - l[31] - l[2] + l[
41] - l[1] - l[4] + l[24] - l[34] + l[39] + l[40] + l[32] - l[5] + l[36] - l[27])
s.add(
-12 == l[38] + l[8] + l[36] + l[35] - l[23] - l[34] + l[13] - l[4] - l[27] - l[24] + l[26] + l[31] - l[30] - l[
5] - l[40] + l[28] - l[11] - l[2] - l[39] + l[15] + l[10] - l[17] + l[3] + l[19] + l[22] + l[33] + l[0] + l[
37] +
l[16] - l[9] - l[32] + l[25] - l[21] - l[12] + l[6] - l[41] + l[20] - l[18])
s.add(
81 == l[6] - l[30] - l[20] - l[27] - l[14] - l[39] + l[41] - l[33] - l[0] + l[25] - l[32] - l[3] + l[26] - l[
12] + l[8] - l[35] - l[24] + l[15] + l[9] - l[4] + l[13] + l[36] + l[34] + l[1] - l[28] - l[21] + l[18] + l[
23] + l[29] - l[10] - l[38] + l[22] + l[37] + l[5] + l[19] + l[7] + l[16] - l[31])
s.check()
for key in l:
print(chr(int("%s" % (s.model()[key]))), end='')
flag：flag{A_l0ng_10NG_eqU4Ti0n_1s_E4Sy_W1Th_z3}