SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

Rules
Specs
Model Validation Track
Proof Exhibition Track
Parallel & Cloud Tracks
Participants

Participants

The following solvers have been submitted to SMT-COMP 2023 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 44483
44756
42 Bitwuzla at the SMT-COMP 2023
COLIBRI X 44384
44384
413 COLIBRI: SMT solving with CP
OSTRICH X 44420
44767
67223 OSTRICH Version 1.3
OpenSMT X X X 44686
44750
9471002 The OpenSMT Solver in SMT-COMP 2023
Q3B X 39062
44707
2353490582350 Q3B in SMT Competition 2023
SMT-RAT-MCSAT X X 44411
44765
48738 SMT-RAT 23.05
SMTInterpol X X X X X 44719
44759
3021856368 SMTInterpol with resolution proofs
STP X X X 41385
41385
16 STP 2023
UltimateEliminator+MathSAT X X X 44489
44761
0 Ultimate Eliminator at SMT-COMP 2023
UltimateIntBlastingWrapper+SMTInterpol X 44525
44760
4294967296 Ultimate IntBlastingWrapper
Vampire X X X X X 44484
44484
6586 Vampire 4.8-SMT System Description
Yaga X X 44678
44678
3621199 The Yaga SMT Solver in SMT-COMP 2023
Yices2 X X X X 44479
44480(inc)
44481(mv)
44479
44751(inc)
44755(mv)
0 Yices 2 in SMT-COMP 2023
YicesQS X 39111
39111
0 YicesQS 2023, an extension of Yices for quantified satisfiability
Z3++ X X 44702(sq)
44703(mv)
44702
44703(mv)
1 Z3++ at SMT-COMP 2023
Z3-Noodler X 44407
44716
6590 Z3-Noodler, System description for SMT-comp 2023
Z3-Owl X X 44471
44715
8 Z3-Owl at SMT-COMP 2023
cvc5-NRA-LS X X 44469
44741
44742(mv)
99 NRA-LS at the SMT Competition 2023
cvc5-lfsc X 44515
44736
52240 cvc5 at the SMT Competition 2023
cvc5 X X X X X 44516
44517(inc)
44737
44738(inc)
1965 cvc5 at the SMT Competition 2023
iProver X X 44524
44768
191937 iProver v3.8 (SMT-COMP-2023)
ismt X 44672
44672
20230512 ISMT for SMT-COMP 2023
yices-ismt X 44713
44713
Yices-ISMT for SMT-COMP 2023
z3-alpha X 44485
44764
33 Z3-alpha: a reinforcement learning guided SMT solver
Q3B-pBDDn 36885
- 78549 Q3B-pBDD in SMT Competition 2023
Total - competing 22 7 6 11 4 1 3
Total - non-competing 0 0 0 0 0 0 0
Total 22 7 6 11 4 1 3 756654015 (mod 230)

n Non-competing.

The opening value of the NYSE Composite Index on 2023-05-30 was 15078.69, resulting in a competition seed of 756654015 + 1507869 = 758161884.

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
SMTInterpol LIA
LRA
NIA
NRA
LIA
LRA
LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
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
LIA
LRA
NIA
NRA
YicesQS 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
iProver LIA
LRA
NIA
NRA
LIA
LRA
NIA
NRA
Total - competing 6 3 4 4 1 2
Total - non-competing 0 0 0 0 0 0
Total 6 3 4 4 1 2

Bitvec

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

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
UFDT
UF
UFDT
UF
UFDT
Yices2 UF
UFDT
UF
UF
UFDT
cvc5-lfsc UF
UFDT
cvc5 UF
UFDT
UF
UF
UFDT
UF
UFDT
iProver UF
UFDT
UF
UFDT
Total - competing 5 3 4 3 1 2
Total - non-competing 0 0 0 0 0 0
Total 5 3 4 3 1 2

Equality+LinearArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
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
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
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
iProver ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
Total - competing 5 3 4 4 1 2
Total - non-competing 0 0 0 0 0 0
Total 5 3 4 4 1 2

Equality+MachineArith

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

Equality+NonLinearArith

Solver Single Query Track Incremental Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
SMTInterpol ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
UltimateEliminator+MathSAT ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
Vampire ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5-lfsc ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
cvc5 ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFNIRA
UFDTNIA
UFNIA
UFNRA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
iProver ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
ANIA
AUFDTNIRA
AUFNIA
AUFNIRA
UFDTNIA
UFDTNIRA
UFNIA
Total - competing 4 3 3 3 1 2
Total - non-competing 0 0 0 0 0 0
Total 4 3 3 3 1 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
BVFP
BVFPLRA
FP
FPLRA
UltimateEliminator+MathSAT BVFP
BVFPLRA
FP
FPLRA
BVFP
BVFPLRA
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 3 2 0 0
Total - non-competing 0 0 0 0 0 0
Total 3 3 3 2 0 0

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
UltimateIntBlastingWrapper+SMTInterpol QF_BV
Yices2 QF_BV
QF_BV
QF_BV
QF_BV
Z3-Owl QF_BV
QF_BV
cvc5-lfsc QF_BV
cvc5 QF_BV
QF_BV
QF_BV
QF_BV
QF_BV
Total - competing 6 4 3 4 2 0 1
Total - non-competing 0 0 0 0 0 0 0
Total 6 4 3 4 2 0 1

