TL;DR: Lazily recover the random numbers with z3, instead of trying to reverse the bit masking. Feed results into randcrack to predict the next outputs. Runs in a few seconds.

The vulnerability here is that the random numbers from the Mersenne Twister can be recovered with 624 outputs of full bitlength. Since python also uses the same PRNG, we can utilize randcrack to recover the PRNG state. No need to brute-force the seed. Randcrack takes in exactly 624x 32-bit integers, and starts predicting numbers from that point on. Please note that either something changed server side after solving this challenge, or I got lucky on my first run, because new runs seem to not provide the flag anymore. I suspect this is due to a mismatch between signed and unsigned numbers or something. It worked fine on my first go, so didn't bother debugging this for the writeup. Just know that it's not 100%.

- UnblvR

```python
from z3 import *
from socket import socket
from randcrack import RandCrack

ALPHA = "BCDGPTVZ"
rc = RandCrack()

s = socket()
s.connect(("misc.hsctf.com", 9988))
data = recvuntil(s, b"letters are being said.\n").decode()
lines = data.split('\n')[8:-2]
assert len(lines) == 216

for i in range(8, 216): #Need exactly 624 integers out of 648, so skip the 8*3=24 first
v1 = BitVec("v1", 32)
v2 = BitVec("v2", 32)
v3 = BitVec("v3", 32)
results = list(map(ALPHA.index, lines[i]))
z = Solver()
z.add((v2 >> 0x1F & 0x1 | v3 >> 0x0 & 0x3) == results[0])
z.add((v1 >> 0x09 & 0x7) == results[1])
z.add((v3 >> 0x05 & 0x7) == results[2])
z.add((v3 >> 0x08 & 0x7) == results[3])
z.add((v1 >> 0x15 & 0x7) == results[4])
z.add((v1 >> 0x06 & 0x7) == results[5])
z.add((v3 >> 0x1D & 0x7) == results[6])
z.add((v1 >> 0x1B & 0x7) == results[7])
z.add((v2 >> 0x04 & 0x7) == results[8])
z.add((v2 >> 0x0D & 0x7) == results[9])
z.add((v2 >> 0x0A & 0x7) == results[10])
z.add((v3 >> 0x1A & 0x7) == results[11])
z.add((v2 >> 0x16 & 0x7) == results[12])
z.add((v3 >> 0x17 & 0x7) == results[13])
z.add((v2 >> 0x1C & 0x7) == results[14])
z.add((v3 >> 0x14 & 0x7) == results[15])
z.add((v2 >> 0x01 & 0x7) == results[16])
z.add((v3 >> 0x11 & 0x7) == results[17])
z.add((v1 >> 0x00 & 0x7) == results[18])
z.add((v2 >> 0x13 & 0x7) == results[19])
z.add((v1 >> 0x18 & 0x7) == results[20])
z.add((v3 >> 0x0B & 0x7) == results[21])
z.add((v2 >> 0x19 & 0x7) == results[22])
z.add((v2 >> 0x10 & 0x7) == results[23])
z.add((v1 >> 0x03 & 0x7) == results[24])
z.add((v1 >> 0x12 & 0x7) == results[25])
z.add((v1 >> 0x0F & 0x7) == results[26])
z.add((v3 >> 0x02 & 0x7) == results[27])
z.add((v1 >> 0x0C & 0x7) == results[28])
z.add((v2 >> 0x07 & 0x7) == results[29])
z.add((v3 >> 0x0E & 0x7) == results[30])
z.add((v1 >> 0x1E & 0x3 | v2 >> 0x00 & 0x1) == results[31])
if z.check() == sat:
m = z.model()
rc.submit((m[v1]).as_long())
rc.submit((m[v2]).as_long())
rc.submit((m[v3]).as_long())
#print([m[v1], m[v2], m[v3]])

v1 = rc.predict_randrange(0, 4294967295)
v2 = rc.predict_randrange(0, 4294967295)
v3 = rc.predict_randrange(0, 4294967295)

send(s, str(ALPHA[v1 >> 0x1E & 0x3 | v2 >> 0x00 & 0x1]))
send(s, str(ALPHA[v1 >> 0x09 & 0x7]))
send(s, str(ALPHA[v3 >> 0x05 & 0x7]))
send(s, str(ALPHA[v3 >> 0x08 & 0x7]))
send(s, str(ALPHA[v1 >> 0x15 & 0x7]))
send(s, str(ALPHA[v1 >> 0x06 & 0x7]))
send(s, str(ALPHA[v3 >> 0x1D & 0x7]))
send(s, str(ALPHA[v1 >> 0x1B & 0x7]))
send(s, str(ALPHA[v2 >> 0x04 & 0x7]))
send(s, str(ALPHA[v2 >> 0x0D & 0x7]))
send(s, str(ALPHA[v2 >> 0x0A & 0x7]))
send(s, str(ALPHA[v2 >> 0x16 & 0x7]))
send(s, str(ALPHA[v3 >> 0x1A & 0x7]))
send(s, str(ALPHA[v3 >> 0x17 & 0x7]))
send(s, str(ALPHA[v2 >> 0x1C & 0x7]))
send(s, str(ALPHA[v3 >> 0x14 & 0x7]))
send(s, str(ALPHA[v2 >> 0x01 & 0x7]))
send(s, str(ALPHA[v1 >> 0x00 & 0x7]))
send(s, str(ALPHA[v3 >> 0x11 & 0x7]))
send(s, str(ALPHA[v2 >> 0x13 & 0x7]))
send(s, str(ALPHA[v1 >> 0x18 & 0x7]))
send(s, str(ALPHA[v3 >> 0x0B & 0x7]))
send(s, str(ALPHA[v2 >> 0x19 & 0x7]))
send(s, str(ALPHA[v2 >> 0x10 & 0x7]))
send(s, str(ALPHA[v1 >> 0x03 & 0x7]))
send(s, str(ALPHA[v1 >> 0x12 & 0x7]))
send(s, str(ALPHA[v1 >> 0x0F & 0x7]))
send(s, str(ALPHA[v1 >> 0x0C & 0x7]))
send(s, str(ALPHA[v2 >> 0x07 & 0x7]))
send(s, str(ALPHA[v3 >> 0x0E & 0x7]))
send(s, str(ALPHA[v2 >> 0x1F & 0x1 | v3 >> 0x0 & 0x3]))
print(s.recv(1024))
```