SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

SMT-COMP 2021 Results - Single Query Track (Summary)

Summary of all competition results for the Single Query Track.
Results are given ranked by performance for each scoring scheme (best solver is given as left-most solver).

Arith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	z3ⁿ, 2020-z3ⁿ, 2019-Par4ⁿ, cvc5 - fixedⁿ, cvc5, 2020-CVC4ⁿ, UltimateEliminator+MathSAT, Vampire, Vampire - fixedⁿ, Yices2-QS, iProver, SMTInterpol, veriT, 2018-Z3ⁿ
Parallel Performance	cvc5	z3ⁿ, 2020-z3ⁿ, 2019-Par4ⁿ, cvc5 - fixedⁿ, cvc5, 2020-CVC4ⁿ, UltimateEliminator+MathSAT, Vampire, Vampire - fixedⁿ, Yices2-QS, iProver, SMTInterpol, veriT, 2018-Z3ⁿ
SAT Performance	cvc5	z3ⁿ, 2020-z3ⁿ, 2019-Par4ⁿ, cvc5 - fixedⁿ, cvc5, 2020-CVC4ⁿ, UltimateEliminator+MathSAT, Yices2-QS, 2018-Z3ⁿ, SMTInterpol, Vampire, Vampire - fixedⁿ, veriT, iProver
UNSAT Performance	Vampire	z3ⁿ, 2020-z3ⁿ, Vampire, Vampire - fixedⁿ, 2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, 2019-Par4ⁿ, UltimateEliminator+MathSAT, iProver, Yices2-QS, SMTInterpol, veriT, 2018-Z3ⁿ
24s Performance	cvc5	z3ⁿ, 2020-z3ⁿ, 2019-Par4ⁿ, cvc5 - fixedⁿ, cvc5, 2020-CVC4ⁿ, UltimateEliminator+MathSAT, Vampire, Vampire - fixedⁿ, Yices2-QS, iProver, SMTInterpol, veriT, 2018-Z3ⁿ

Bitvec

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2019-Par4ⁿ, cvc5, z3ⁿ, Yices2-QS, UltimateEliminator+MathSAT
Parallel Performance	cvc5	2019-Par4ⁿ, cvc5, z3ⁿ, Yices2-QS, UltimateEliminator+MathSAT
SAT Performance	cvc5	2019-Par4ⁿ, z3ⁿ, cvc5, Yices2-QS, UltimateEliminator+MathSAT
UNSAT Performance	cvc5	2019-Par4ⁿ, cvc5, z3ⁿ, Yices2-QS, UltimateEliminator+MathSAT
24s Performance	cvc5	2019-Par4ⁿ, z3ⁿ, cvc5, Yices2-QS, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2020-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, Vampire, Vampire - fixedⁿ, 2020-z3ⁿ, z3ⁿ, veriT, 2019-Par4ⁿ, iProver, SMTInterpol, 2018-CVC4ⁿ, 2019-CVC4ⁿ, UltimateEliminator+MathSAT, 2018-Z3ⁿ, 2020-Vampireⁿ
Parallel Performance	cvc5	2020-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, Vampire, Vampire - fixedⁿ, 2020-z3ⁿ, z3ⁿ, veriT, iProver, 2019-Par4ⁿ, SMTInterpol, 2018-CVC4ⁿ, 2019-CVC4ⁿ, UltimateEliminator+MathSAT, 2018-Z3ⁿ, 2020-Vampireⁿ
SAT Performance	cvc5	2020-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, z3ⁿ, 2020-z3ⁿ, 2018-CVC4ⁿ, Vampire, Vampire - fixedⁿ, 2020-Vampireⁿ, SMTInterpol, 2019-Par4ⁿ, UltimateEliminator+MathSAT, 2018-Z3ⁿ, 2019-CVC4ⁿ, iProver, veriT
UNSAT Performance	cvc5	2020-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, Vampire, Vampire - fixedⁿ, veriT, 2020-z3ⁿ, z3ⁿ, iProver, 2019-Par4ⁿ, SMTInterpol, 2018-CVC4ⁿ, 2019-CVC4ⁿ, UltimateEliminator+MathSAT, 2018-Z3ⁿ, 2020-Vampireⁿ
24s Performance	cvc5	cvc5, cvc5 - fixedⁿ, 2020-CVC4ⁿ, Vampire, Vampire - fixedⁿ, 2020-z3ⁿ, veriT, z3ⁿ, 2019-Par4ⁿ, iProver, SMTInterpol, 2018-CVC4ⁿ, UltimateEliminator+MathSAT, 2019-CVC4ⁿ, 2018-Z3ⁿ, 2020-Vampireⁿ

