Results Unsat Core

SMT-COMP 2020 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).

AUFBVDTLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

AUFDTLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

AUFDTNIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

AUFFPDTLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

AUFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT

AUFLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	z3ⁿ, CVC4-uc, SMTInterpol, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	z3ⁿ, CVC4-uc, SMTInterpol-fixedⁿ, SMTInterpol, UltimateEliminator+MathSAT

AUFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	UltimateEliminator+MathSAT, CVC4-uc, z3ⁿ
Parallel Performance	-	UltimateEliminator+MathSAT, CVC4-uc, z3ⁿ

AUFNIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT

BV

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT

BVFPLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

LIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT, SMTInterpol-fixedⁿ, SMTInterpol
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT, SMTInterpol-fixedⁿ, SMTInterpol

NIA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT
Parallel Performance	-	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT

QF_ABV

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	z3ⁿ, Bitwuzla, Yices2-fixedⁿ, Yices2, Bitwuzla-fixedⁿ, CVC4-uc, MathSAT5ⁿ
Parallel Performance	Bitwuzla	z3ⁿ, Bitwuzla, Yices2-fixedⁿ, Yices2, Bitwuzla-fixedⁿ, CVC4-uc, MathSAT5ⁿ

QF_ABVFP

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla, Bitwuzla-fixedⁿ, CVC4-uc, MathSAT5ⁿ
Parallel Performance	Bitwuzla	Bitwuzla, Bitwuzla-fixedⁿ, CVC4-uc, MathSAT5ⁿ

QF_ALIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	z3ⁿ, CVC4-uc, SMTInterpol-fixedⁿ, SMTInterpol, MathSAT5ⁿ, Yices2-fixedⁿ, Yices2
Parallel Performance	CVC4-uc	z3ⁿ, CVC4-uc, SMTInterpol-fixedⁿ, SMTInterpol, MathSAT5ⁿ, Yices2-fixedⁿ, Yices2

QF_AUFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2, Yices2-fixedⁿ, z3ⁿ, Bitwuzla, Bitwuzla-fixedⁿ, CVC4-uc, MathSAT5ⁿ
Parallel Performance	Yices2	Yices2, Yices2-fixedⁿ, z3ⁿ, Bitwuzla, Bitwuzla-fixedⁿ, CVC4-uc, MathSAT5ⁿ

QF_AUFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, Yices2-fixedⁿ, Yices2, SMTInterpol, SMTInterpol-fixedⁿ, MathSAT5ⁿ
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, Yices2-fixedⁿ, Yices2, SMTInterpol-fixedⁿ, SMTInterpol, MathSAT5ⁿ

QF_AX

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2-fixedⁿ, Yices2, z3ⁿ, CVC4-uc, MathSAT5ⁿ, SMTInterpol, SMTInterpol-fixedⁿ
Parallel Performance	Yices2	Yices2-fixedⁿ, Yices2, z3ⁿ, CVC4-uc, MathSAT5ⁿ, SMTInterpol, SMTInterpol-fixedⁿ

QF_BV

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, Yices2-fixedⁿ, Yices2, CVC4-uc, z3ⁿ, MathSAT5ⁿ
Parallel Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, Yices2-fixedⁿ, Yices2, CVC4-uc, z3ⁿ, MathSAT5ⁿ

QF_BVFP

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla, Bitwuzla-fixedⁿ, z3ⁿ, CVC4-uc, MathSAT5ⁿ
Parallel Performance	Bitwuzla	Bitwuzla, Bitwuzla-fixedⁿ, z3ⁿ, CVC4-uc, MathSAT5ⁿ

QF_FP

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, CVC4-uc, z3ⁿ, MathSAT5ⁿ
Parallel Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, CVC4-uc, z3ⁿ, MathSAT5ⁿ

