SMT-COMP 2020 Results - Incremental Track (Summary)

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

ANIA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	CVC4-inc, 2018-CVC4 (incremental)n, UltimateEliminator+MathSAT

AUFNIRA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	2019-CVC4-incn, CVC4-inc, z3n, UltimateEliminator+MathSAT

BV

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	2019-Z3n, CVC4-inc, z3n, UltimateEliminator+MathSAT

BVFP

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	2019-CVC4-incn, CVC4-inc, UltimateEliminator+MathSAT

LIA

Scoring Scheme	Winner	Ranking
Parallel Performance	UltimateEliminator+MathSAT	z3n, 2018-Z3 (incremental)n, UltimateEliminator+MathSAT, CVC4-inc, SMTInterpol, SMTInterpol-fixedn

LRA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	CVC4-inc, UltimateEliminator+MathSAT, z3n, SMTInterpol-fixedn, SMTInterpol

QF_ABV

Scoring Scheme	Winner	Ranking
Parallel Performance	Bitwuzla	Bitwuzla-fixedn, Bitwuzla, Yices2 incremental, 2018-Boolector (incremental)n, Yices2-fixed incrementaln, MathSAT5n, z3n, CVC4-inc

QF_ABVFP

Scoring Scheme	Winner	Ranking
Parallel Performance	Bitwuzla	Bitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4-inc

QF_AUFBV

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	Yices2 incremental, Yices2-fixed incrementaln, 2019-Yices 2.6.2 Incrementaln, z3n, MathSAT5n, CVC4-inc, Bitwuzla, Bitwuzla-fixedn

QF_AUFLIA

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	2018-Yices (incremental)n, Yices2 incremental, Yices2-fixed incrementaln, z3n, SMTInterpol-fixedn, SMTInterpol, MathSAT5n, CVC4-inc

QF_BV

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	Yices2-fixed incrementaln, Yices2 incremental, 2019-Yices 2.6.2 Incrementaln, STP + CMS, Bitwuzla-fixedn, Bitwuzla, STP + MergeSAT, z3n, MathSAT5n, CVC4-inc, LazyBV2Int

QF_BVFP

The division has disagreements

Scoring Scheme	Winner	Ranking
Parallel Performance	Bitwuzla	Bitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4-inc, z3n

QF_FP

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	CVC4-inc, Bitwuzla, Bitwuzla-fixedn, MathSAT5n, z3n

QF_LIA

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	Yices2-fixed incrementaln, 2018-Yices (incremental)n, Yices2 incremental, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, CVC4-inc, z3n

QF_LRA

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	2018-MathSAT (incremental)n, MathSAT5n, Yices2-fixed incrementaln, Yices2 incremental, OpenSMT, SMTInterpol, SMTInterpol-fixedn, CVC4-inc, z3n

QF_NIA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	MathSAT5n, 2019-MathSAT-defaultn, CVC4-inc, z3n, Yices2-fixed incrementaln, Yices2 incremental

QF_UF

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	2019-Yices 2.6.2 Incrementaln, Yices2-fixed incrementaln, Yices2 incremental, z3n, CVC4-inc, SMTInterpol, SMTInterpol-fixedn, OpenSMT, MathSAT5n

QF_UFBV

Scoring Scheme	Winner	Ranking
Parallel Performance	Bitwuzla	Bitwuzla-fixedn, Bitwuzla, 2018-Boolector (incremental)n, Yices2 incremental, Yices2-fixed incrementaln, z3n, MathSAT5n, CVC4-inc

QF_UFFP

Scoring Scheme	Winner	Ranking
Parallel Performance	Bitwuzla	Bitwuzla-fixedn, Bitwuzla, CVC4-inc, MathSAT5n

QF_UFLIA

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	2018-Z3 (incremental)n, z3n, MathSAT5n, Yices2-fixed incrementaln, Yices2 incremental, SMTInterpol, SMTInterpol-fixedn, CVC4-inc

QF_UFLRA

Scoring Scheme	Winner	Ranking
Parallel Performance	Yices2 incremental	z3n, 2019-Z3n, MathSAT5n, Yices2 incremental, Yices2-fixed incrementaln, SMTInterpol, SMTInterpol-fixedn, CVC4-inc

QF_UFNIA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	MathSAT5n, 2019-MathSAT-defaultn, z3n, CVC4-inc, Yices2 incremental, Yices2-fixed incrementaln

UF

The division has disagreements

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	z3n, CVC4-inc, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT

UFLRA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	2019-Z3n, z3n, CVC4-inc, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT

UFNIA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	z3n, CVC4-inc, UltimateEliminator+MathSAT

UFNRA

Scoring Scheme	Winner	Ranking
Parallel Performance	CVC4-inc	z3n, CVC4-inc, UltimateEliminator+MathSAT