Equality+MachineArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	cvc5, cvc5 - fixedⁿ, 2020-CVC4ⁿ, z3ⁿ, 2020-z3ⁿ, 2018-Z3ⁿ, UltimateEliminator+MathSAT
Parallel Performance	cvc5	cvc5, cvc5 - fixedⁿ, 2020-CVC4ⁿ, z3ⁿ, 2020-z3ⁿ, 2018-Z3ⁿ, UltimateEliminator+MathSAT
SAT Performance	cvc5	2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, 2020-z3ⁿ, 2018-Z3ⁿ, UltimateEliminator+MathSAT
UNSAT Performance	cvc5	cvc5, cvc5 - fixedⁿ, 2020-CVC4ⁿ, z3ⁿ, 2020-z3ⁿ, 2018-Z3ⁿ, UltimateEliminator+MathSAT
24s Performance	cvc5	cvc5 - fixedⁿ, cvc5, 2020-CVC4ⁿ, z3ⁿ, 2020-z3ⁿ, 2018-Z3ⁿ, UltimateEliminator+MathSAT

Equality+NonLinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	Vampire	2020-CVC4ⁿ, cvc5 - fixedⁿ, Vampire, Vampire - fixedⁿ, 2020-Vampireⁿ, z3ⁿ, iProver, UltimateEliminator+MathSAT, SMTInterpol, cvc5, 2019-Par4ⁿ
Parallel Performance	iProver	2020-CVC4ⁿ, cvc5 - fixedⁿ, Vampire - fixedⁿ, 2020-Vampireⁿ, z3ⁿ, iProver, UltimateEliminator+MathSAT, SMTInterpol, cvc5, 2019-Par4ⁿ, Vampire
SAT Performance	UltimateEliminator+MathSAT	2020-CVC4ⁿ, cvc5 - fixedⁿ, z3ⁿ, UltimateEliminator+MathSAT, SMTInterpol, Vampire, iProver, Vampire - fixedⁿ, 2020-Vampireⁿ, cvc5, 2019-Par4ⁿ
UNSAT Performance	cvc5	cvc5, cvc5 - fixedⁿ, 2020-CVC4ⁿ, Vampire - fixedⁿ, 2020-Vampireⁿ, 2019-Par4ⁿ, z3ⁿ, iProver, UltimateEliminator+MathSAT, SMTInterpol, Vampire
24s Performance	Vampire	cvc5 - fixedⁿ, 2020-CVC4ⁿ, z3ⁿ, Vampire, Vampire - fixedⁿ, 2020-Vampireⁿ, iProver, UltimateEliminator+MathSAT, SMTInterpol, cvc5, 2019-Par4ⁿ

Equality

Scoring Scheme	Winner	Ranking
Sequential Performance	Vampire	2020-CVC4ⁿ, Vampire, 2020-Vampireⁿ, Vampire - fixedⁿ, cvc5, iProver - fixed2ⁿ, iProver - fixedⁿ, veriT, z3ⁿ, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver
Parallel Performance	Vampire	2020-CVC4ⁿ, Vampire, 2020-Vampireⁿ, Vampire - fixedⁿ, cvc5, iProver - fixed2ⁿ, iProver - fixedⁿ, veriT, z3ⁿ, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver
SAT Performance	Vampire	2020-CVC4ⁿ, 2020-Vampireⁿ, Vampire, Vampire - fixedⁿ, cvc5, iProver - fixed2ⁿ, iProver, iProver - fixedⁿ, z3ⁿ, Yices2, SMTInterpol, UltimateEliminator+MathSAT, veriT
UNSAT Performance	cvc5	2020-CVC4ⁿ, cvc5, Vampire, Vampire - fixedⁿ, 2020-Vampireⁿ, iProver - fixed2ⁿ, iProver - fixedⁿ, veriT, z3ⁿ, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver
24s Performance	Vampire	2020-Vampireⁿ, Vampire, Vampire - fixedⁿ, cvc5, 2020-CVC4ⁿ, iProver - fixed2ⁿ, iProver - fixedⁿ, veriT, z3ⁿ, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver

FPArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	cvc5, 2020-CVC4ⁿ, z3ⁿ, UltimateEliminator+MathSAT, 2019-Z3ⁿ
Parallel Performance	cvc5	cvc5, 2020-CVC4ⁿ, z3ⁿ, UltimateEliminator+MathSAT, 2019-Z3ⁿ
SAT Performance	cvc5	cvc5, 2020-CVC4ⁿ, z3ⁿ, UltimateEliminator+MathSAT, 2019-Z3ⁿ
UNSAT Performance	cvc5	cvc5, z3ⁿ, 2020-CVC4ⁿ, UltimateEliminator+MathSAT, 2019-Z3ⁿ
24s Performance	cvc5	cvc5, 2020-CVC4ⁿ, z3ⁿ, UltimateEliminator+MathSAT, 2019-Z3ⁿ

QF_Bitvec

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	2020-Bitwuzla-fixedⁿ, Bitwuzla, Yices2, STP, cvc5, MathSAT5ⁿ, z3ⁿ
Parallel Performance	Bitwuzla	2020-Bitwuzla-fixedⁿ, Bitwuzla, Yices2, STP, cvc5, MathSAT5ⁿ, z3ⁿ
SAT Performance	Bitwuzla	2020-Bitwuzla-fixedⁿ, Bitwuzla, Yices2, STP, cvc5, z3ⁿ, MathSAT5ⁿ
UNSAT Performance	Yices2	2020-Bitwuzla-fixedⁿ, Yices2, STP, Bitwuzla, cvc5, MathSAT5ⁿ, z3ⁿ
24s Performance	Bitwuzla	2020-Bitwuzla-fixedⁿ, Bitwuzla, Yices2, STP, cvc5, MathSAT5ⁿ, z3ⁿ

QF_Equality+Bitvec

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	2020-Bitwuzlaⁿ, Bitwuzla, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, cvc5
Parallel Performance	Bitwuzla	2020-Bitwuzlaⁿ, Bitwuzla, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, cvc5
SAT Performance	Bitwuzla	2020-Bitwuzlaⁿ, Bitwuzla, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, cvc5
UNSAT Performance	Bitwuzla	Bitwuzla, 2020-Bitwuzlaⁿ, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, cvc5, z3ⁿ
24s Performance	Bitwuzla	Bitwuzla, 2020-Bitwuzlaⁿ, 2020-Yices2-fixedⁿ, 2020-Yices2ⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, cvc5

QF_Equality+LinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	SMTInterpol	SMTInterpol, cvc5 - fixedⁿ, cvc5, z3ⁿ, Yices2, MathSAT5ⁿ, veriT, 2019-Yices 2.6.2ⁿ, 2019-SMTInterpolⁿ, mc2, 2018-Yicesⁿ
Parallel Performance	SMTInterpol	SMTInterpol, cvc5 - fixedⁿ, cvc5, z3ⁿ, Yices2, MathSAT5ⁿ, veriT, 2019-Yices 2.6.2ⁿ, 2019-SMTInterpolⁿ, mc2, 2018-Yicesⁿ
SAT Performance	SMTInterpol	SMTInterpol, cvc5 - fixedⁿ, cvc5, Yices2, z3ⁿ, MathSAT5ⁿ, veriT, 2019-Yices 2.6.2ⁿ, 2019-SMTInterpolⁿ, mc2, 2018-Yicesⁿ
UNSAT Performance	cvc5	cvc5, SMTInterpol, cvc5 - fixedⁿ, MathSAT5ⁿ, z3ⁿ, Yices2, 2019-Yices 2.6.2ⁿ, veriT, 2019-SMTInterpolⁿ, mc2, 2018-Yicesⁿ
24s Performance	SMTInterpol	SMTInterpol, cvc5, cvc5 - fixedⁿ, Yices2, z3ⁿ, MathSAT5ⁿ, veriT, 2019-Yices 2.6.2ⁿ, 2019-SMTInterpolⁿ, mc2, 2018-Yicesⁿ

