SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2015

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

Competition-Wide Scoring for the Main Track

Competition results as of Fri Oct 30 12:49:29 GMT

Sequential PerformanceParallel Performance Sequential Performance (industrial)Parallel Performance (industrial)
RankSolver Score
- z3n 159.36
1 CVC4 144.67
2 CVC4 (exp) 140.47
3 Yices 101.91
- MathSatn 79.77
4 veriT 70.68
5 SMTInterpol 68.31
6 CVC3 24.44
7 Boolector (QF_AUFBV) 16.61
8 raSAT 13.52
9 Boolector (QF_BV) 10.06
10 STP-CMSat4 9.96
11 OpenSMT2 8.75
12 Yices2-NL 8.64
13 AProVE 8.61
14 SMT-RAT (parallel) 6.96
15 OpenSMT2 (parallel) -17.60
16 SMT-RAT -130.02
17 STP-CMSat4 (mt-v15) -142.54
18 STP-CMSat4 (v15) -162.91
19 STP-MiniSAT (v15) -162.91
RankSolver Score
- z3n 159.36
1 CVC4 144.74
2 CVC4 (exp) 140.51
3 Yices 101.91
- MathSatn 79.77
4 veriT 70.68
5 SMTInterpol 68.44
6 CVC3 24.44
7 Boolector (QF_AUFBV) 16.61
8 raSAT 13.52
9 Boolector (QF_BV) 10.06
10 STP-CMSat4 9.96
11 OpenSMT2 8.75
12 Yices2-NL 8.64
13 AProVE 8.61
14 SMT-RAT (parallel) 6.97
15 OpenSMT2 (parallel) -17.60
16 SMT-RAT -130.02
17 STP-CMSat4 (mt-v15) -142.54
18 STP-CMSat4 (v15) -162.91
19 STP-MiniSAT (v15) -162.91
RankSolver Score
- z3n 139.34
1 CVC4 124.59
2 CVC4 (exp) 120.49
3 Yices 81.64
4 veriT 60.94
- MathSatn 60.27
5 SMTInterpol 47.87
6 CVC3 25.19
7 Boolector (QF_AUFBV) 16.61
8 raSAT 13.59
9 Boolector (QF_BV) 10.04
10 STP-CMSat4 10.00
11 Yices2-NL 8.71
12 AProVE 8.60
13 SMT-RAT (parallel) 7.15
14 OpenSMT2 1.10
15 OpenSMT2 (parallel) 1.10
16 SMT-RAT -119.71
17 STP-CMSat4 (mt-v15) -141.72
18 STP-CMSat4 (v15) -161.97
19 STP-MiniSAT (v15) -161.97
RankSolver Score
- z3n 139.34
1 CVC4 124.63
2 CVC4 (exp) 120.51
3 Yices 81.64
4 veriT 60.94
- MathSatn 60.27
5 SMTInterpol 47.97
6 CVC3 25.19
7 Boolector (QF_AUFBV) 16.61
8 raSAT 13.59
9 Boolector (QF_BV) 10.04
10 STP-CMSat4 10.00
11 Yices2-NL 8.71
12 AProVE 8.60
13 SMT-RAT (parallel) 7.16
14 OpenSMT2 1.10
15 OpenSMT2 (parallel) 1.10
16 SMT-RAT -119.71
17 STP-CMSat4 (mt-v15) -141.72
18 STP-CMSat4 (v15) -161.97
19 STP-MiniSAT (v15) -161.97

n. Non-competitive.