SMT-COMP 2022 Results - Unsat Core Track (Summary)

Summary of all competition results for the Unsat Core 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	cvc5, 2020-CVC4-ucn, z3-4.8.17n, Vampire, smtinterpol, UltimateEliminator+MathSAT
Parallel Performance	cvc5	cvc5, 2020-CVC4-ucn, z3-4.8.17n, Vampire, smtinterpol, UltimateEliminator+MathSAT

Bitvec

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2020-CVC4-ucn, cvc5, z3-4.8.17n, UltimateEliminator+MathSAT
Parallel Performance	cvc5	2020-CVC4-ucn, cvc5, z3-4.8.17n, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2021-cvc5-ucn, z3-4.8.17n, cvc5, Vampire, smtinterpol, UltimateEliminator+MathSAT
Parallel Performance	cvc5	2021-cvc5-ucn, z3-4.8.17n, cvc5, Vampire, smtinterpol, UltimateEliminator+MathSAT

Equality+MachineArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	z3-4.8.17n, cvc5, 2021-cvc5-ucn, UltimateEliminator+MathSAT
Parallel Performance	cvc5	z3-4.8.17n, cvc5, 2021-cvc5-ucn, UltimateEliminator+MathSAT

Equality+NonLinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2020-CVC4-ucn, cvc5, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT
Parallel Performance	cvc5	2020-CVC4-ucn, cvc5, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT

Equality

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	2020-CVC4-ucn, cvc5, Vampire, z3-4.8.17n, smtinterpol, UltimateEliminator+MathSAT
Parallel Performance	Vampire	Vampire, 2020-CVC4-ucn, cvc5, z3-4.8.17n, smtinterpol, UltimateEliminator+MathSAT

FPArith

Scoring Scheme	Winner	Ranking
Sequential Performance	-	2020-CVC4-ucn, z3-4.8.17n, UltimateEliminator+MathSAT, cvc5
Parallel Performance	-	2020-CVC4-ucn, z3-4.8.17n, UltimateEliminator+MathSAT, cvc5

QF_Bitvec

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla, 2020-Bitwuzla-fixedn, Yices2, z3-4.8.17n, cvc5, MathSATn
Parallel Performance	Bitwuzla	Bitwuzla, 2020-Bitwuzla-fixedn, Yices2, z3-4.8.17n, cvc5, MathSATn

QF_Datatypes

Scoring Scheme	Winner	Ranking
Sequential Performance	cvc5	z3-4.8.17n, 2021-z3n, cvc5, smtinterpol
Parallel Performance	cvc5	z3-4.8.17n, 2021-z3n, cvc5, smtinterpol

QF_Equality+Bitvec

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla, 2021-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn
Parallel Performance	Bitwuzla	Bitwuzla, 2021-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn

QF_Equality+LinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2, MathSATn, 2021-MathSAT5n, z3-4.8.17n, smtinterpol, cvc5
Parallel Performance	Yices2	Yices2, MathSATn, 2021-MathSAT5n, z3-4.8.17n, smtinterpol, cvc5

QF_Equality+NonLinearArith

Scoring Scheme	Winner	Ranking
Sequential Performance	smtinterpol	2021-cvc5-ucn, smtinterpol, MathSATn, z3-4.8.17n, cvc5
Parallel Performance	smtinterpol	2021-cvc5-ucn, smtinterpol, MathSATn, z3-4.8.17n, cvc5

QF_Equality

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	z3-4.8.17n, 2021-z3n, Yices2, MathSATn, smtinterpol, cvc5
Parallel Performance	Yices2	z3-4.8.17n, 2021-z3n, Yices2, MathSATn, smtinterpol, cvc5

QF_FPArith

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	z3-4.8.17n, Bitwuzla, 2021-Bitwuzlan, cvc5, MathSATn
Parallel Performance	Bitwuzla	z3-4.8.17n, Bitwuzla, 2021-Bitwuzlan, cvc5, MathSATn

QF_LinearIntArith

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	MathSATn, Yices2, z3-4.8.17n, 2021-cvc5-ucn, smtinterpol, cvc5
Parallel Performance	Yices2	MathSATn, Yices2, z3-4.8.17n, 2021-cvc5-ucn, smtinterpol, cvc5

QF_LinearRealArith

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	2020-Yices2n, Yices2, cvc5, z3-4.8.17n, MathSATn, smtinterpol
Parallel Performance	Yices2	2020-Yices2n, Yices2, cvc5, z3-4.8.17n, smtinterpol, MathSATn