QF_Equality+NonLinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2020-CVC4ⁿ, z3ⁿ, 2019-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, MathSAT5ⁿ, Yices2, 2019-Par4ⁿ, 2019-MathSAT-defaultⁿ, veriT+raSAT+Redlog
Parallel Performance	cvc5	2020-CVC4ⁿ, z3ⁿ, 2019-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, MathSAT5ⁿ, Yices2, 2019-Par4ⁿ, 2019-MathSAT-defaultⁿ, veriT+raSAT+Redlog
SAT Performance	cvc5	2020-CVC4ⁿ, 2019-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, z3ⁿ, MathSAT5ⁿ, Yices2, 2019-Par4ⁿ, 2019-MathSAT-defaultⁿ, veriT+raSAT+Redlog
UNSAT Performance	cvc5	z3ⁿ, 2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, 2019-CVC4ⁿ, MathSAT5ⁿ, Yices2, 2019-MathSAT-defaultⁿ, 2019-Par4ⁿ, veriT+raSAT+Redlog
24s Performance	cvc5	2020-CVC4ⁿ, z3ⁿ, 2019-CVC4ⁿ, cvc5 - fixedⁿ, cvc5, MathSAT5ⁿ, Yices2, 2019-Par4ⁿ, 2019-MathSAT-defaultⁿ, veriT+raSAT+Redlog

QF_Equality

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	z3ⁿ, cvc5, 2020-z3ⁿ, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, SMTInterpol, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT
Parallel Performance	cvc5	z3ⁿ, cvc5, 2020-z3ⁿ, SMTInterpol, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT
SAT Performance	cvc5	z3ⁿ, cvc5, 2020-z3ⁿ, SMTInterpol, 2020-Yices2-fixedⁿ, 2020-Yices2ⁿ, Yices2, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT
UNSAT Performance	cvc5	z3ⁿ, cvc5, 2020-z3ⁿ, 2020-Yices2ⁿ, 2020-Yices2-fixedⁿ, Yices2, SMTInterpol, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT
24s Performance	Yices2	2020-Yices2-fixedⁿ, 2020-Yices2ⁿ, Yices2, z3ⁿ, 2020-z3ⁿ, cvc5, SMTInterpol, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT

QF_FPArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	cvc5, Bitwuzla, 2020-CVC4ⁿ, MathSAT5ⁿ, 2020-MathSAT5ⁿ, 2020-Bitwuzlaⁿ, 2020-Bitwuzla-fixedⁿ, COLIBRI - fixedⁿ, z3ⁿ, cvc5 - fixedⁿ, 2020-COLIBRIⁿ, COLIBRI
Parallel Performance	cvc5	cvc5, Bitwuzla, 2020-CVC4ⁿ, MathSAT5ⁿ, 2020-MathSAT5ⁿ, 2020-Bitwuzlaⁿ, 2020-Bitwuzla-fixedⁿ, COLIBRI - fixedⁿ, z3ⁿ, cvc5 - fixedⁿ, 2020-COLIBRIⁿ, COLIBRI
SAT Performance	cvc5	cvc5, Bitwuzla, MathSAT5ⁿ, 2020-MathSAT5ⁿ, 2020-CVC4ⁿ, COLIBRI - fixedⁿ, COLIBRI, 2020-Bitwuzla-fixedⁿ, 2020-Bitwuzlaⁿ, z3ⁿ, cvc5 - fixedⁿ, 2020-COLIBRIⁿ
UNSAT Performance	cvc5	cvc5, Bitwuzla, 2020-Bitwuzlaⁿ, 2020-Bitwuzla-fixedⁿ, 2020-CVC4ⁿ, MathSAT5ⁿ, 2020-MathSAT5ⁿ, COLIBRI - fixedⁿ, 2020-COLIBRIⁿ, z3ⁿ, cvc5 - fixedⁿ, COLIBRI
24s Performance	cvc5	cvc5, Bitwuzla, 2020-CVC4ⁿ, COLIBRI - fixedⁿ, MathSAT5ⁿ, 2020-MathSAT5ⁿ, 2020-Bitwuzla-fixedⁿ, 2020-Bitwuzlaⁿ, z3ⁿ, cvc5 - fixedⁿ, 2020-COLIBRIⁿ, COLIBRI

