Rating:

```
from z3 import *
import string
flag=bytes.fromhex("07740277000105007572727106040400")
first=flag[:8]
second=flag[8:]
def test(inp,target):
for i in range(8):
xorer=inp[i]
for j in range(8):
inp[j]^=xorer
assert inp==target
def find(target):
flag=[BitVec(f"x{i}",8) for i in range(8)]
k=flag[:]
for i in range(8):
xorer=k[i]
for j in range(8):
k[j]^=xorer

s=Solver()
### only uppercase hex character
for i in range(len(flag)):
s.add(flag[i]<0x7f)
s.add(0x20<=flag[i])
for j in string.printable[:-6]:
if(j not in "0123456789ABCDEF"):
s.add(flag[i]!=ord(j))

for i in range(len(target)):
s.add(k[i]==target[i])
print(s.check())
m=s.model()
l=[]
for i in flag:
l.append(m[i].as_long())
return bytearray(l).decode()

flag_first=find(first)
flag_second=find(second)
test(bytearray(flag_first.encode()),first)
test(bytearray(flag_second.encode()),second)
print("ENO{"+flag_first+flag_second+"}")
```

Original writeup (https://hackmd.io/@vidner/nullcon-sksd#Bicycle-rev).