SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

Participants

The following solvers have been submitted to SMT-COMP 2021 or were entered as non-competing solvers by the organizers for comparison.

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track Preliminary Solver ID Final Solver ID Seed System Description
AProVE X 1229 1229 170142 AProVE at SMT-COMP 2021
Bitwuzla X X X X 33006 33292 42 Bitwuzla at the SMT-COMP 2021
COLIBRI X 32990 32990 9075420 COLIBRI
OpenSMT X X X 33003 33438 13390 The OpenSMT Solver in SMT-COMP 2021
SMT-RAT-MCSAT X 33080 33080 5650572280 SMT-RAT 21.05
SMT-RAT X 33081 33081 9077370145 SMT-RAT 21.05
SMTInterpol-remus X 33041 33435 1 SMTInterpol and SMTInterpol-remus
SMTInterpol X X X X 32995 33439 384076683 SMTInterpol and SMTInterpol-remus
SMTS cube-and-conquer X -1 10 0 The OpenSMT Solver in SMT-COMP 2021
SMTS portfolio X -1 13 0 The OpenSMT Solver in SMT-COMP 2021
STP-CMS-Cloud X -1 14 0 STP in the SMT-COMP 2021
STP-parallel X -1 15 0 STP in the SMT-COMP 2021
STP X X X 28776 33442 2021 STP in the SMT-COMP 2021
UltimateEliminator+MathSAT X X X 28804 33466 0 UltimateEliminator at SMT-COMP 2021
Vampire X X X X 33206 33458 5676 Vampire (4.6-smt)
Yices2-QS X 33316 33422 278 Yices-QS, an extension of Yices for quantified satisfaction
Yices2 X X 33007 33403 43874423 Yices 2 at SMTCOMP2021
Yices2 incremental X 33009 33404 89347412 Yices 2 at SMTCOMP2021
Yices2 model-validation X 33008 33405 13863812 Yices 2 at SMTCOMP2021
YicesLS X X 33317 33369 1 LS-IDL: Local Search For SMT on Integer Difference Logic
Z3str4 X 33313 33313 458751 Z3str4 String Solver: System Description
cvc5-gg X X -1 11 0 cvc5-gg at the SMT Competition 2021
cvc5-inc X 33070 33449 5 cvc5 at the SMT Competition 2021
cvc5-mv X 33069 33447 5 cvc5 at the SMT Competition 2021
cvc5-uc X 33074 33448 5 cvc5 at the SMT Competition 2021
cvc5 X 33075 33446 5 cvc5 at the SMT Competition 2021
iProver X 33293 33459 12281 iProver-v3.5 (SMT-COMP 2021)
mc2 X 33279 33279 750 MC2
veriT+raSAT+Redlog X 33044 33044 54000 veriT+raSAT+Redlog at SMT-COMP 2021
veriT X 33043 33452 6923 veriT at SMT-COMP 2021
2018-CVC4n X 19775 CVC4 at the SMT Competition 2018
2018-MathSAT (incremental)n X 19993
2018-Yicesn X 19791
2018-Yices (incremental)n X 19995
2018-Z3n X 19792
2018-Z3 (incremental)n X 19996
2019-CVC4-incn X 23417 23733 CVC4 at the SMT Competition 2019
2019-CVC4n X 23420 23737 CVC4 at the SMT Competition 2019
2019-MathSAT-defaultn X 23373 23680 MathSAT5 (Nonlinear) at the SMT Competition 2019
2019-Par4n X 23391 23672 Par4
2019-SMTInterpoln X 23360 23554 SMTInterpol
2019-Yices 2.6.2n X 23363 23694 Yices 2 in SMT-COMP 2019
2019-Yices 2.6.2 Incrementaln X 23364 23695 Yices 2 in SMT-COMP 2019
2019-Z3n X X 23470 23470
2020-Bitwuzla-fixedn X X X 29091 29091 Bitwuzla at the SMT Competition 2020
2020-Bitwuzlan X X X 28351 28818 Bitwuzla at the SMT Competition 2020
2020-COLIBRIn X 28309 28737 COLIBRI
2020-CVC4-incn X 28466 28799 CVC4 at the SMT Competition 2020
2020-CVC4-ucn X 28357 28800 CVC4 at the SMT Competition 2020
2020-CVC4n X 28354 28798 CVC4 at the SMT Competition 2020
2020-MathSAT5n X X 28851 28851
2020-OpenSMTn X X 28564 28738 OpenSMT in SMT-COMP 2020
2020-SMT-RATn X 28075 28075 SMT-RAT 20.04
2020-SMTInterpol-fixedn X 29030 29030 SMTInterpol
2020-Vampiren X 28324 28782 Vampire 4.5-SMT System Description
2020-Yices2-fixedn X X 29032 29032 Yices 2 in SMT-COMP 2020
2020-Yices2-fixed Model Validationn X 29033 29033 Yices 2 in SMT-COMP 2020
2020-Yices2-fixed incrementaln X 29034 29034 Yices 2 in SMT-COMP 2020
2020-Yices2n X X 28343 28820 Yices 2 in SMT-COMP 2020
2020-Yices2 Model Validationn X 28464 28819 Yices 2 in SMT-COMP 2020
2020-Yices2 incrementaln X 28344 28821 Yices 2 in SMT-COMP 2020
2020-z3n X X X X 28814 28814
Bitwuzla - fixedn X 33809 0
COLIBRI - fixedn X 33704 0
MathSAT5n X X X X 33739 0
OpenSMT - fixedn X 33687 0
Par4n X X -1 12 0 Par4 System Description
Vampire - fixedn X 33720 0
Z3str4 - fixedn X 33727 0
cvc5-inc - fixedn X 33964 0
cvc5-mv - fixedn X 33966 0
cvc5-uc - fixedn X 33965 0
cvc5 - fixedn X 33963 0
iProver - fixedn X 33670 0
iProver - fixed2n X 33931 0
z3-mvn X 33758 0
z3n X X X 33741 0
Total - competing 19 7 7 7 5 3
Total - non-competing 29 16 10 8 1 1
Total 48 23 17 15 6 4 236518915 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2021-06-15 was 16662.4235, resulting in a competition seed of 236518915 + 1666242 = 238185157.

