SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants

Participants

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

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track Preliminary Solver ID Final Solver ID Seed System Description
Bitwuzla X X X X 36798
- 42 Bitwuzla at the SMT-COMP 2022
COLIBRI X 36854
- 7 COLIBRI: SMT solving with CP
NRA-LS X 36859(sq)
- 666 NRA-LS at the SMT Competition 2022
OSTRICH X 36797
- 74672647 The OSTRICH String Solver
OpenSMT X X X X X 36857(old)
36972
- 91648253 OpenSMT in SMT-COMP 2022
Q3B-pBDD X 36885
- 658700 Q3B-pBDD in SMT Competition 2022
Q3B X 36884
- 735340574 Q3B in SMT-COMP 2022
SMT-RAT-MCSAT 22.06 X 36804
- 5630542780 SMT-RAT 22.06
SMTS cube-and-conquer X X
SMTS portfolio X X
STP X X X 36690
- 679 STP at the SMT-COMP 2022
UltimateEliminator+MathSAT X X X 36966
- 0 UltimateEliminator at SMT-COMP 2022
Vampire X X X X X 36957
- 6284 Vampire 4.7 for SMT-COMP 22
Yices-ismt X 36803(sq)
- 19970805 Yices-ismt on SMT COMP 2022
Yices2 X X X X 33403
33404(inc)
33405(mv)
- 0 Yices 2 in SMT-COMP 2022
YicesQS X 36836
- 0 Yices-QS, an extension of Yices for quantified satisfiability
Z3++ X X 36759
- 1 Z3++ at SMT-COMP 2022
Z3str4 X 36880
- 33 Z3str4, an SMT solver for the SMT-LIB theory of strings
cvc5-cloud X X
cvc5-lfsc X 36874
- 5 cvc5 at the SMT Competition 2022
cvc5 X X X X X 36875(sq)
36870(inc)
36872(mv)
36873(pe)
36869(uc)
- 5 cvc5 at the SMT Competition 2022
smtinterpol X X X X X 36790
- 945345692 SMTInterpol
solsmt X X X 36940
- 3729 solsmt at the SMT Competition 2022
veriT+raSAT+Redlog X 33044(sq)
- 2039 veriT+raSAT+Redlog at SMT-COMP 2022
veriT X X 36867(pe)
33452(sq)
- 109 veriT at SMT-COMP 2022
Total - competing 21 8 6 8 6 5 4
Total - non-competing 0 0 0 0 0 0 0
Total 21 8 6 8 6 5 4 1055742106 (mod 230)

n Non-competing.

Divisions

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

Arith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
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
YicesQS LIA
LRA
NIA
NRA
cvc5-cloud LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
cvc5-lfsc LIA
LRA
NIA
NRA
cvc5 LIA
LRA
NIA
NRA
LIA
LRA
LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
smtinterpol LIA
LRA
NIA
NRA
LIA
LRA
LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
veriT LIA
LIA
Total - competing 6 3 4 4 2 2
Total - non-competing 0 0 0 0 0 0
Total 6 3 4 4 2 2

Bitvec

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
Bitwuzla BV
BV
Q3B-pBDD BV
Q3B BV
UltimateEliminator+MathSAT BV
BV
BV
YicesQS BV
cvc5-cloud BV
BV
cvc5-lfsc BV
cvc5 BV
BV
BV
BV
Total - competing 6 3 2 2 1 1
Total - non-competing 0 0 0 0 0 0
Total 6 3 2 2 1 1

Equality

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
UltimateEliminator+MathSAT UF
UFDT
UF
UF
UFDT
Vampire UF
UFDT
UF
UFDT
UF
UF
UFDT
UF
UFDT
Yices2 UF
UF
cvc5-cloud UF
UFDT
UF
UFDT
cvc5-lfsc UF
UFDT
cvc5 UF
UFDT
UF
UF
UFDT
UF
UFDT
smtinterpol UF
UFDT
UF
UF
UFDT
UF
UFDT
veriT UF
UF
Total - competing 6 3 5 5 2 2
Total - non-competing 0 0 0 0 0 0
Total 6 3 5 5 2 2

Equality+LinearArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
UltimateEliminator+MathSAT ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
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-cloud ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5-lfsc ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5 ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
smtinterpol ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
veriT ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
Total - competing 5 3 4 4 2 2
Total - non-competing 0 0 0 0 0 0
Total 5 3 4 4 2 2

