The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABV division as of Fri Jun 27 16:49:23 EDT 2014
Competition benchmarks = 6457 (total = 15091, unknown status = 4190, trivial = 4423)
| Solver | Errors | Solved | Not Solved | Remaining | CPU Time (on solved instances) | Weighted Medal Score (weight = 3.810) |
|---|---|---|---|---|---|---|
| Boolector (justification) | 0 | 6413 | 44 | 0 | 53176.27 | 3.758 |
| Boolector (dual propagation) | 0 | 6410 | 47 | 0 | 69040.03 | 3.755 |
| MathSATn | 0 | 6394 | 63 | 0 | 73535.00 | 3.736 |
| SONOLAR | 0 | 6386 | 71 | 0 | 53248.38 | 3.727 |
| CVC4 | 0 | 6352 | 105 | 0 | 78865.09 | 3.687 |
| Z3n | 0 | 6351 | 106 | 0 | 53957.15 | 3.686 |
| Yices2 | 1 | 6410 | 46 | 0 | 37112.15 | 3.755 |
| Kleaver-STP | 56 | 5827 | 574 | 0 | 1120.08 | 3.103 |
| Kleaver-portfolio | 91 | 5799 | 567 | 0 | 3403.29 | 3.073 |
n. Non-competitive.