Linear Equation 1

import z3

def compute(inp:list):
    result = [0] * 32
    result[0] = (inp[20] ^ 0x40) * 0xec + (inp[21] ^ 0x40) * -0x84 + (inp[14] ^ 0x40) * -0x79 + (inp[22] ^ 0x40) * -0x1a + (inp[21] ^ 0x40) * -0x40
    result[1] = (inp[5] ^ 0x6b) * 0xc + (inp[6] ^ 0x6b) * 0x59 + (inp[8] ^ 0x6b) * 0xdc + (inp[17] ^ 0x6b) * -0x4a + (inp[15] ^ 0x6b) * 0xa2
    result[2] = (inp[9] ^ 0xf7) * -0x60 + (inp[30] ^ 0xf7) * -0xc1 + (inp[5] ^ 0xf7) * -0xea + (inp[14] ^ 0xf7) * 199 + (inp[27] ^ 0xf7) * 0xbf
    result[3] = (inp[12] ^ 0x6e) * 0x25 + (inp[11] ^ 0x6e) * -0x80 + (inp[5] ^ 0x6e) * 0x88 + (inp[7] ^ 0x6e) * 0x6a
    result[4] = (inp[4] ^ 0x24) * -0x7b + (inp[28] ^ 0x24) * 0xd7 + (inp[12] ^ 0x24) * -0xfa + (inp[11] ^ 0x24) * 0xf7 + (inp[13] ^ 0x24) * -4
    result[5] = (inp[16] ^ 0x54) * 0x20 + (inp[24] ^ 0x54) * -0x86 + (inp[11] ^ 0x54) * -0x94 + (inp[8] ^ 0x54) * -0x24 + (inp[26] ^ 0x54) * 0x85
    result[6] = (inp[22] ^ 1) * 0x139 + (inp[17] ^ 1) * -0xd4 + (inp[7] ^ 1) * -5 + (inp[13] ^ 1) * -0xa4
    result[7] = (inp[15] ^ 0xa7) * -0xd8 + (inp[19] ^ 0xa7) * 0xd2 + (inp[4] ^ 0xa7) * 0x81 + (inp[27] ^ 0xa7) * -0xde
    result[8] = (inp[11] ^ 0x27) * 0xb9 + (inp[26] ^ 0x27) * -0xb6 + (inp[21] ^ 0x27) * -0x36 + (inp[21] ^ 0x27) * 0x4f + (inp[10] ^ 0x27) * 0x8e
    result[9] = (inp[22] ^ 0x8d) * 0xc6 + (inp[21] ^ 0x8d) * -0x15 + (inp[11] ^ 0x8d) * 0x26 + (inp[11] ^ 0x8d) * 0x71 + (inp[24] ^ 0x8d) * -0xb6
    result[10] = (inp[18] ^ 200) * -0x3a + (inp[13] ^ 200) * -0x5b + (inp[27] ^ 200) * -0xca + (inp[20] ^ 200) * 0x16e
    result[11] = (inp[27] ^ 0x6d) * 0xcc + (inp[13] ^ 0x6d) * -0x7c + (inp[5] ^ 0x6d) * -0x55 + (inp[21] ^ 0x6d) + (inp[21] ^ 0x6d) * 2 + (inp[24] ^ 0x6d) * 0xf6
    result[12] = (inp[29] ^ 0x66) * -0xe7 + (inp[6] ^ 0x66) * 0xc4 + (inp[16] ^ 0x66) * 0xf3 + (inp[26] ^ 0x66) * -0x4b + (inp[20] ^ 0x66) * -0x5d
    result[13] = (inp[22] ^ 0x1f) * 0xcc + (inp[21] ^ 0x1f) * -0xfd + (inp[25] ^ 0x1f) * -0x6a + (inp[14] ^ 0x1f) * -0x3d + (inp[13] ^ 0x1f) * 0x7d
    result[14] = (inp[15] ^ 0x2b) * -0xcf + (inp[13] ^ 0x2b) * 0x93 + (inp[17] ^ 0x2b) * 0x8f + (inp[9] ^ 0x2b) * 0xb2 + (inp[30] ^ 0x2b) * 0x1e
    result[15] = (inp[24] ^ 0xd) * -0x5a + (inp[30] ^ 0xd) * -100 + (inp[19] ^ 0xd) * -0x24 + (inp[21] ^ 0xd) * -0x6a
    result[16] = (inp[21] ^ 0x1e) * 0xe + (inp[9] ^ 0x1e) * 0x24 + (inp[12] ^ 0x1e) * 0xf6 + (inp[26] ^ 0x1e) * -0x35 + (inp[23] ^ 0x1e) * -0x1f
    result[17] = (inp[7] ^ 0x1f) * 0x8a + (inp[8] ^ 0x1f) * 0x71 + (inp[29] ^ 0x1f) * 0x7c + (inp[17] ^ 0x1f) * 6 + (inp[10] ^ 0x1f) * 0x95
    result[18] = (inp[6] ^ 0x23) * -0x49 + (inp[27] ^ 0x23) * -0x32 + (inp[24] ^ 0x23) * -0x1a + (inp[19] ^ 0x23) * 0xe8 + (inp[4] ^ 0x23) * -0xa6
    result[19] = (inp[28] ^ 0x87) * -0x46 + (inp[18] ^ 0x87) + (inp[18] ^ 0x87) * 8 + (inp[30] ^ 0x87) * 0xd4 + (inp[23] ^ 0x87) * -0x7c + (inp[24] ^ 0x87) * 0x1e
    result[20] = (inp[24] ^ 0xe9) * 0x20 + (inp[17] ^ 0xe9) * -99 + (inp[26] ^ 0xe9) * -0xae + (inp[9] ^ 0xe9) * -0x92 + (inp[8] ^ 0xe9) * 0xd7
    result[21] = (inp[23] ^ 0x3e) * -0xd8 + (inp[26] ^ 0x3e) * 10 + (inp[19] ^ 0x3e) * -9 + (inp[11] ^ 0x3e) * -0x10 + (inp[8] ^ 0x3e) * 0xdc
    result[22] = (inp[25] ^ 0xdf) * 0x5f + (inp[27] ^ 0xdf) * 0x43 + (inp[4] ^ 0xdf) * -0x94 + (inp[11] ^ 0xdf) * 0x50
    result[23] = (inp[19] ^ 0x6a) * 0x45 + (inp[4] ^ 0x6a) * 0x52 + (inp[17] ^ 0x6a) * -0xa9 + (inp[23] ^ 0x6a) * 0x6e + (inp[14] ^ 0x6a) * -0xdb
    result[24] = (inp[27] ^ 0x1b) * 0xd7 + (inp[29] ^ 0x1b) * -0x98 + (inp[11] ^ 0x1b) * 0x20 + (inp[23] ^ 0x1b) * 0x4c + (inp[4] ^ 0x1b) * 0x6e
    result[25] = (inp[4] ^ 1) * -0x11 + (inp[23] ^ 1) * -0x9e + (inp[7] ^ 1) * -0x87 + (inp[17] ^ 1) * -0xcd + (inp[18] ^ 1) * 0x93
    result[26] = (inp[5] ^ 0xd) * 0x2f + (inp[9] ^ 0xd) * 0x51 + (inp[16] ^ 0xd) * -0xf1 + (inp[8] ^ 0xd) * 0xff + (inp[21] ^ 0xd) * -0x12
    result[27] = inp[0]
    result[28] = inp[1]
    result[29] = inp[2]
    result[30] = inp[3]
    result[31] = inp[31]
    return result

Y = [
    0xca9, 0x5ae1, -0x5912, 0x5010, 0x3909, -0x2439, 0x1374, -0x2733, 0x3746, 0x578c, 0x35e4, 0x3a3a, -0x4997, 0x517, 0x45fd, -0x7f12, 0x2b33, 0x654d, -0x17e1, 0x6dce, -0x5c96, -0x6ae, 0x5e9c, -0x280d, 0x525e, -0x5132, -0xf85, ord("E"), ord("C"), ord("W"), ord("{"), ord("}")
]

X = [z3.BitVec(f"X{i}", 8) for i in range(32)]
s = z3.Solver()
z3_result = compute(X)

for i in range(32):
    s.add(X[i] >= 0x20)
    s.add(X[i] <= 0x7e)

for i in range(1, 32):
    s.add(z3_result[i] == Y[i])
print(s.check())

m = s.model()

for i in range(32):
    print(chr(m[X[i]].as_long()), end="")
    

sat
ECW{l1N34r_C0Nstr41n15_4r3_345y}