Benchmarking theorem provers for programming tasks: yices vs. z3

This is a very limited and naive view of those kind of benchmarks. Of course z3 is at the bottom of the benchmarks in most cases, but it comes with a nice python api, so people will still use that.

For real usecases there exists multiple of extremely specialized solvers, and there exist yearly competitions to find the fastest for each problem set. http://www.satcompetition.org/

For picat we use mostly lingeling, google has the very good or-tools library, and there are dozens more much better than z3. Eg I find cbmc extremely useful, because it allows the statements to be written in the C language and results are calculated based on the C expressions and statements. You don't have to translate them to an mostly obscure language or python.

Eg for 2018 there were these tracks: "2018 consisted of four tracks: In addition to the Main Track for sequential SAT solvers, a Random SAT track (for solvers focusing on efficiently solving satisfiable randomly generated SAT instances), Parallel track (for parallel SAT solvers designed for computers with multiple CPUs or CPU cores), and a special No-Limits track where solver source code and solution certificates are not required and portfolios of any nature are allowed) were organized. Additionally, “Glucose hacks”, i.e., solvers based on small modifications to the Glucose 3.0 CDCL SAT solver, were encouraged to be submitted to the main track with the intention of separately awarding the best Glucose hack."