z3.py

from z3 import *

s = Solver()
keystream = BitVec('keystream',258)
#keystream = 0x989a137e549e7cd1b4f589c3498d5818838a2c5b74e56a47a99a1bb7c8dc1989

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

#print(''.join(format(x, '02X') for x in keystream.to_bytes(32,'little')))
#keystream=next(keystream)
#print(''.join(format(x, '02X') for x in keystream.to_bytes(32,'little')))

#if(keystream==0xedeb3d03d7e3875a9714de657ed54c2dc4db66c9173d2be8aeeb28907d462ede):
#  print("sat!!!")

keystreamnew=keystream
for i in range(128):
  keystreamnew = next(keystreamnew)

#s.add(keystreamnew==0xedeb3d03d7e3875a9714de657ed54c2dc4db66c9173d2be8aeeb28907d462ede)
s.add(keystreamnew==0x52cc2cc124e3f2c28f5b9123904dc015babfd5c0988cb8d670f190fbb57593e2)

res=s.check()
valueres=int(str(s.model()[keystream]))
print(''.join(format(x, '02X') for x in valueres.to_bytes(33,'little')))
s = Solver()
s.add(keystreamnew==valueres)
res=s.check()
print(''.join(format(x, '02X') for x in int(str(s.model()[keystream])).to_bytes(33,'little')))

while(res==sat):
  resnum=int(str(s.model()[keystream]))
  #print(resnum)
  print(''.join(format(x, '02X') for x in resnum.to_bytes(33,'little')))
  #print(s.model()[keystream])
  s.add(Or(keystream!=s.model()[keystream]))
  res=s.check()