lcg-z3.py

from z3 import BitVec, Solver

A = 0x5d588b656c078965
B = 0x269ec3

BITS = 64
M = 2**BITS
SHIFT = BITS - 1
K = 64

def f(x):
    return (A * x + B) % M

actuals = [0 for i in range(K)]

x0 = [0 for i in range(K)]
a = [1 for i in range(K)]

for i in range(1, K):
    x0[i] = f(x0[i - 1])
    a[i] = A * a[i - 1] % M

n = BitVec("n", BITS)
s = Solver()

output = [((x0[i] + n * a[i]) & (M - 1)) >> SHIFT for i in range(K)]

for i in range(K):
    s.add(output[i] == actuals[i])

print(s.check())
m = s.model()
print(m)