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

AUFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

AUFLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

AUFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Z3n, CVC4-uc
Parallel Performance	-	UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, CVC4-uc, Z3n

AUFNIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, 2018-CVC4 (unsat core)n, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4-uc	CVC4-uc, 2018-CVC4 (unsat core)n, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

BV

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	CVC4-uc, Z3n, 2018-Z3 (unsat core)n, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4-uc	CVC4-uc, Z3n, 2018-Z3 (unsat core)n, UltimateEliminator+MathSAT-5.5.4

LIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1
Parallel Performance	CVC4-uc	2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1

NIA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, 2018-CVC4 (unsat core)n, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	-	CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, 2018-CVC4 (unsat core)n, UltimateEliminator+MathSAT-5.5.4

QF_ABV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Z3n, 2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc
Parallel Performance	Yices 2.6.2	Z3n, 2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc

QF_ALIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	2018-Z3 (unsat core)n, Z3n, Yices 2.6.2, SMTInterpol, CVC4-uc
Parallel Performance	Yices 2.6.2	2018-Z3 (unsat core)n, Z3n, Yices 2.6.2, SMTInterpol, CVC4-uc

QF_ANIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n

QF_AUFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, Z3n, 2018-MathSAT (unsat core)n, CVC4-uc
Parallel Performance	Yices 2.6.2	Yices 2.6.2, Z3n, 2018-MathSAT (unsat core)n, CVC4-uc

QF_AUFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, Yices 2.6.2, SMTInterpol
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, Yices 2.6.2, SMTInterpol

QF_AUFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	MathSAT-default	2018-Z3 (unsat core)n, Z3n, MathSAT-default, CVC4-uc, MathSAT-na-ext
Parallel Performance	MathSAT-default	2018-Z3 (unsat core)n, Z3n, MathSAT-default, CVC4-uc, MathSAT-na-ext

QF_AX

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	2018-Yices (unsat core)n, Yices 2.6.2, Z3n, CVC4-uc, SMTInterpol
Parallel Performance	Yices 2.6.2	2018-Yices (unsat core)n, Yices 2.6.2, Z3n, CVC4-uc, SMTInterpol

QF_BV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc, Z3n
Parallel Performance	Yices 2.6.2	2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc, Z3n

QF_LIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, Z3n, 2018-SMTInterpol (unsat core)n, SMTInterpol, CVC4-uc
Parallel Performance	Yices 2.6.2	Yices 2.6.2, Z3n, 2018-SMTInterpol (unsat core)n, SMTInterpol, CVC4-uc

QF_LIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	Z3n, 2018-Z3 (unsat core)n, Yices 2.6.2, CVC4-uc, SMTInterpol
Parallel Performance	-	Z3n, 2018-Z3 (unsat core)n, Yices 2.6.2, CVC4-uc, SMTInterpol

QF_LRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, CVC4-uc, 2018-SMTInterpol (unsat core)n, Z3n, SMTInterpol
Parallel Performance	Yices 2.6.2	Yices 2.6.2, CVC4-uc, 2018-SMTInterpol (unsat core)n, Z3n, SMTInterpol

QF_NIA

Scoring Scheme	Winner	Ranking
Sequential Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, 2018-Z3 (unsat core)n, Z3n, CVC4-uc
Parallel Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, 2018-Z3 (unsat core)n, Z3n, CVC4-uc

QF_NIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	MathSAT-na-ext	MathSAT-na-ext, MathSAT-default, Z3n, 2018-Z3 (unsat core)n, CVC4-uc
Parallel Performance	MathSAT-na-ext	MathSAT-na-ext, MathSAT-default, Z3n, 2018-Z3 (unsat core)n, CVC4-uc

QF_NRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n

QF_UF

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, SMTInterpol, Z3n, CVC4-uc, 2018-CVC4 (unsat core)n
Parallel Performance	Yices 2.6.2	Yices 2.6.2, SMTInterpol, Z3n, CVC4-uc, 2018-CVC4 (unsat core)n

QF_UFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	2018-Z3 (unsat core)n, Z3n, Yices 2.6.2, CVC4-uc
Parallel Performance	Yices 2.6.2	2018-Z3 (unsat core)n, Z3n, Yices 2.6.2, CVC4-uc

QF_UFIDL

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yices (unsat core)n, CVC4-uc, Z3n, SMTInterpol
Parallel Performance	Yices 2.6.2	2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc, Z3n, SMTInterpol

QF_UFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Z3 (unsat core)n, Z3n, SMTInterpol, CVC4-uc
Parallel Performance	Yices 2.6.2	Yices 2.6.2, 2018-Z3 (unsat core)n, Z3n, SMTInterpol, CVC4-uc

QF_UFLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	Z3n, 2018-MathSAT (unsat core)n, CVC4-uc, Yices 2.6.2, SMTInterpol
Parallel Performance	CVC4-uc	Z3n, 2018-MathSAT (unsat core)n, CVC4-uc, Yices 2.6.2, SMTInterpol

QF_UFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	MathSAT-default	2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc
Parallel Performance	MathSAT-default	2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc

QF_UFNRA

Scoring Scheme	Winner	Ranking
Sequential Performance	MathSAT-default	2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc
Parallel Performance	MathSAT-default	2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc

UF

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

UFIDL

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel Performance	CVC4-uc	CVC4-uc, 2018-CVC4 (unsat core)n, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4

UFLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4-uc	2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4-uc	2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4