from z3.z3 import *
from ctypes import c_uint32


def int32(val):
    return c_uint32(val).value


a = 1103515245
c = 12345
m = 2147483647
seed = int32(1337)
seeds = []
STATE = [0x1e48add6, 0xaaa7550c, 0x18df53bf, 0xe6af1116]

start = [0x0, 0x0, 0x0, 0x0]

for i in range(2 * 4):
    seed = int32((int32(int32(int32(a) * int32(seed)) + int32(c)) % m))
    seeds.append(seed)
    print(hex(seed))


s = Solver()

user_input = BitVecs("ui0 ui1 ui2 ui3", 32)

for i in range(4):
    start[i] |= user_input[(i * 4)] << 24
    start[i] |= user_input[(i * 4)+1] << 16
    start[i] |= user_input[(i * 4)+2] << 8
    start[i] |= user_input[(i * 4)+3] << 0

for i in range(4):
    temp = start[i]
    temp *= 0xcafebeef
    temp += seeds[i*2]
    temp *= 0xfacefeed
    temp ^= seeds[i*2+1]

    s.add(STATE[i] == temp)

while s.check() == sat:
    m = s.model()
    block = []
    for var in m:
        block.append(var() != m[var])
    s.add(Or(block))

    string = ""
    for i in range(4):
        string += m[user_input[i]].as_string()
        temp = int32(0x61626364 * 0xcafebeef)-seeds[i]

        print(f"x * 0xcafebeef = {hex(temp)}")

    print(m)
    # print(string)
    for i in range(int(len(string)/2)):
        print(chr(int(string[i*2:i*2+2], 16)), end="")