SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Benchmarks

SMT-COMP 2018 will use a large subset of the benchmarks available within the 2018-05-20 release of SMT-LIB, as described in the competition rules.

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2018-05-20 on StarExec.

Main Track

All non-incremental SMT-LIB benchmarks are eligible for the main track. In total, there are 50 main track divisions. Division QF_SLIA, which contains strings, is experimental in 2018.

Logic Eligible Benchmarks Excluded Benchmarks
ABVFP 1
ALIA 42
AUFBVDTLIA 1709
AUFDTLIA 728
AUFLIA 4 32721
AUFLIRA 20011
AUFNIA2 0 31
AUFNIRA 1480
BV 5751
BVFP 24
FP 61
LIA 388
LRA 2419
NIA 14
NRA 3813
QF_ABV 15066
QF_ABVFP 18129
QF_ALIA 139
QF_ANIA 8
QF_AUFBV 31
QF_AUFLIA 1009 2941
QF_AUFNIA 17
QF_AX 551
QF_BV 40102
QF_BVFP 17215
QF_DT 8000
QF_FP 40300
QF_IDL 2193
QF_LIA 6947
QF_LIRA 7
QF_LRA 1649
QF_NIA 23876
QF_NIRA 3
QF_NRA 11489
QF_RDL 255
QF_SLIA 72705
QF_UF 7423 341
QF_UFBV 1224
QF_UFIDL 428
QF_UFLIA 583
QF_UFLRA 1284
QF_UFNIA 7
QF_UFNRA 36
UF 7562
UFBV 200
UFDT 4527
UFDTLIA 303
UFIDL 68
UFLIA 10137
UFLRA 15
UFNIA 3308
Total 333241 3603

1. All benchmarks in family 20170829-Rodin/ were excluded because they contained :named terms.
2. As there are no eligible benchmarks in SMT-LIB, AUFNIA is not actually a main track division in SMT-COMP 2018.

Application Track

In total, there are 21 application track divisions.

Logic Eligible Benchmarks Excluded Benchmarks Benchmarks with unknown status3 Benchmarks in SMT-LIB
ABVFP4 0 4 4
ALIA 24 0 24
ANIA 3 0 3
AUFNIRA 117 48 165
BV 17 1 18
BVFP4 0 10 10
LIA 6 0 6
LRA4 0 55 0 5
QF_ABV 15 0 15
QF_ABVFP4 0 9 9
QF_ALIA 44 0 44
QF_ANIA 5 0 5
QF_AUFBV 10 0 10
QF_AUFLIA 72 0 72
QF_BV 815 3 818
QF_BVFP 2 63 65
QF_FP 2 1 3
QF_LIA 69 0 69
QF_LRA 10 0 10
QF_NIA 10 0 10
QF_UF4 0 766 766
QF_UFBV 2327 0 2327
QF_UFLIA 780 0 780
QF_UFLRA 3058 0 3058
QF_UFNIA 1 0 1
UFLRA 1870 0 1870
Total 9257 5 905 10167

3. For the application track, a benchmark is ineligible if its first check-sat command has unknown status. Otherwise, (some non-empty prefix of) the benchmark is eligible.
4. As there are no eligible benchmarks in SMT-LIB, ABVFP, BVFP, LRA, QF_ABVFP and QF_UF are not actually application track divisions in SMT-COMP 2018.
5. The five benchmarks in incremental/LRA/20160930-Kopczynski-LOIS/ were excluded because they did not contain :status information.

Unsat-Core Track

All unsatisfiable main track benchmarks are eligible for the unsat-core track (with minor modifications, e.g., named assertions). In total, there are 44 unsat-core track divisions.

Logic Eligible Benchmarks All main track benchmarks
ABVFP6 0 1
ALIA 41 42
AUFBVDTLIA 25 1709
AUFDTLIA6 0 728
AUFLIA 3 4
AUFLIRA 19771 20011
AUFNIA6 0 0
AUFNIRA 1053 1480
BV 4937 5751
BVFP6 0 24
FP6 0 61
LIA 233 388
LRA 1539 2419
NIA 4 14
NRA 3801 3813
QF_ABV 4677 15066
QF_ABVFP 3934 18129
QF_ALIA 80 139
QF_ANIA 8 8
QF_AUFBV 25 31
QF_AUFLIA 516 1009
QF_AUFNIA 12 17
QF_AX 279 551
QF_BV 25700 40102
QF_BVFP 3174 17215
QF_DT 4422 8000
QF_FP 20026 40300
QF_IDL 816 2193
QF_LIA 3019 6947
QF_LIRA 5 7
QF_LRA 683 1649
QF_NIA 4842 23876
QF_NIRA 2 3
QF_NRA 5357 11489
QF_RDL 113 255
QF_SLIA6 0 72705
QF_UF 4330 7423
QF_UFBV 575 1224
QF_UFIDL 322 428
QF_UFLIA 183 583
QF_UFLRA 511 1284
QF_UFNIA 7 7
QF_UFNRA 11 36
UF 3442 7562
UFBV 97 200
UFDT 1863 4527
UFDTLIA6 0 303
UFIDL 57 68
UFLIA 7743 10137
UFLRA 10 15
UFNIA 2457 3308
Total 130705 333241

6. As there are no eligible benchmarks in SMT-LIB, ABVFP, AUFDTLIA, AUFNIA, BVFP, FP, QF_SLIA and UFDTLIA are not actually unsat-core track divisions in SMT-COMP 2018.