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.
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.