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.
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.
- Spin-off project symlang: https://github.com/connglli/symlang