Divisions

These are the logic divisions in which each solver is participating.

Arith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
SMTInterpol-remus LIA
LRA
SMTInterpol LIA
LRA
LIA
LRA
LIA
LRA
UltimateEliminator+MathSAT LIA
LRA
NIA
NRA
LIA
LRA
LIA
LRA
NIA
NRA
Vampire LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
Yices2-QS NRA
cvc5-gg LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
cvc5-inc LIA
LRA
cvc5-uc LIA
LRA
NIA
NRA
cvc5 LIA
LRA
NIA
NRA
iProver LIA
LRA
NIA
NRA
veriT LIA
2018-Z3n NIA
2019-Par4n LRA
NRA
2020-CVC4-incn LIA
LRA
2020-CVC4-ucn LIA
LRA
NIA
NRA
2020-CVC4n LIA
LRA
NIA
NRA
2020-z3n LIA
LRA
NIA
NRA
LIA
LRA
Par4n LRA
NRA
LRA
NRA
Vampire - fixedn LIA
LRA
NIA
NRA
cvc5-inc - fixedn LIA
LRA
cvc5-uc - fixedn LIA
LRA
NIA
NRA
cvc5 - fixedn LIA
LRA
NIA
NRA
z3n LIA
LRA
NIA
NRA
LIA
LRA
LIA
LRA
NIA
NRA
Total - competing 7 3 5 2 2
Total - non-competing 7 4 3 1 1
Total 14 7 8 3 3

Bitvec

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
UltimateEliminator+MathSAT BV
BV
BV
Yices2-QS BV
cvc5-gg BV
BV
cvc5-inc BV
cvc5-uc BV
cvc5 BV
2019-Par4n BV
2019-Z3n BV
2020-CVC4-ucn BV
Par4n BV
BV
z3n BV
BV
BV
Total - competing 3 2 2 1 1
Total - non-competing 2 2 2 1 1
Total 5 4 4 2 2

