\myheading{Now CBMC}

\renewcommand{\CURPATH}{CRC/CBMC}

Here I reimplement KLEE examples you already saw above.
All timings are when KLEE 3.0 running on AMD Ryzen 5 3600.

I'm not using \verb|klee_assume()| calls here, only standard \verb|assert()|'s.

\lstinputlisting[style=customc]{\CURPATH/CBMC_crc64_find.c}

\begin{lstlisting}[caption=Command to run]
% cbmc --trace --function main --z3 CBMC_crc64_find.c
\end{lstlisting}

\lstinputlisting{\CURPATH/CBMC_crc64_find.txt}

This result coincides with KLEE's result.

Now a string for CRC64(...)==0:

\lstinputlisting[style=customc]{\CURPATH/CBMC_crc64_find_2.c_part}

\lstinputlisting{\CURPATH/CBMC_crc64_find_2.txt}

Now a 16-byte string where each character is a nibble?
Or, in other word, 16-nibble hexadecimal string?
Or, in other words, 8-byte hexadecimal string?

\lstinputlisting[style=customc]{\CURPATH/CBMC_crc64_find_3.c_part}

\lstinputlisting{\CURPATH/CBMC_crc64_find_3.txt}

Yes, \verb|CRC64("8493a5648600c495")==0|, and this is very predictable:
we just need to find a 64-bit input for CRC64 so that it's output would be zero.
No magic here.

Again, CBMC can't find a string consisting only of \emph{0..9} characters, like KLEE.

\myhrule{}

Thanks to Martin Nyx Brain\footnote{\url{https://github.com/diffblue/cbmc/issues/5099}}, for help.