The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
n Non-competing.
Solver | Single Query Track | Incremental Track | Unsat Core Track | Proof Exhibition Track | Cloud Track | Parallel Track |
---|---|---|---|---|---|---|
SMTInterpol | LIA LRA |
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 |
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 |
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 |
Solver | Single Query Track | Incremental Track | Unsat Core Track | Proof Exhibition Track | Cloud Track | Parallel Track |
---|---|---|---|---|---|---|
UltimateEliminator+MathSAT | UF |
UF |
UF |
|||
Vampire | UF UFDT |
UF UFDT |
UF UFDT |
UF UFDT |
UF UFDT |
|
Yices2 | UF |
UF |
UF |
|||
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 |
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 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 |
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 |
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 |
ABV ABVFP ABVFPLRA AUFBV AUFBVFP UFBV UFBVFP |
|||
UltimateEliminator+MathSAT | ABV ABVFP ABVFPLRA AUFBV AUFBVFP UFBV UFBVFP UFBVLIA |
ABVFPLRA |
ABV ABVFP ABVFPLRA AUFBV AUFBVFP UFBV UFBVFP UFBVLIA |
|||
UltimateIntBlastingWrapper+SMTInterpol | ABV AUFBV AUFBVDTLIA UFBV UFBVDT UFBVLIA |
|||||
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 |
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 AUFNIA AUFNIRA UFNIA |
ANIA AUFNIRA UFNIA UFNRA |
ANIA AUFNIA AUFNIRA 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 |
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 |
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 |
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_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 |
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_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 |
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_ABV QF_AUFBV QF_UFBV |
|||
UltimateIntBlastingWrapper+SMTInterpol | QF_ABV QF_AUFBV QF_UFBV QF_UFBVDT |
||||||
Yices2 | QF_ABV QF_AUFBV QF_UFBV |
QF_ABV QF_AUFBV QF_UFBV |
QF_ABV QF_AUFBV QF_UFBV |
QF_ABV QF_AUFBV QF_UFBV |
|||
Z3-Owl | QF_ABV QF_AUFBV QF_UFBV |
||||||
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_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 |
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 |
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_UFIDL QF_UFLIA QF_UFLRA |
QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA |
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_UFIDL QF_UFLIA QF_UFLRA |
QF_ALIA QF_AUFLIA QF_UFLIA QF_UFLRA |
QF_ALIA QF_AUFLIA QF_UFIDL QF_UFLIA QF_UFLRA |
QF_ALIA QF_AUFLIA 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_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 |
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_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 |
|||
Yices2 | QF_ANIA QF_AUFNIA QF_UFNIA QF_UFNRA |
QF_ANIA QF_UFNIA QF_UFNRA |
QF_ANIA QF_AUFNIA 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_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 |
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_UFFP |
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 |
|||
COLIBRI | QF_ABVFP QF_ABVFPLRA QF_AUFBVFP QF_BVFP QF_BVFPLRA QF_FP QF_FPLRA QF_UFFP |
||||||
Z3-Owl | QF_BVFP QF_FP |
||||||
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_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 |
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 |
||||
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_IDL QF_LIA |
|||||
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 |
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_LRA |
|||||
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 |
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_NIA |
|||||
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 |
||||||
yices-ismt | QF_NIA |
||||||
z3-alpha | QF_NIA |
||||||
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 |
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 |
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 |
||||
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 |