Equality

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
SMTInterpol-remus UF
SMTInterpol UF
UF
UF
UltimateEliminator+MathSAT UF
UF
UF
Vampire UF
UFDT
UF
UFDT
UF
UFDT
UF
UFDT
Yices2 UF
cvc5-gg UF
UFDT
UF
UFDT
cvc5-inc UF
cvc5-uc UF
UFDT
cvc5 UF
UFDT
iProver UF
UFDT
veriT UF
2020-CVC4-ucn UF
UFDT
2020-CVC4n UF
UFDT
2020-Vampiren UF
UFDT
2020-z3n UF
Par4n UF
UF
Vampire - fixedn UF
UFDT
iProver - fixedn UF
UFDT
iProver - fixed2n UF
UFDT
z3n UF
UF
UF
Total - competing 7 3 5 2 2
Total - non-competing 6 2 2 1 1
Total 13 5 7 3 3

Equality+LinearArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
SMTInterpol-remus ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
SMTInterpol ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
UltimateEliminator+MathSAT ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
Vampire ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5-gg ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5-inc ALIA
UFLRA
cvc5-uc ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5 ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
iProver UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
veriT ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
2018-CVC4n AUFDTLIA
AUFLIA
2018-Z3n ALIA
UFLRA
2019-CVC4n UFDTLIA
2019-Par4n AUFLIRA
UFIDL
UFLIA
2019-Z3n UFLRA
2020-CVC4-ucn ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
2020-CVC4n ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
2020-Vampiren ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
2020-z3n ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
Par4n AUFLIRA
UFIDL
UFLIA
AUFLIRA
UFIDL
UFLIA
Vampire - fixedn ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5-inc - fixedn ALIA
UFLRA
cvc5-uc - fixedn ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5 - fixedn ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
z3n ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
Total - competing 6 3 5 2 2
Total - non-competing 10 4 4 1 1
Total 16 7 9 3 3

Equality+MachineArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
UltimateEliminator+MathSAT ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVFP
UFBV
UFBVFP
UFBVLIA
ABVFP
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVFP
UFBV
UFBVFP
UFBVLIA
cvc5-gg ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
AUFFPDTLIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
AUFFPDTLIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
cvc5-inc ABVFP
cvc5-uc ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
AUFFPDTLIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
cvc5 ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
AUFFPDTLIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
2018-Z3n UFBV
2020-CVC4-ucn ABV
ABVFP
ABVFPLRA
AUFBVDTLIA
AUFFPDTLIRA
UFBV
UFFPDTLIRA
UFFPDTNIRA
2020-CVC4n ABV
ABVFP
ABVFPLRA
AUFBVDTLIA
AUFFPDTLIRA
UFBV
UFFPDTLIRA
UFFPDTNIRA
2020-z3n ABV
UFBV
Par4n UFBV
UFBV
cvc5-uc - fixedn ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
AUFFPDTLIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
cvc5 - fixedn ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
AUFFPDTLIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
z3n ABV
AUFBV
UFBV
ABV
AUFBV
UFBV
Total - competing 2 2 2 1 1
Total - non-competing 5 0 3 1 1
Total 7 2 5 2 2

