SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2016

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Competition-Wide Scoring for the Main Track

Competition results as of Thu Jul 7 07:24:34 GMT

Sequential PerformancesParallel Performances
RankSolver Score
- Z3n 185.09
1 CVC4 180.95
2 Yices2 119.29
3 veriT-dev 75.11
- MathSat5n 74.06
4 SMTInterpol 68.91
5 vampire_smt_4.1_parallel 65.36
6 vampire_smt_4.1 64.90
7 Boolector 32.52
8 OpenSMT2 18.83
9 toysmt 10.52
10 raSAT 0.4 8.97
11 Boolector (preprop) 8.74
12 stp-cms-st 8.52
13 stp-cms-exp 8.16
14 Minkeyrink 8.02
15 stp-cms-mt 8.02
16 ABC_glucose 7.77
17 MapleSTP 6.91
18 raSAT 0.3 6.82
19 MapleSTP-mt 6.57
20 stp-minisat-st 6.18
21 ABC_default 5.01
22 ProB 3.95
23 AProVE 2.68
24 SMT-RAT -38.67
25 Q3B -7120.68
RankSolver Score
- Z3n 185.09
1 CVC4 181.19
2 Yices2 119.29
3 veriT-dev 75.11
- MathSat5n 74.07
4 SMTInterpol 68.95
5 vampire_smt_4.1_parallel 65.62
6 vampire_smt_4.1 64.90
7 Boolector 32.52
8 OpenSMT2 18.83
9 toysmt 10.52
10 raSAT 0.4 9.07
11 Boolector (preprop) 8.74
12 Minkeyrink 8.71
13 stp-cms-mt 8.58
14 stp-cms-st 8.52
15 stp-cms-exp 8.16
16 ABC_glucose 7.77
17 MapleSTP-mt 7.38
18 MapleSTP 6.91
19 stp-minisat-st 6.18
20 ABC_default 5.01
21 ProB 3.95
22 AProVE 2.68
23 SMT-RAT -38.67
24 raSAT 0.3 -6638.27
25 Q3B -7323.52

n. Non-competitive.