Given were some kind of combined output from three different LFSRs, the task was to reverse their initial state. This was no match for Z3:
#!/usr/bin/env python3
from z3 import *
import binascii, hashlib
ks = bytes(map(ord, open('keystream', 'rb').read().decode()))
k = int(binascii.hexlify(ks), 16)
n = len(ks)*8
a = [Bool('a'+str(i)) for i in range(n+48)]
b = [Bool('b'+str(i)) for i in range(n+48)]
c = [Bool('c'+str(i)) for i in range(n+48)]
s = Solver()
for i in range(n):
s.add(a[i+48] == Xor(a[i], a[i+25]))
s.add(b[i+48] == Xor(b[i], b[i+34]))
s.add(c[i+48] == Xor(c[i], c[i+6]))
s.add(Xor(Xor(And(a[i+48], b[i+48]), And(b[i+48], c[i+48])), And(c[i+48], a[i+48])) == (k&(1<<(n-1-i)) != 0))
s.check()
m = s.model()
ma = [m[a[i]] for i in range(48)]
mb = [m[b[i]] for i in range(48)]
mc = [m[c[i]] for i in range(48)]
init1 = binascii.unhexlify(format(int(''.join(map(lambda x: '1' if x else '0', ma)), 2), '06x'))
init2 = binascii.unhexlify(format(int(''.join(map(lambda x: '1' if x else '0', mb)), 2), '06x'))
init3 = binascii.unhexlify(format(int(''.join(map(lambda x: '1' if x else '0', mc)), 2), '06x'))
print("flag{"+hashlib.sha256(init1+init2+init3).hexdigest()+"}")