SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Benchmarks

SMT-COMP 2020 will use a large subset of the benchmarks available within the 2020-04-25 release of SMT-LIB, as described in the competition rules.

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2020-04-25 on StarExec.

Single Query Track

In total there are 70 divisions in the Single Query Track.
You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.

Division Number of Included Benchmarks
ABV 169
ABVFP 30
ABVFPLRA 75
ALIA 19
AUFBVDTLIA 683
AUFBVDTNIAn 1
AUFDTLIA 147
AUFDTLIRA 4878
AUFDTNIRA 300
AUFFPDTLIRA 154
AUFFPDTNIRAn 13
AUFLIA 1310
AUFLIRA 1346
AUFNIA 3
AUFNIRA 300
BV 696
BVFP 224
BVFPLRA 185
FP 993
FPLRA 27
LIA 300
LRA 802
NIA 17
NRA 93
QF_ABV 3385
QF_ABVFP 500
QF_ABVFPLRA 74
QF_ALIA 116
QF_ANIA 94
QF_AUFBV 34
QF_AUFLIA 467
QF_AUFNIA 9
QF_AX 300
QF_BV 6861
QF_BVFP 394
QF_BVFPLRA 168
QF_DT 4
QF_FP 270
QF_FPLRA 57
QF_IDL 834
QF_LIA 2508
QF_LIRA 7
QF_LRA 429
QF_NIA 9195
QF_NIRA 2
QF_NRA 2230
QF_RDL 247
QF_S 927
QF_SLIA 27033
QF_UF 2800
QF_UFBV 217
QF_UFFP 2
QF_UFIDL 300
QF_UFLIA 300
QF_UFLRA 432
QF_UFNIA 300
QF_UFNRA 27
UF 2291
UFBV 72
UFDT 1223
UFDTLIA 277
UFDTLIRA 4296
UFDTNIA 1
UFDTNIRA 736
UFFPDTLIRA 373
UFFPDTNIRA 21
UFIDL 20
UFLIA 2278
UFLRA 7
UFNIA 5041
Total 89924

Incremental Track

In total there are 32 divisions in the Incremental Track.
You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.

Division Number of Included Benchmarks
ALIA 24
ANIA 3
AUFNIRA 165
BV 18
BVFP 1
LIA 6
LRA 5
QF_ABV 508
QF_ABVFP 62
QF_ALIA 44
QF_ANIAn 5
QF_AUFBV 31
QF_AUFBVLIAn 300
QF_AUFBVNIAn 44
QF_AUFLIA 72
QF_BV 1035
QF_BVFP 119
QF_FP 1
QF_LIA 69
QF_LRA 10
QF_NIA 10
QF_UF 306
QF_UFBV 932
QF_UFBVLIAn 179
QF_UFFP 1
QF_UFLIA 309
QF_UFLRA 1223
QF_UFNIA 1
UF 2031
UFLRA 748
UFNIA 2029
UFNRA 5
Total 10296

Unsat Core Track

In total there are 49 divisions in the Unsat Core Track.
You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.

Division Number of Included Benchmarks
ABV 2
AUFBVDTLIA 20
AUFDTLIRA 4330
AUFDTNIRA 50
AUFFPDTLIRA 132
AUFLIA 996
AUFLIRA 7908
AUFNIA 3
AUFNIRA 421
BV 255
BVFPLRA 1
LIA 235
NIA 2
QF_ABV 1492
QF_ABVFP 1572
QF_ALIA 30
QF_ANIAn 8
QF_AUFBV 34
QF_AUFLIA 300
QF_AUFNIAn 12
QF_AX 202
QF_BV 2119
QF_BVFP 1269
QF_BVFPLRAn 46
QF_FP 8024
QF_LIA 271
QF_LIRA 5
QF_LRA 196
QF_NIAn 1636
QF_NIRAn 2
QF_NRAn 243
QF_UF 1644
QF_UFBV 300
QF_UFFP 2
QF_UFIDL 13
QF_UFLIA 16
QF_UFLRA 101
QF_UFNIAn 164
QF_UFNRAn 11
UF 1374
UFDT 745
UFDTLIRA 3342
UFDTNIRA 300
UFFPDTLIRA 300
UFFPDTNIRA 2
UFIDL 30
UFLIA 3093
UFLRA 10
UFNIA 1276
Total 44539

Model Validation Track

In total there are 6 divisions in the Model Validation Track.
You can download the list of selected benchmarks. Some benchmarks were excluded from scoring after running the competition, because they were not well-formed. Here is the list of excluded benchmarks. Note that not all of them were selected in the first place.

Division Number of Included Benchmarks
QF_BV 5752
QF_IDLe 512
QF_LIAe 1532
QF_LIRAe 1
QF_LRAe 378
QF_RDLe 109
Total 8284

n Non-competing.
e Experimental.