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}