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

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 -1 0 The OpenSMT Solver in SMT-COMP 2021
SMTS portfolio X -1 -1 0 The OpenSMT Solver in SMT-COMP 2021
STP-CMS-Cloud X X -1 -1 0 STP in the SMT-COMP 2021
STP-parallel X -1 -1 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 -1 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
Par4n X X -1 -1 0 Par4 System Description
Total - competing 19 7 7 7 5 4
Total - non-competing 0 0 0 0 1 1
Total 19 7 7 7 6 5 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
Par4n LRA
NRA
LRA
NRA
Total - competing 7 3 5 2 2
Total - non-competing 0 0 0 1 1
Total 7 3 5 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
Par4n BV
BV
Total - competing 3 2 2 1 1
Total - non-competing 0 0 0 1 1
Total 3 2 2 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
Par4n UF
UF
Total - competing 7 3 5 2 2
Total - non-competing 0 0 0 1 1
Total 7 3 5 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
AUFFPDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
ALIA
AUFDTLIA
AUFDTLIRA
AUFFPDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5-inc ALIA
UFLRA
cvc5-uc ALIA
AUFDTLIA
AUFDTLIRA
AUFFPDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
cvc5 ALIA
AUFDTLIA
AUFDTLIRA
AUFFPDTLIRA
AUFLIA
AUFLIRA
UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
iProver UFDTLIA
UFDTLIRA
UFIDL
UFLIA
UFLRA
veriT ALIA
AUFLIA
AUFLIRA
UFIDL
UFLIA
UFLRA
Par4n AUFLIRA
UFIDL
UFLIA
AUFLIRA
UFIDL
UFLIA
Total - competing 6 3 5 2 2
Total - non-competing 0 0 0 1 1
Total 6 3 5 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
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
cvc5-inc ABVFP
cvc5-uc ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
cvc5 ABV
ABVFP
ABVFPLRA
AUFBV
AUFBVDTLIA
AUFBVDTNIA
AUFBVFP
UFBV
UFBVFP
UFBVLIA
UFFPDTLIRA
UFFPDTNIRA
Par4n UFBV
UFBV
Total - competing 2 2 2 1 1
Total - non-competing 0 0 0 1 1
Total 2 2 2 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
Par4n AUFNIRA
UFNIA
AUFNIRA
UFNIA
Total - competing 5 3 4 2 2
Total - non-competing 0 0 0 1 1
Total 5 3 4 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
Total - competing 2 2 2 1 1
Total - non-competing 0 0 0 0 0
Total 2 2 2 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
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
Par4n QF_BV
QF_BV
Total - competing 4 4 3 4 2 3
Total - non-competing 0 0 0 0 1 1
Total 4 4 3 4 3 4

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
Par4n QF_UF
QF_UF
Total - competing 5 4 4 4 3 1
Total - non-competing 0 0 0 0 1 1
Total 5 4 4 4 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
Par4n QF_ABV
QF_ABV
Total - competing 3 3 3 3 1 1
Total - non-competing 0 0 0 0 1 1
Total 3 3 3 3 2 2

QF_Equality+Bitvec+Arith

Solver Incremental Track
cvc5-inc 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 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
Total - competing 5 3 4 3 1 1
Total - non-competing 0 0 0 0 0 0
Total 5 3 4 3 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
Par4n QF_UFNRA
QF_UFNRA
Total - competing 3 3 2 1 1
Total - non-competing 0 0 0 1 1
Total 3 3 2 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
Par4n QF_BVFP
QF_FP
QF_BVFP
QF_FP
Total - competing 3 2 2 1 1
Total - non-competing 0 0 0 1 1
Total 3 2 2 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
Par4n QF_IDL
QF_LIA
QF_LIRA
QF_IDL
QF_LIA
QF_LIRA
Total - competing 6 4 4 5 3 1
Total - non-competing 0 0 0 0 1 1
Total 6 4 4 5 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
Par4n QF_LRA
QF_LRA
Total - competing 6 4 4 4 3 1
Total - non-competing 0 0 0 0 1 1
Total 6 4 4 4 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
Par4n QF_NIA
QF_NIA
Total - competing 4 3 2 1 1
Total - non-competing 0 0 0 1 1
Total 4 3 2 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
Par4n QF_NRA
QF_NRA
Total - competing 4 2 1 1
Total - non-competing 0 0 1 1
Total 4 2 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
Total - competing 2 1 1 1
Total - non-competing 0 0 0 0
Total 2 1 1 1