\myheading{Linear congruential generator}

This is popular \ac{PRNG} from OpenWatcom \ac{CRT} library: \url{https://github.com/open-watcom/open-watcom-v2/blob/d468b609ba6ca61eeddad80dd2485e3256fc5261/bld/clib/math/c/rand.c}.

What expression it generates on each step?

\lstinputlisting[style=custompy]{\CURPATH/5_LCG/LCG.py}

\lstinputlisting{\CURPATH/5_LCG/1.txt}

Now if we once got several values from this PRNG, like 4583, 16304, 14440, 32315, 28670, 12568..., how would we
recover the initial seed?
The problem in fact is solving a system of equations:

\begin{lstlisting}
((((initial_seed*1103515245)+12345)>>16)&32767)==4583
((((((initial_seed*1103515245)+12345)*1103515245)+12345)>>16)&32767)==16304
((((((((initial_seed*1103515245)+12345)*1103515245)+12345)*1103515245)+12345)>>16)&32767)==14440
((((((((((initial_seed*1103515245)+12345)*1103515245)+12345)*1103515245)+12345)*1103515245)+12345)>>16)&32767)==32315
\end{lstlisting}

As it turns out, Z3 can solve this system correctly using only two equations:

\lstinputlisting[style=custompy]{\CURPATH/5_LCG/Z3_solve.py}

\begin{lstlisting}
[x = 11223344]
\end{lstlisting}

(Though, it takes $\approx 20$ seconds on my ancient Intel Atom netbook.)