Tags: z3 re
Rating: 1.7
Analyze the binary in ghidra to find the expression to clear to win. Z3 to find the combination to get the correct result
**Follow/Message me at https://twitter.com/pwntheweb for queries :#**
```
from z3 import *
v = []
s = Solver()
for i in range(23):
e = BitVec('v'+str(i), 64)
v.append(e)
s.add(e >= 0)
s.add(e <= 255)
s.add()
s.add(v[0] ^ v[1] == 63)
s.add(v[1] ^ v[2] == 11)
s.add(v[2] ^ v[3] == 39)
s.add(v[3] ^ v[4] == 51)
s.add(v[4] ^ v[5] == 65)
s.add(v[5] ^ v[6] == 79)
s.add(v[6] ^ v[7] == 59)
s.add(v[7] ^ v[8] == 27)
s.add(v[8] ^ v[9] == 33)
s.add(v[9] ^ v[10] == 50)
s.add(v[10] ^ v[11] == 115)
s.add(v[11] ^ v[12] == 121)
s.add(v[12] ^ v[13] == 43)
s.add(v[13] ^ v[14] == 58)
s.add(v[14] == v[15])
s.add(v[15] ^ v[16] == 2)
s.add(v[16] ^ v[17] == 56)
s.add(v[17] ^ v[18] == 29)
s.add(v[18] ^ v[19] == 3)
s.add(v[19] ^ v[20] == 4)
s.add(v[20] ^ v[21] == 73)
s.add(v[21] ^ v[22] == 97)
s.add(v[22] == 88)
print(s.check())
values=(s.model())
print values
```