Equality+NonLinearArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
SMTInterpol UFNIA
ANIA
AUFNIRA
UFNIA
UFNRA
UFNIA
UltimateEliminator+MathSAT AUFNIA
AUFNIRA
UFNIA
ANIA
AUFNIRA
UFNIA
UFNRA
AUFNIA
AUFNIRA
UFNIA
Vampire AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5-gg AUFDTNIRA
AUFFPDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFFPDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5-inc ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
cvc5-uc AUFDTNIRA
AUFFPDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5 AUFDTNIRA
AUFFPDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
iProver UFDTNIA
UFDTNIRA
UFNIA
2019-CVC4-incn AUFNIRA
2019-Par4n AUFNIRA
UFNIA
2020-CVC4-incn ANIA
AUFNIRA
UFNIA
UFNRA
2020-CVC4-ucn AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
2020-CVC4n AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
2020-Vampiren AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
2020-z3n AUFNIRA
UFNIA
UFNRA
Par4n AUFNIRA
UFNIA
AUFNIRA
UFNIA
Vampire - fixedn AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5-inc - fixedn ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
cvc5-uc - fixedn AUFDTNIRA
AUFFPDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5 - fixedn AUFDTNIRA
AUFFPDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
z3n AUFNIA
AUFNIRA
UFNIA
AUFNIRA
UFNIA
UFNRA
AUFNIA
AUFNIRA
UFNIA
Total - competing 5 3 4 2 2
Total - non-competing 6 5 3 1 1
Total 11 8 7 3 3

FPArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
UltimateEliminator+MathSAT BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFP
BVFPLRA
FP
FPLRA
cvc5-gg BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
FP
FPLRA
cvc5-inc BVFP
cvc5-uc BVFP
BVFPLRA
FP
FPLRA
cvc5 BVFP
BVFPLRA
FP
FPLRA
2019-CVC4-incn BVFP
2019-Z3n BVFP
FP
2020-CVC4-ucn BVFP
BVFPLRA
FP
FPLRA
2020-CVC4n BVFP
BVFPLRA
FP
FPLRA
z3n FP
FP
Total - competing 2 2 2 1 1
Total - non-competing 3 1 2 0 0
Total 5 3 4 1 1

QF_Bitvec

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track
Bitwuzla QF_BV
QF_BV
QF_BV
QF_BV
STP-CMS-Cloud QF_BV
STP-parallel QF_BV
STP QF_BV
QF_BV
QF_BV
Yices2 QF_BV
QF_BV
Yices2 incremental QF_BV
Yices2 model-validation QF_BV
cvc5-gg QF_BV
QF_BV
cvc5-inc QF_BV
cvc5-mv QF_BV
cvc5-uc QF_BV
cvc5 QF_BV
2020-Bitwuzla-fixedn QF_BV
QF_BV
2020-Bitwuzlan QF_BV
2020-Yices2-fixed incrementaln QF_BV
MathSAT5n QF_BV
QF_BV
QF_BV
QF_BV
Par4n QF_BV
QF_BV
z3-mvn QF_BV
z3n QF_BV
QF_BV
QF_BV
Total - competing 4 4 3 4 2 2
Total - non-competing 3 3 3 3 1 1
Total 7 7 6 7 3 3

QF_Equality

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track
OpenSMT QF_UF
QF_UF
QF_UF
SMTInterpol-remus QF_AX
QF_DT
QF_UF
QF_UFDT
SMTInterpol QF_AX
QF_DT
QF_UF
QF_UFDT
QF_UF
QF_AX
QF_DT
QF_UF
QF_UFDT
QF_UF
SMTS cube-and-conquer QF_UF
SMTS portfolio QF_UF
Yices2 QF_AX
QF_UF
QF_AX
QF_UF
Yices2 incremental QF_UF
Yices2 model-validation QF_UF
cvc5-gg QF_AX
QF_DT
QF_UF
QF_UFDT
QF_AX
QF_DT
QF_UF
QF_UFDT
cvc5-inc QF_UF
cvc5-mv QF_UF
cvc5-uc QF_AX
QF_DT
QF_UF
QF_UFDT
cvc5 QF_AX
QF_DT
QF_UF
QF_UFDT
veriT QF_UF
2019-Par4n QF_UF
2019-Yices 2.6.2 Incrementaln QF_UF
2020-SMTInterpol-fixedn QF_AX
QF_UF
2020-Yices2-fixedn QF_AX
QF_UF
QF_AX
QF_UF
2020-Yices2n QF_AX
QF_UF
2020-z3n QF_AX
QF_DT
QF_UF
MathSAT5n QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
QF_UF
Par4n QF_UF
QF_UF
z3-mvn QF_UF
z3n QF_AX
QF_DT
QF_UF
QF_UFDT
QF_UF
QF_AX
QF_DT
QF_UF
QF_UFDT
Total - competing 5 4 4 4 3 1
Total - non-competing 6 3 4 2 1 1
Total 11 7 8 6 4 2