QF_LIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2-fixedⁿ, Yices2, z3ⁿ, MathSAT5ⁿ, CVC4-uc, SMTInterpol, SMTInterpol-fixedⁿ
Parallel Performance	Yices2	Yices2-fixedⁿ, Yices2, z3ⁿ, MathSAT5ⁿ, CVC4-uc, SMTInterpol, SMTInterpol-fixedⁿ

QF_LIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	z3ⁿ, Yices2-fixedⁿ, Yices2, CVC4-uc, MathSAT5ⁿ, SMTInterpol, SMTInterpol-fixedⁿ
Parallel Performance	-	z3ⁿ, Yices2-fixedⁿ, Yices2, CVC4-uc, MathSAT5ⁿ, SMTInterpol-fixedⁿ, SMTInterpol

QF_LRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2, Yices2-fixedⁿ, CVC4-uc, z3ⁿ, MathSAT5ⁿ, SMTInterpol-fixedⁿ, SMTInterpol
Parallel Performance	Yices2	Yices2, Yices2-fixedⁿ, CVC4-uc, z3ⁿ, MathSAT5ⁿ, SMTInterpol-fixedⁿ, SMTInterpol

QF_UF

Scoring Scheme	Winner	Ranking
Sequential Performance	SMTInterpol	SMTInterpol-fixedⁿ, SMTInterpol, z3ⁿ, Yices2-fixedⁿ, Yices2, CVC4-uc, MathSAT5ⁿ
Parallel Performance	SMTInterpol	SMTInterpol-fixedⁿ, SMTInterpol, z3ⁿ, Yices2-fixedⁿ, Yices2, CVC4-uc, MathSAT5ⁿ

QF_UFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	z3ⁿ, Yices2, Yices2-fixedⁿ, Bitwuzla-fixedⁿ, Bitwuzla, CVC4-uc, MathSAT5ⁿ
Parallel Performance	Yices2	z3ⁿ, Yices2, Yices2-fixedⁿ, Bitwuzla-fixedⁿ, Bitwuzla, CVC4-uc, MathSAT5ⁿ

QF_UFFP

Scoring Scheme	Winner	Ranking
Sequential Performance	-	MathSAT5ⁿ, Bitwuzla, Bitwuzla-fixedⁿ, CVC4-uc
Parallel Performance	-	MathSAT5ⁿ, Bitwuzla, Bitwuzla-fixedⁿ, CVC4-uc

QF_UFIDL

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2-fixedⁿ, Yices2, CVC4-uc, MathSAT5ⁿ, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol
Parallel Performance	Yices2	Yices2-fixedⁿ, Yices2, CVC4-uc, MathSAT5ⁿ, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol

QF_UFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, CVC4-uc
Parallel Performance	Yices2	Yices2-fixedⁿ, Yices2, MathSAT5ⁿ, z3ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, CVC4-uc

QF_UFLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	z3ⁿ, MathSAT5ⁿ, CVC4-uc, Yices2, Yices2-fixedⁿ, SMTInterpol-fixedⁿ, SMTInterpol
Parallel Performance	CVC4-uc	z3ⁿ, MathSAT5ⁿ, CVC4-uc, Yices2-fixedⁿ, Yices2, SMTInterpol-fixedⁿ, SMTInterpol

UF

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, UltimateEliminator+MathSAT

UFDT

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

UFDTLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

UFDTNIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

UFFPDTLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

UFFPDTNIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, UltimateEliminator+MathSAT

UFIDL

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	z3ⁿ, CVC4-uc, SMTInterpol, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	z3ⁿ, CVC4-uc, SMTInterpol, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT

UFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, UltimateEliminator+MathSAT

UFLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	SMTInterpol	z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, CVC4-uc, UltimateEliminator+MathSAT
Parallel Performance	SMTInterpol	z3ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, CVC4-uc, UltimateEliminator+MathSAT

UFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT
Parallel Performance	CVC4-uc	CVC4-uc, z3ⁿ, UltimateEliminator+MathSAT