It's hard to cross check since you didn't mention what you consider are good answers, but the quick answer snippet on Kagi says:

> The Yogar-CBMC and JCBMC solvers are notable multi-threaded variants of the CBMC (C Bounded Model Checker) framework: ...

Followed by further details and references. The search results themselves look relevant and reasonable to me, but again, outside my area of expertise.

Both are bad answers

Okay and why is that?

I was asking for multi-threaded solvers supported by CBMC, not multi-threaded CBMC, which is 1% of the runtime of large models.

I'm trying to find proofs for strstr implementations, like Morris-Pratt in C. JCBMC is for Java programs.

Good answers would be Z3, yices2, CVC5, Kisssat. Bad answers would be CaDiCaL, minisat2 (the default), and all the other supported single threaded solvers for the dimacs and ipasir interface for the SAT problems (which are much simplier than SMT problems).

Just unrolling the loops and comparing to a small brute force strstr leads to very large models, which would need to run in several minutes, compared to the typical 20s. I'm considering running it on one of my big work machines with a parallel solver. Out of the 220 strstr's I suspect several of them to be wrong. I know that they are wrong, but CBMC gives me counterexamples where they would break exactly, and why. Better than a fuzzer, which just guesses around.

Kagi answers that there is "CBMC", which is single-threaded, but that there are extensions "Deagle" and "Yogar-CBMC" that provide multi-threading for CBMC. It gives links to the papers for all three, however some of them are closed access (or in other words, fact checked, unlike arxiv).