QF_Equality+Bitvec

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track
Bitwuzla QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBV
Yices2 QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
Yices2 incremental QF_ABV
QF_AUFBV
QF_UFBV
Yices2 model-validation QF_UFBV
cvc5-gg QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
cvc5-inc QF_ABV
QF_AUFBV
QF_UFBV
cvc5-mv QF_UFBV
cvc5-uc QF_ABV
QF_AUFBV
QF_UFBV
cvc5 QF_ABV
QF_AUFBV
QF_UFBV
2020-Bitwuzla-fixedn QF_ABV
QF_AUFBV
QF_UFBV
2020-Bitwuzlan QF_ABV
QF_AUFBV
QF_UFBV
2020-Yices2-fixedn QF_ABV
QF_AUFBV
QF_UFBV
2020-Yices2n QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
2020-Yices2 incrementaln QF_ABV
QF_AUFBV
QF_UFBV
2020-z3n QF_ABV
QF_AUFBV
QF_UFBV
MathSAT5n QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBV
Par4n QF_ABV
QF_ABV
z3-mvn QF_UFBV
z3n QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
Total - competing 3 3 3 3 1 1
Total - non-competing 5 4 4 2 1 1
Total 8 7 7 5 2 2

QF_Equality+Bitvec+Arith

Solver Incremental Track
cvc5-inc QF_AUFBVLIA
QF_AUFBVNIA
QF_UFBVLIA
MathSAT5n QF_AUFBVLIA
QF_AUFBVNIA
QF_UFBVLIA
cvc5-inc - fixedn QF_AUFBVLIA
QF_AUFBVNIA
QF_UFBVLIA
Total - competing 1
Total - non-competing 2
Total 3

QF_Equality+LinearArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track
SMTInterpol-remus QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
SMTInterpol QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
Yices2 QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
Yices2 incremental QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
Yices2 model-validation QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-gg QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-inc QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
cvc5-mv QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-uc QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5 QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
mc2 QF_UFLRA
veriT QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
2018-Yicesn QF_UFLIA
2018-Yices (incremental)n QF_AUFLIA
2018-Z3 (incremental)n QF_ALIA
QF_UFLIA
2019-SMTInterpoln QF_UFLRA
2019-Yices 2.6.2n QF_ALIA
QF_AUFLIA
QF_UFIDL
2020-CVC4-ucn QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
2020-Yices2-fixedn QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
2020-z3n QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
MathSAT5n QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-inc - fixedn QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
cvc5-mv - fixedn QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-uc - fixedn QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5 - fixedn QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
z3-mvn QF_UFIDL
QF_UFLIA
QF_UFLRA
z3n QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
Total - competing 5 3 4 3 1 1
Total - non-competing 6 6 6 3 0 0
Total 11 9 10 6 1 1

QF_Equality+NonLinearArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
SMTInterpol QF_ANIA
QF_UFNIA
QF_UFNRA
Yices2 QF_UFNIA
QF_UFNRA
QF_UFNIA
QF_UFNRA
Yices2 incremental QF_UFNIA
cvc5-gg QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
cvc5-inc QF_ANIA
QF_UFNIA
QF_UFNRA
cvc5-uc QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
cvc5 QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
veriT+raSAT+Redlog QF_UFNRA
2019-CVC4n QF_ANIA
QF_UFNIA
2019-MathSAT-defaultn QF_AUFNIA
2019-Par4n QF_UFNRA
2020-CVC4n QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
2020-MathSAT5n QF_ANIA
QF_UFNIA
MathSAT5n QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
Par4n QF_UFNRA
QF_UFNRA
cvc5-inc - fixedn QF_ANIA
QF_UFNIA
QF_UFNRA
cvc5-uc - fixedn QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
cvc5 - fixedn QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
z3n QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
Total - competing 3 3 2 1 1
Total - non-competing 7 4 3 1 1
Total 10 7 5 2 2

