SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

Rules
Benchmarks
Specs
Model Validation Track
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

QF_Equality+LinearArith

Tracks

Track Number of Benchmarks StatusLogics Benchmarks
Single Query Track 1922 competitiveQF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
166
530
76
9
300
300
541
Incremental Track 2031 competitiveQF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
44
72
386
1529
Unsat Core Track 598 competitiveQF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
30
300
11
17
113
26
101
Model Validation Track 921 competitiveQF_UFIDL
QF_UFLIA
QF_UFLRA
206
330
385
Proof Exhibition Track 799 competitiveQF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
72
190
11
66
150
160
150
Cloud Track 0 competitive
Parallel Track 0 competitive