babymix_solution.py

from z3 import *

conditions = ["(flag[12] - flag[17] + flag[12] + flag[8] == 153)",
"(flag[10] + flag[21] + (flag[19] ^ flag[2]) == 217 )",
"((flag[5] ^ flag[16]) + flag[16] + flag[3] + (flag[0] ^ flag[16]) == 232 )",
"(flag[10] + flag[3] + flag[3] - flag[19] + (flag[19] ^ flag[0]) == 328 )",
"(flag[10] - flag[8] + flag[2] - flag[19] == 74 )",
"(flag[17] - flag[1] + flag[4] + flag[11] + flag[17] - flag[9] == 166 )",
"(flag[14] + flag[10] + flag[18] - flag[9] + flag[5] + flag[10] == 413 )",
"(flag[5] - flag[16] + flag[8] - flag[12] + flag[17] - flag[13] + flag[11] - flag[2] + flag[1] + flag[21] == 98 )",
"((flag[19] ^ flag[13]) + flag[6] - flag[13] + flag[17] - flag[11] + (flag[16] ^ flag[12]) == 85 )",
"(flag[4] - flag[16] + (flag[2] ^ flag[7]) == 77 )",
"(flag[8] - flag[17] + flag[14] - flag[3] + (flag[8] ^ flag[14]) + flag[5] + flag[1] + flag[7] + flag[10] == 384 )",
"(flag[4] - flag[0] + flag[2] - flag[4] + flag[15] - flag[21] + flag[17] + flag[2] == 265 )",
"(flag[5] - flag[18] + flag[17] - flag[4] + flag[15] + flag[2] + flag[21] - flag[18] + flag[7] + flag[6] == 250 )",
"(flag[21] - flag[19] + flag[7] - flag[18] + flag[16] - flag[21] + (flag[12] ^ flag[18]) == 75 )",
"((flag[10] ^ flag[2]) + flag[2]+ flag[7] + flag[20] + flag[13] + (flag[3] ^ flag[16]) + flag[9] + flag[6] == 621 )",
"(flag[8] - flag[3] + (flag[14] ^ flag[2]) + flag[11] + flag[0] + flag[1] - flag[19] == 283 )",
"(flag[16] - flag[14] + (flag[0] ^ flag[11]) + (flag[0] ^ flag[14]) + flag[13] - flag[19] == 106 )",
"(flag[19] + flag[10] + flag[10] + flag[19] + flag[0] - flag[20] + flag[3] - flag[18] == 297 )",
"(flag[0] - flag[15] + flag[20] + flag[18] == 156 )",
"(flag[13] - flag[8] + flag[10] - flag[20] + flag[3] - flag[17] == 85 )",
"(flag[3] - flag[17] + flag[19] + flag[4] + (flag[12] ^ flag[17]) + flag[10] - flag[2] == 160 )",
"(flag[11] - flag[21] + flag[12] - flag[10] == 36 )",
"((flag[18] ^ flag[19]) + flag[6] - flag[16] + (flag[5] ^ flag[16]) == 102 )",
"(flag[6] - flag[13] + (flag[10] ^ flag[15]) + flag[21] - flag[5] == -48 )",
"((flag[5] ^ flag[3]) + flag[12] - flag[11] + (flag[6] ^ flag[4]) == 29 )",
"(flag[6] - flag[14] + flag[9] - flag[2] + flag[8] - flag[15] + flag[21] - flag[11] == -109 )",
"(flag[19] - flag[7] + flag[0] + flag[16] + flag[11] + flag[17] == 361 )"]


flag = [BitVec(f'arr[{i}]',9) for i in range(32)] # 32 -> length of the flag!

s = Solver()

for i in conditions:
    s.add(eval(i))

print(s.check())
print(s.model())

print("FLAG: ")

arr = [0] * 32

arr[2] = 120
arr[8] = 108
arr[5] = 116
arr[6] = 95
arr[9] = 108
arr[14] = 101
arr[4] = 105
arr[0] = 109
arr[16] = 104
arr[18] = 114
arr[3] = 95
arr[11] = 116
arr[20] = 49
arr[10] = 95
arr[7] = 52
arr[19] = 33 
arr[21] = 33
arr[12] = 48
arr[1] = 49
arr[15] = 116
arr[13] = 103
arr[17] = 51

for i in arr:
    print(chr(i), end="")