QF_FPArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
Bitwuzla QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
COLIBRI QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
cvc5-gg QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
cvc5-inc QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
cvc5-uc QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTLIRA
cvc5 QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTLIRA
2020-Bitwuzla-fixedn QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
2020-Bitwuzlan QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
2020-COLIBRIn QF_ABVFP
QF_ABVFPLRA
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
2020-CVC4-incn QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
2020-CVC4n QF_ABVFP
QF_ABVFPLRA
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
2020-MathSAT5n QF_ABVFP
QF_ABVFPLRA
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
Bitwuzla - fixedn QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
COLIBRI - fixedn QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
MathSAT5n QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_ABVFP
QF_BVFP
QF_FP
QF_UFFP
QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
Par4n QF_BVFP
QF_FP
QF_BVFP
QF_FP
cvc5-uc - fixedn QF_UFFPDTLIRA
cvc5 - fixedn QF_UFFPDTLIRA
z3n QF_BVFP
QF_FP
QF_FPLRA
QF_BVFP
QF_FP
QF_BVFP
QF_FP
QF_FPLRA
Total - competing 3 2 2 1 1
Total - non-competing 9 5 5 1 1
Total 12 7 7 2 2

QF_LinearIntArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track
OpenSMT QF_IDL
QF_LIA
QF_LIA
QF_IDL
QF_LIA
SMTInterpol-remus QF_IDL
QF_LIA
QF_LIRA
SMTInterpol QF_IDL
QF_LIA
QF_LIRA
QF_LIA
QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
SMTS cube-and-conquer QF_IDL
QF_LIA
SMTS portfolio QF_IDL
QF_LIA
Yices2 QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
Yices2 incremental QF_LIA
Yices2 model-validation QF_IDL
QF_LIA
QF_LIRA
YicesLS QF_IDL
QF_IDL
cvc5-gg QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
cvc5-inc QF_LIA
cvc5-mv QF_IDL
QF_LIA
QF_LIRA
cvc5-uc QF_IDL
QF_LIA
QF_LIRA
cvc5 QF_IDL
QF_LIA
QF_LIRA
veriT QF_IDL
QF_LIA
QF_LIRA
2019-Par4n QF_IDL
QF_LIA
QF_LIRA
2020-Yices2-fixedn QF_IDL
QF_LIA
QF_LIRA
2020-Yices2-fixed Model Validationn QF_IDL
QF_LIA
QF_LIRA
2020-Yices2-fixed incrementaln QF_LIA
2020-Yices2 Model Validationn QF_IDL
QF_LIA
QF_LIRA
2020-z3n QF_IDL
QF_LIA
QF_LIRA
MathSAT5n QF_IDL
QF_LIA
QF_LIRA
QF_LIA
QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
OpenSMT - fixedn QF_IDL
QF_LIA
Par4n QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
cvc5-inc - fixedn QF_LIA
cvc5-mv - fixedn QF_IDL
QF_LIA
QF_LIRA
cvc5-uc - fixedn QF_IDL
QF_LIA
QF_LIRA
cvc5 - fixedn QF_IDL
QF_LIA
QF_LIRA
z3-mvn QF_IDL
QF_LIA
QF_LIRA
z3n QF_IDL
QF_LIA
QF_LIRA
QF_LIA
QF_IDL
QF_LIA
QF_LIRA
Total - competing 6 4 4 5 3 1
Total - non-competing 5 4 4 6 1 1
Total 11 8 8 11 4 2

