SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

Benchmarks

SMT-COMP 2019 will use a large subset of the benchmarks available within the 2019-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/2019-05-06 on StarExec.

Single Query Track

In total there are 55 divisions in the Single Query Track.
The list of selected benchmarks is available here.

Division Number of Included Benchmarks
ABVFP 1
ALIA 19
AUFBVDTLIAn 854
AUFDTLIA 275
AUFLIA 1638
AUFLIRA 1683
AUFNIA 3
AUFNIRA 300
BV 823
BVFP 24
FP 1238
LIA 300
LRA 1003
NIA 11
NRA 93
QF_ABV 7538
QF_ABVFPn 630
QF_ALIA 139
QF_ANIA 7
QF_AUFBV 41
QF_AUFLIA 651
QF_AUFNIA 9
QF_AX 300
QF_BV 8909
QF_BVFP 516
QF_BVFPLRAn 1
QF_DT 4
QF_FP 250
QF_FPLRAn 13
QF_IDL 1042
QF_LIA 3136
QF_LIRA 7
QF_LRA 546
QF_NIA 11494
QF_NIRA 2
QF_NRA 2842
QF_RDL 247
QF_Se 988
QF_SLIAe 23175
QF_UF 3512
QF_UFBV 223
QF_UFIDL 300
QF_UFLIA 300
QF_UFLRA 541
QF_UFNIA 300
QF_UFNRA 26
UF 2816
UFBV 72
UFDT 1547
UFDTLIA 299
UFDTNIA 1
UFIDL 20
UFLIA 2848
UFLRA 7
UFNIA 6253
Total 89817

Incremental Track

In total there are 29 divisions in the Incremental Track.
The list of selected benchmarks is available here.

Division Number of Included Benchmarks
ABVFP 4
ALIA 24
ANIA 3
AUFNIRA 165
BV 18
BVFP 10
LIA 6
LRA 5
QF_ABV 631
QF_ABVFPn 69
QF_ALIA 44
QF_ANIA 5
QF_AUFBV 25
QF_AUFBVLIAn 300
QF_AUFBVNIA 44
QF_AUFLIA 72
QF_BV 1291
QF_BVFPn 182
QF_FPn 2
QF_LIA 69
QF_LRA 10
QF_NIA 10
QF_UF 383
QF_UFBV 1165
QF_UFBVLIAn 179
QF_UFLIA 386
QF_UFLRA 1529
QF_UFNIA 1
UFLRA 935
Total 7567

Challenge Track (non-incremental)

In total there are 3 divisions in the Challenge Track (non-incremental).
The list of selected benchmarks is available here.

Division Number of Included Benchmarks
QF_ABV 7
QF_AUFBV 15
QF_BV 7
Total 29

Challenge Track (incremental)

In total there are 3 divisions in the Challenge Track (incremental).
The list of selected benchmarks is available here.

Division Number of Included Benchmarks
QF_ABV 9
QF_AUFBV 6
QF_BV 7
Total 22

Unsat Core Track

In total there are 38 divisions in the Unsat Core Track.
The list of selected benchmarks is available here.

Division Number of Included Benchmarks
AUFBVDTLIAn 20
AUFLIA 1245
AUFLIRA 9885
AUFNIA 3
AUFNIRA 526
BV 233
LIA 200
NIA 2
QF_ABV 1865
QF_ABVFPn 1965
QF_ALIA 38
QF_ANIA 8
QF_AUFBV 34
QF_AUFLIA 300
QF_AUFNIA 12
QF_AX 202
QF_BV 2641
QF_BVFPn 1586
QF_FPn 10031
QF_LIA 271
QF_LIRA 5
QF_LRA 196
QF_NIA 2045
QF_NIRA 2
QF_NRA 243
QF_UF 2055
QF_UFBV 300
QF_UFIDL 13
QF_UFLIA 16
QF_UFLRA 101
QF_UFNIA 164
QF_UFNRA 11
UF 1705
UFDTn 931
UFIDL 30
UFLIA 3867
UFLRA 10
UFNIA 1580
Total 44341

Model Validation Track (experimental)

In total there are 1 divisions in the Model Validation Track (experimental).
The list of selected benchmarks is available here.

Division Number of Included Benchmarks
QF_BV 7191
Total 7191

n Non-competing.
e Experimental.