z3b.py

from z3 import *

keystream = BitVec('keystream',258)

def next(x):
  x = (x & 1) << 257 | x << 1 | x >> 255
  y = 0
  for i in range(256):
    i0=(x>>i)&1
    i1=((x>>i)&2)>>1
    i2=((x>>i)&4)>>2
    y|=(i0^(i1|i2))<<i
  return y

keystreamnew=next(keystream)

oldres=0x52cc2cc124e3f2c28f5b9123904dc015babfd5c0988cb8d670f190fbb57593e2
for l in range(128):
  s=Solver()
  s.add((keystream&0x30000000000000000000000000000000000000000000000000000000000000000)==0)
  s.add(keystreamnew==oldres)
  res=s.check()
  resultnum=s.model()[keystream]
  print(str("%.064x" % resultnum.as_long()))
  oldres=resultnum.as_long()

print('Flag: '+oldres.to_bytes(32,'little').decode())