z3_seed_solver.py

from z3 import *

SEED_SIZE=48
SALT_VALUES = [273991342780504,178948312324771,97321158527664,74524266130753,78222244435754,254886856462562,258708074213289]

s = Solver()
const_seed = BitVec('seed', SEED_SIZE)

for i, val in enumerate(SALT_VALUES):
    salt = BitVec(f'salt{i}', SEED_SIZE)
    s.add(salt == val)

    result = BitVec(f'result{i}', 48)
    result = ((const_seed + salt) ^ 0x5deece66d) * 0x5deece66d + 0xB
    # ULT - unsigned less than
    s.add(ULT(result, 90_000_000_000_000))

s.add(const_seed > 0)

if s.check() == sat:
    m = s.model()
    print('seed:', m[const_seed])