QF_LinearIntArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2019-Par4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, MathSAT5ⁿ, Yices2, SMTInterpol, OpenSMT - fixedⁿ, veriT, YicesLS, OpenSMT
Parallel Performance	cvc5	2019-Par4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, MathSAT5ⁿ, Yices2, SMTInterpol, OpenSMT - fixedⁿ, veriT, YicesLS, OpenSMT
SAT Performance	cvc5	2019-Par4ⁿ, z3ⁿ, cvc5, cvc5 - fixedⁿ, MathSAT5ⁿ, Yices2, SMTInterpol, OpenSMT - fixedⁿ, veriT, YicesLS, OpenSMT
UNSAT Performance	cvc5	2019-Par4ⁿ, cvc5, cvc5 - fixedⁿ, MathSAT5ⁿ, Yices2, z3ⁿ, OpenSMT - fixedⁿ, OpenSMT, SMTInterpol, veriT, YicesLS
24s Performance	Yices2	2019-Par4ⁿ, Yices2, z3ⁿ, MathSAT5ⁿ, cvc5, cvc5 - fixedⁿ, SMTInterpol, OpenSMT - fixedⁿ, veriT, YicesLS, OpenSMT

QF_LinearRealArith

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2, cvc5, OpenSMT, z3ⁿ, veriT, SMTInterpol, MathSAT5ⁿ, 2020-OpenSMTⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ, mc2
Parallel Performance	Yices2	Yices2, cvc5, OpenSMT, z3ⁿ, veriT, SMTInterpol, MathSAT5ⁿ, 2019-Par4ⁿ, 2020-OpenSMTⁿ, 2019-Yices 2.6.2ⁿ, mc2
SAT Performance	Yices2	Yices2, cvc5, OpenSMT, z3ⁿ, SMTInterpol, veriT, MathSAT5ⁿ, 2019-Par4ⁿ, 2020-OpenSMTⁿ, mc2, 2019-Yices 2.6.2ⁿ
UNSAT Performance	cvc5	cvc5, Yices2, z3ⁿ, OpenSMT, veriT, MathSAT5ⁿ, SMTInterpol, 2020-OpenSMTⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ, mc2
24s Performance	Yices2	Yices2, OpenSMT, veriT, z3ⁿ, cvc5, MathSAT5ⁿ, SMTInterpol, 2020-OpenSMTⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ, mc2

QF_NonLinearIntArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2019-Par4ⁿ, z3ⁿ, MathSAT5ⁿ, cvc5, cvc5 - fixedⁿ, Yices2, AProVE, SMT-RAT, 2020-SMT-RATⁿ
Parallel Performance	cvc5	2019-Par4ⁿ, z3ⁿ, MathSAT5ⁿ, cvc5, cvc5 - fixedⁿ, Yices2, AProVE, SMT-RAT, 2020-SMT-RATⁿ
SAT Performance	cvc5	2019-Par4ⁿ, z3ⁿ, cvc5, cvc5 - fixedⁿ, MathSAT5ⁿ, Yices2, AProVE, SMT-RAT, 2020-SMT-RATⁿ
UNSAT Performance	Yices2	2019-Par4ⁿ, z3ⁿ, Yices2, MathSAT5ⁿ, cvc5, cvc5 - fixedⁿ, SMT-RAT, 2020-SMT-RATⁿ, AProVE
24s Performance	Yices2	2019-Par4ⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, cvc5, cvc5 - fixedⁿ, AProVE, 2020-SMT-RATⁿ, SMT-RAT

QF_NonLinearRealArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2019-Par4ⁿ, cvc5, Yices2, z3ⁿ, SMT-RAT-MCSAT, veriT+raSAT+Redlog, MathSAT5ⁿ
Parallel Performance	cvc5	2019-Par4ⁿ, cvc5, Yices2, z3ⁿ, SMT-RAT-MCSAT, veriT+raSAT+Redlog, MathSAT5ⁿ
SAT Performance	cvc5	2019-Par4ⁿ, cvc5, z3ⁿ, Yices2, SMT-RAT-MCSAT, veriT+raSAT+Redlog, MathSAT5ⁿ
UNSAT Performance	cvc5	2019-Par4ⁿ, cvc5, Yices2, MathSAT5ⁿ, z3ⁿ, SMT-RAT-MCSAT, veriT+raSAT+Redlog
24s Performance	cvc5	2019-Par4ⁿ, cvc5, Yices2, z3ⁿ, SMT-RAT-MCSAT, veriT+raSAT+Redlog, MathSAT5ⁿ

QF_Strings

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, Z3str4
Parallel Performance	cvc5	2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, Z3str4
SAT Performance	cvc5	2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, Z3str4
UNSAT Performance	cvc5	2020-CVC4ⁿ, cvc5, cvc5 - fixedⁿ, z3ⁿ, Z3str4
24s Performance	cvc5	cvc5 - fixedⁿ, cvc5, 2020-CVC4ⁿ, z3ⁿ, Z3str4