Equality+MachineArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
Bitwuzla ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVFP
UFBV
UFBVFP
ABVFPLRA
UltimateEliminator+MathSAT ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
ABVFPLRA
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
cvc5-cloud ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
cvc5-lfsc ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
cvc5 ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
ABVFPLRA
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVDTNIRA
AUFBVFP
AUFFPDTNIRA
UFBV
UFBVFP
UFBVLIA
UFFPDTNIRA
Total - competing 3 3 2 2 1 1
Total - non-competing 0 0 0 0 0 0
Total 3 3 2 2 1 1

Equality+NonLinearArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
UltimateEliminator+MathSAT AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
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-cloud AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5-lfsc AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5 AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
smtinterpol AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
Total - competing 4 3 4 3 2 2
Total - non-competing 0 0 0 0 0 0
Total 4 3 4 3 2 2

FPArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
Bitwuzla BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
UltimateEliminator+MathSAT BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
BVFP
BVFPLRA
FP
FPLRA
cvc5-cloud BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
FP
FPLRA
cvc5-lfsc BVFP
BVFPLRA
FP
FPLRA
cvc5 BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
FP
FPLRA
Total - competing 3 3 2 2 1 1
Total - non-competing 0 0 0 0 0 0
Total 3 3 2 2 1 1

QF_Bitvec

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
Bitwuzla QF_BV
QF_BV
QF_BV
QF_BV
STP QF_BV
QF_BV
QF_BV
Yices2 QF_BV
QF_BV
QF_BV
QF_BV
Z3++ QF_BV
QF_BV
cvc5-cloud QF_BV
QF_BV
cvc5-lfsc QF_BV
cvc5 QF_BV
QF_BV
QF_BV
QF_BV
QF_BV
Total - competing 5 4 3 5 2 1 1
Total - non-competing 0 0 0 0 0 0 0
Total 5 4 3 5 2 1 1

QF_Datatypes

Solver Single Query Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
cvc5-cloud QF_DT
QF_UFDT
QF_DT
QF_UFDT
cvc5-lfsc QF_DT
QF_UFDT
cvc5 QF_DT
QF_UFDT
QF_DT
QF_UFDT
QF_DT
QF_UFDT
smtinterpol QF_DT
QF_UFDT
QF_DT
QF_UFDT
QF_DT
QF_UFDT
Total - competing 2 2 3 1 1
Total - non-competing 0 0 0 0 0
Total 2 2 3 1 1

QF_Equality

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
OpenSMT QF_UF
QF_UF
QF_UF
QF_UF
QF_UF
SMTS cube-and-conquer QF_UF
QF_UF
SMTS portfolio QF_UF
QF_UF
Vampire QF_UF
Yices2 QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
QF_UF
cvc5-cloud QF_AX
QF_UF
QF_AX
QF_UF
cvc5-lfsc QF_AX
QF_UF
cvc5 QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
smtinterpol QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
veriT QF_UF
QF_UF
Total - competing 5 4 3 4 6 4 3
Total - non-competing 0 0 0 0 0 0 0
Total 5 4 3 4 6 4 3

QF_Equality+Bitvec

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition 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
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBV
cvc5-cloud QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
cvc5-lfsc QF_ABV
QF_AUFBV
QF_UFBV
cvc5 QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
Total - competing 3 3 3 3 2 1 1
Total - non-competing 0 0 0 0 0 0 0
Total 3 3 3 3 2 1 1

QF_Equality+Bitvec+Arith

Solver Incremental Track
cvc5 QF_AUFBVLIA
QF_AUFBVNIA
QF_UFBVLIA
Total - competing 1
Total - non-competing 0
Total 1

QF_Equality+LinearArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
OpenSMT QF_UFLIA
QF_UFLRA
QF_UFLIA
QF_UFLRA
QF_UFLIA
QF_UFLRA
QF_UFLIA
QF_UFLRA
SMTS cube-and-conquer QF_UFLIA
QF_UFLRA
QF_UFLIA
QF_UFLRA
SMTS portfolio QF_UFLIA
QF_UFLRA
QF_UFLIA
QF_UFLRA
Yices2 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-cloud QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-lfsc 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
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
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
QF_ALIA
QF_AUFLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
veriT QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFIDL
QF_UFLIA
QF_UFLRA
Total - competing 5 4 3 4 4 4 3
Total - non-competing 0 0 0 0 0 0 0
Total 5 4 3 4 4 4 3

QF_Equality+NonLinearArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
Yices2 QF_UFNIA
QF_UFNRA
QF_UFNIA
QF_UFNIA
QF_UFNRA
cvc5-cloud QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
cvc5-lfsc QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
cvc5 QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
smtinterpol QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFNIA
QF_UFNRA
veriT+raSAT+Redlog QF_UFNRA
Total - competing 4 3 3 3 1 1
Total - non-competing 0 0 0 0 0 0
Total 4 3 3 3 1 1