QF_LinearRealArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Cloud Track Parallel Track
OpenSMT QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
SMTInterpol-remus QF_LRA
QF_RDL
SMTInterpol QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_RDL
SMTS cube-and-conquer QF_LRA
QF_RDL
SMTS portfolio QF_LRA
QF_RDL
Yices2 QF_LRA
QF_RDL
QF_LRA
QF_RDL
Yices2 incremental QF_LRA
Yices2 model-validation QF_LRA
QF_RDL
cvc5-gg QF_LRA
QF_RDL
QF_LRA
QF_RDL
cvc5-inc QF_LRA
cvc5-mv QF_LRA
QF_RDL
cvc5-uc QF_LRA
QF_RDL
cvc5 QF_LRA
QF_RDL
mc2 QF_LRA
veriT QF_LRA
QF_RDL
2018-MathSAT (incremental)n QF_LRA
2019-Par4n QF_LRA
2019-Yices 2.6.2n QF_RDL
2020-OpenSMTn QF_LRA
QF_LRA
2020-Yices2-fixed Model Validationn QF_LRA
QF_RDL
2020-Yices2n QF_LRA
QF_RDL
MathSAT5n QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_RDL
Par4n QF_LRA
QF_LRA
z3-mvn QF_LRA
QF_RDL
z3n QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
Total - competing 6 4 4 4 3 1
Total - non-competing 5 3 3 4 1 1
Total 11 7 7 8 4 2

QF_NonLinearIntArith

Solver Single Query Track Incremental Track Unsat Core Track Cloud Track Parallel Track
AProVE QF_NIA
SMT-RAT QF_NIA
QF_NIRA
SMTInterpol QF_NIA
Yices2 QF_NIA
QF_NIRA
QF_NIA
QF_NIRA
Yices2 incremental QF_NIA
cvc5-gg QF_NIA
QF_NIRA
QF_NIA
QF_NIRA
cvc5-inc QF_NIA
cvc5-uc QF_NIA
QF_NIRA
cvc5 QF_NIA
QF_NIRA
2019-Par4n QF_NIA
2020-MathSAT5n QF_NIA
2020-SMT-RATn QF_NIA
QF_NIRA
MathSAT5n QF_NIA
QF_NIRA
QF_NIA
QF_NIA
QF_NIRA
Par4n QF_NIA
QF_NIA
cvc5-inc - fixedn QF_NIA
cvc5-uc - fixedn QF_NIA
QF_NIRA
cvc5 - fixedn QF_NIA
QF_NIRA
z3n QF_NIA
QF_NIRA
QF_NIA
QF_NIA
QF_NIRA
Total - competing 4 3 2 1 1
Total - non-competing 5 4 3 1 1
Total 9 7 5 2 2

QF_NonLinearRealArith

Solver Single Query Track Unsat Core Track Cloud Track Parallel Track
SMT-RAT-MCSAT QF_NRA
Yices2 QF_NRA
QF_NRA
cvc5-gg QF_NRA
QF_NRA
cvc5-uc QF_NRA
cvc5 QF_NRA
veriT+raSAT+Redlog QF_NRA
2019-Par4n QF_NRA
MathSAT5n QF_NRA
QF_NRA
Par4n QF_NRA
QF_NRA
z3n QF_NRA
QF_NRA
Total - competing 4 2 1 1
Total - non-competing 3 2 1 1
Total 7 4 2 2

QF_Strings

Solver Single Query Track Unsat Core Track Cloud Track Parallel Track
Z3str4 QF_S
QF_SLIA
QF_SNIA
cvc5-gg QF_S
QF_SLIA
QF_SNIA
QF_S
QF_SLIA
QF_SNIA
cvc5-uc QF_S
QF_SLIA
QF_SNIA
cvc5 QF_S
QF_SLIA
QF_SNIA
2020-CVC4n QF_S
QF_SLIA
Z3str4 - fixedn QF_S
QF_SLIA
QF_SNIA
cvc5-uc - fixedn QF_S
QF_SLIA
QF_SNIA
cvc5 - fixedn QF_S
QF_SLIA
QF_SNIA
z3n QF_S
QF_SLIA
Total - competing 2 1 1 1
Total - non-competing 4 1 0 0
Total 6 2 1 1