The 2014 SMT competition‘s QF_BV divison is over (benchmark tarball here), and the results are (copied from here):
| Solver | Errors | Solved | Not Solved | CPU time (solved instances) |
| Boolector | 0 | 2361 | 127 | 138077.59 |
| STP-CryptoMiniSat4 | 0 | 2283 | 205 | 190660.82 |
| [MathSAT] | 0 | 2199 | 289 | 262349.39 |
| [Z3] | 0 | 2180 | 308 | 214087.66 |
| CVC4 | 0 | 2166 | 322 | 87954.62 |
| 4Simp | 0 | 2121 | 367 | 187966.86 |
| SONOLAR | 0 | 2026 | 462 | 174134.49 |
| Yices2 | 0 | 1770 | 718 | 159991.55 |
| abziz_min_features | 9 | 2155 | 324 | 134385.22 |
| abziz_all_features | 9 | 2093 | 386 | 122540.04 |
First, let me congratulate Boolector by Armin Biere. STP came a not-so-close second. STP was meant to be submitted twice, once with MiniSat and once with CyrptoMiniSat4 — this is the only reason why the STP submission is called STP-CryptoMiniSat4. Unfortunately, the other submission could not be made because of some compilation problems.
About the results
There are a couple of things I would like to draw your attention to. First is the cumulated solving time of solved instances. Note how it decreases compared to MathSat and Z3. Note also the differences in the DIFF of the number of solved instances. It’s relatively small between 4Simp…MathSat(<40) and increases dramatically with STP and Boolector (with around 80 each). Another thing of interest is that STP is surrounded by commercial products: Boolector, Z3 and MathSAT are all products you have to pay for to use in a commercial setting. In contrast, the biggest issue with STP is that if the optional(!) CryptoMiniSat4 is linked in, it's LGPLv2 instead of MIT licensed. In other words, a lot of effort is in there, and it's all free. Sometimes free as in beer, sometimes free as in freedom.
About STP
Lately, a lot of work has been done on STP. If you look a the github repository, it has about 80 issues resolved, about 40 open, lots of pull requests, and a lot of commits. A group of people, namely (in nickname order): Dan Liew, Vijay Ganesh, Khoo Yit Phang, Ryan Govostes, Trevor Hansen, a lot of external contributors (e.g. Stephen McCamant) and myself have been working on it pretty intensively. It now has a an automated test facility and a robust build system besides all the code cleanup and other improvements.
It’s a great team and I’m happy to be a minor part of it. If you feel like you could contribute, don’t hesitate to fork the repo, make some changes, and ask for a pull request. The discussions on the pull requests can be pretty elaborate which makes for a nice learning experience for all involved. Come and join — next year hopefully we’ll win :)