QF_Datatypes

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

QF_Equality

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
OpenSMT QF_AX
QF_UF
QF_UF
QF_AX
QF_UF
Yices2 QF_AX
QF_UF
QF_UF
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_AX
QF_UF
QF_AX
QF_UF
Total - competing 3 3 2 3 2 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 3 3 2 3 2 0 0

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_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
UltimateIntBlastingWrapper+SMTInterpol QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
Yices2 QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
Z3-Owl QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
cvc5-lfsc QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
cvc5 QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
QF_ABV
QF_AUFBV
QF_UFBV
QF_UFBVDT
Total - competing 5 3 3 3 2 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 5 3 3 3 2 0 0

QF_Equality+Bitvec+Arith

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

QF_Equality+LinearArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
OpenSMT QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
SMTInterpol QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
Yices2 QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5-lfsc QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
cvc5 QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
QF_ALIA
QF_AUFLIA
QF_UFDTLIA
QF_UFDTLIRA
QF_UFIDL
QF_UFLIA
QF_UFLRA
Total - competing 4 4 3 4 3 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 4 4 3 4 3 0 0

QF_Equality+NonLinearArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
SMTInterpol QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
Yices2 QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
cvc5-lfsc QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
cvc5 QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
QF_ANIA
QF_AUFNIA
QF_UFDTNIA
QF_UFNIA
QF_UFNRA
Total - competing 3 3 2 2 3 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 3 3 2 2 3 0 0

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_UFFPDTNIRA
QF_ABVFP
QF_ABVFPLRA
QF_BVFP
QF_BVFPLRA
QF_FP
QF_UFFP
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
COLIBRI QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTNIRA
Z3-Owl 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_UFFP
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
QF_ABVFP
QF_ABVFPLRA
QF_AUFBVFP
QF_BVFP
QF_BVFPLRA
QF_FP
QF_FPLRA
QF_UFFP
QF_UFFPDTNIRA
Total - competing 4 2 2 2 2 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 4 2 2 2 2 0 0

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_LIRA
QF_LIA
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
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_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
Total - competing 5 4 3 5 3 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 5 4 3 5 3 0 0

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
SMTInterpol QF_LRA
QF_RDL
QF_LRA
QF_LRA
QF_RDL
QF_LRA
QF_RDL
QF_LRA
QF_RDL
Yaga QF_LRA
QF_RDL
QF_LRA
QF_RDL
Yices2 QF_LRA
QF_RDL
QF_LRA
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
Total - competing 5 4 3 5 3 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 5 4 3 5 3 0 0

QF_NonLinearIntArith

Solver Single Query Track Incremental Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
SMTInterpol QF_NIA
Yices2 QF_NIA
QF_NIRA
QF_NIA
QF_NIA
QF_NIRA
Z3++ 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
QF_NIA
QF_NIRA
ismt QF_NIA
QF_NIRA
yices-ismt QF_NIA
QF_NIRA
z3-alpha QF_NIA
QF_NIRA
Total - competing 5 3 1 4 2 0 0
Total - non-competing 0 0 0 0 0 0 0
Total 5 3 1 4 2 0 0

QF_NonLinearRealArith

Solver Single Query Track Unsat Core Track Model Validation Track Proof Exhibition Track Cloud Track Parallel Track
SMT-RAT-MCSAT QF_NRA
QF_NRA
Yices2 QF_NRA
QF_NRA
Z3++ QF_NRA
QF_NRA
cvc5-NRA-LS QF_NRA
QF_NRA
cvc5-lfsc QF_NRA
cvc5 QF_NRA
QF_NRA
QF_NRA
QF_NRA
z3-alpha QF_NRA
Total - competing 6 1 5 2 0 0
Total - non-competing 0 0 0 0 0 0
Total 6 1 5 2 0 0

QF_Strings

Solver Single Query Track Unsat Core Track Proof Exhibition Track Cloud Track Parallel Track
OSTRICH QF_S
QF_SLIA
QF_SNIA
Z3-Noodler 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
z3-alpha QF_S
QF_SLIA
QF_SNIA
Total - competing 4 1 2 0 0
Total - non-competing 0 0 0 0 0
Total 4 1 2 0 0