Link to paper: https://dl.acm.org/doi/pdf/10.1145/3503222.3507764

Thanks!

Agreed; such an analysis/study would be nice to have. It is worth to point that the small tests were the results of test input reduction --- the original tests were often quite large. Many of the bugs were due to incorrect handling of corner/boundary cases, such as "division by zero" (which has well-defined semantics in SMT-LIB).

To add a quick follow-up to dwinterer's nice reply, note please Z3's current support for nonlinear arithmetic and string logics is more advanced than CVC4's, where many of the detected bugs in Z3 occurred.

Figure 8 in the OOPSLA paper (https://arxiv.org/pdf/2004.08799.pdf) provides a breakdown of the bugs found in different logics for Z3 and CVC4.

Project website: https://testsmt.github.io/

For information, links to all the bugs that we reported so far (in GCC/LLVM/CompCert/ICC and Scala) can be found at http://web.cs.ucdavis.edu/~su/emi-project/: 728 in Clang/LLVM (~250 were miscompilations); 783 in GCC.

(Also refer to http://helloqirun.github.io/projects/spe/spe.html for additional bugs reported so far in Rust and Rust bindgen.)

Link to our talk slides: http://www.cs.ucdavis.edu/~su/publications/emi-talk.pdf