QF_FPArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition 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_ABVFPLRA
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
QF_FP
QF_FPLRA
QF_UFFP
COLIBRI QF_ABVFP
QF_ABVFPLRA
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
cvc5-cloud QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTNIRA
QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTNIRA
cvc5-lfsc QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTNIRA
cvc5 QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTNIRA
QF_ABVFP
QF_ABVFPLRA
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
QF_UFFPDTNIRA
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
QF_UFFPDTNIRA
Total - competing 3 2 2 2 2 1 1
Total - non-competing 0 0 0 0 0 0 0
Total 3 2 2 2 2 1 1

QF_LinearIntArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
OpenSMT QF_IDL
QF_LIA
QF_LIA
QF_IDL
QF_LIA
QF_LIA
QF_IDL
QF_LIA
SMTS cube-and-conquer QF_IDL
QF_LIA
QF_IDL
QF_LIA
SMTS portfolio QF_IDL
QF_LIA
QF_IDL
QF_LIA
Yices2 QF_IDL
QF_LIA
QF_LIRA
QF_LIA
QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
Z3++ QF_IDL
QF_LIA
QF_IDL
QF_LIA
cvc5-cloud QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
cvc5-lfsc QF_IDL
QF_LIA
QF_LIRA
cvc5 QF_IDL
QF_LIA
QF_LIRA
QF_LIA
QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
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
QF_IDL
QF_LIA
QF_LIRA
veriT QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
Total - competing 6 4 3 5 5 4 3
Total - non-competing 0 0 0 0 0 0 0
Total 6 4 3 5 5 4 3

QF_LinearRealArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
OpenSMT QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
SMTS cube-and-conquer QF_LRA
QF_RDL
QF_LRA
QF_RDL
SMTS portfolio QF_LRA
QF_RDL
QF_LRA
QF_RDL
Yices2 QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_RDL
cvc5-cloud QF_LRA
QF_RDL
QF_LRA
QF_RDL
cvc5-lfsc QF_LRA
QF_RDL
cvc5 QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_RDL
QF_LRA
QF_RDL
smtinterpol QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_RDL
QF_LRA
QF_RDL
solsmt QF_LRA
QF_RDL
QF_LRA
QF_RDL
QF_LRA
QF_RDL
veriT QF_LRA
QF_RDL
QF_LRA
QF_RDL
Total - competing 6 5 3 5 5 4 3
Total - non-competing 0 0 0 0 0 0 0
Total 6 5 3 5 5 4 3

QF_NonLinearIntArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
Yices-ismt QF_NIA
Yices2 QF_NIA
QF_NIRA
QF_NIA
QF_NIA
QF_NIRA
Z3++ QF_NIA
cvc5-cloud QF_NIA
QF_NIRA
QF_NIA
QF_NIRA
cvc5-lfsc QF_NIA
QF_NIRA
cvc5 QF_NIA
QF_NIRA
QF_NIA
QF_NIA
QF_NIRA
QF_NIA
QF_NIRA
smtinterpol QF_NIA
QF_NIRA
QF_NIA
QF_NIA
QF_NIRA
QF_NIA
QF_NIRA
Total - competing 5 3 3 3 1 1
Total - non-competing 0 0 0 0 0 0
Total 5 3 3 3 1 1

QF_NonLinearRealArith

Solver Single Query Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
NRA-LS QF_NRA
SMT-RAT-MCSAT 22.06 QF_NRA
Yices2 QF_NRA
QF_NRA
Z3++ QF_NRA
cvc5-cloud QF_NRA
QF_NRA
cvc5-lfsc QF_NRA
cvc5 QF_NRA
QF_NRA
QF_NRA
smtinterpol QF_NRA
QF_NRA
QF_NRA
veriT+raSAT+Redlog QF_NRA
Total - competing 7 3 3 1 1
Total - non-competing 0 0 0 0 0
Total 7 3 3 1 1

QF_Strings

Solver Single Query Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
OSTRICH QF_S
QF_SLIA
QF_SNIA
Z3str4 QF_S
QF_SLIA
cvc5-cloud QF_S
QF_SLIA
QF_SNIA
QF_S
QF_SLIA
QF_SNIA
cvc5-lfsc QF_S
QF_SLIA
QF_SNIA
cvc5 QF_S
QF_SLIA
QF_SNIA
QF_S
QF_SLIA
QF_SNIA
QF_S
QF_SLIA
QF_SNIA
Total - competing 3 1 2 1 1
Total - non-competing 0 0 0 0 0
Total 3 1 2 1 1