\myheading{MK85 toy-level SMT-solver}

\leveldown{}

\renewcommand{\CURPATH}{solvers/MK85}

Thanks to PicoSAT SAT solver, its performance on small and simple bitvector examples is comparable to Z3.
In many cases, it's used instead of Z3, whenever you see \texttt{from MK85 import *} in Python file.

\input{\CURPATH/adder/main}
\input{\CURPATH/optimization/main}
\input{\CURPATH/shifter_EN}
\input{\CURPATH/MaxSMT/main}

\levelup{}