SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2014

Rules
Benchmarks
Tools
Specs
Participants
Results
Report

Medal Standings

Competition results for the Medal standings division as of Fri Jun 27 16:49:23 EDT 2014

Gold/Silver Medal Current Standings

The gold and silver medal winners are the first and second place measured by absence of errors and the most solved problems, measured by a weighted, non-linear metric across divisions.

Solver % Complete Weighted
Errors
Weighted
Solved
veriT 100% 0.000 25.325
SMTInterpol 100% 0.000 22.831
CVC3 100% 0.000 9.618
SONOLAR 100% 0.000 5.978
AProVE 100% 0.000 3.776
Boolector (justification) 100% 0.000 3.758
Boolector (dual propagation) 100% 0.000 3.755
OpenSMT2 100% 0.000 3.582
Boolector 100% 0.000 3.058
STP-CryptoMiniSat4 100% 0.000 2.859
4Simp 100% 0.000 2.468
raSAT 100% 0.000 0.000
Yices2 100% 3.810 38.624
CVC4 100% 7.283 54.152
abziz_min_features 100% 30.563 2.548
abziz_all_features 100% 30.563 2.403
Kleaver-STP 100% 213.362 3.103
Kleaver-portfolio 100% 346.713 3.073

Bronze medal

The bronze medal is awarded to the winner of the QF_BV division.

An Alternate Scoring Metric

The organizers also considered a different metric for gold/silver medals. We officially adopted the one above, as expressed in the competition rules, since it emphasizes soundness of solvers (a solver with an error in any division scores lower than solvers with no errors, even when they compete in fewer divisions). In the alternate metric, a division without errors contributes the squared fraction of solved instances weighted by the log10 of the number of benchmarks in the division; a division with errors contributes the negative of the division’s weight times the number of errors. For comparative information only, the table below shows rankings using this metric.

Solver % Complete Alternate
Metric
CVC4 100% 43.509
Yices2 100% 31.059
veriT 100% 25.325
SMTInterpol 100% 22.831
CVC3 100% 9.618
SONOLAR 100% 5.978
AProVE 100% 3.776
Boolector (justification) 100% 3.758
Boolector (dual propagation) 100% 3.755
OpenSMT2 100% 3.582
Boolector 100% 3.058
STP-CryptoMiniSat4 100% 2.859
4Simp 100% 2.468
raSAT 100% 0.000
abziz_min_features 100% -30.563
abziz_all_features 100% -30.563
Kleaver-STP 100% -213.362
Kleaver-portfolio 100% -346.713