Results Single Query

SMT-COMP 2020 alternative results - Single Query Track (Summary)

What the results of single-query SMT-COMP 2020 would have looked like with divisions split as shown below.

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).

BV

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2019-Par4ⁿ, CVC4, Bitwuzla-fixedⁿ, z3ⁿ, UltimateEliminator+MathSAT, Bitwuzla
Parallel Performance	CVC4	2019-Par4ⁿ, CVC4, Bitwuzla-fixedⁿ, z3ⁿ, UltimateEliminator+MathSAT, Bitwuzla
SAT Performance	CVC4	2019-Par4ⁿ, Bitwuzla-fixedⁿ, z3ⁿ, CVC4, UltimateEliminator+MathSAT, Bitwuzla
UNSAT Performance	CVC4	2019-Par4ⁿ, CVC4, Bitwuzla-fixedⁿ, z3ⁿ, UltimateEliminator+MathSAT, Bitwuzla
24s Performance	CVC4	2019-Par4ⁿ, Bitwuzla-fixedⁿ, z3ⁿ, CVC4, UltimateEliminator+MathSAT, Bitwuzla

QF_BV

Scoring Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, Yices2-fixedⁿ, 2019-Boolectorⁿ, 2019-Poolectorⁿ, STP + CMS, MinkeyRink-fixedⁿ, CVC4, MathSAT5ⁿ, z3ⁿ, LazyBV2Int, MinkeyRink, STP + MergeSAT, Yices2
Parallel Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, 2019-Poolectorⁿ, Yices2-fixedⁿ, 2019-Boolectorⁿ, MinkeyRink-fixedⁿ, STP + CMS, CVC4, MathSAT5ⁿ, z3ⁿ, LazyBV2Int, MinkeyRink, STP + MergeSAT, Yices2
SAT Performance	Bitwuzla	Bitwuzla-fixedⁿ, MinkeyRink-fixedⁿ, Bitwuzla, 2019-Poolectorⁿ, 2019-Boolectorⁿ, Yices2-fixedⁿ, STP + CMS, CVC4, STP + MergeSAT, z3ⁿ, MathSAT5ⁿ, LazyBV2Int, MinkeyRink, Yices2
UNSAT Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, Yices2-fixedⁿ, 2019-Poolectorⁿ, 2019-Boolectorⁿ, STP + CMS, Yices2, MinkeyRink-fixedⁿ, CVC4, MathSAT5ⁿ, z3ⁿ, LazyBV2Int, MinkeyRink, STP + MergeSAT
24s Performance	Bitwuzla	2019-Poolectorⁿ, MinkeyRink-fixedⁿ, Bitwuzla, Bitwuzla-fixedⁿ, Yices2-fixedⁿ, 2019-Boolectorⁿ, STP + CMS, STP + MergeSAT, CVC4, MathSAT5ⁿ, z3ⁿ, LazyBV2Int, MinkeyRink, Yices2

QF_Equality (QF_UF, QF_AX, QF_DT)

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	z3ⁿ, CVC4, Yices2, Yices2-fixedⁿ, 2019-Yices 2.6.2ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT, Alt-Ergo, 2018-Yicesⁿ, 2018-CVC4ⁿ
Parallel Performance	CVC4	z3ⁿ, CVC4, Yices2, 2019-Yices 2.6.2ⁿ, Yices2-fixedⁿ, SMTInterpol, SMTInterpol-fixedⁿ, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT, Alt-Ergo, 2018-Yicesⁿ, 2018-CVC4ⁿ
SAT Performance	CVC4	z3ⁿ, CVC4, Yices2, 2019-Yices 2.6.2ⁿ, Yices2-fixedⁿ, SMTInterpol, SMTInterpol-fixedⁿ, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT, 2018-Yicesⁿ, 2018-CVC4ⁿ, Alt-Ergo
UNSAT Performance	Yices2	Yices2, 2019-Yices 2.6.2ⁿ, Yices2-fixedⁿ, z3ⁿ, CVC4, SMTInterpol, SMTInterpol-fixedⁿ, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT, Alt-Ergo, 2018-Yicesⁿ, 2018-CVC4ⁿ
24s Performance	Yices2	Yices2, 2019-Yices 2.6.2ⁿ, Yices2-fixedⁿ, z3ⁿ, CVC4, SMTInterpol, SMTInterpol-fixedⁿ, MathSAT5ⁿ, 2019-Par4ⁿ, veriT, OpenSMT, Alt-Ergo, 2018-Yicesⁿ, 2018-CVC4ⁿ

QF_Equality+LinearArith (QF_ALIA, QF_AUFLIA, QF_UFLIA, QF_UFLRA, QF_UFIDL)

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

QF_Equality+NonLinearArith (QF_UFNRA, QF_UFNIA, QF_ANIA, QF_AUFNIA)

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

QF_LinearIntArith (QF_LIA, QF_LIRA, QF_IDL)

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

QF_LinearRealArith (QF_LRA, QF_RDL)

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2, Yices2-fixedⁿ, CVC4, z3ⁿ, veriT, MathSAT5ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, OpenSMT, 2019-SPASS-SATTⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ
Parallel Performance	Yices2	Yices2, Yices2-fixedⁿ, CVC4, z3ⁿ, veriT, MathSAT5ⁿ, SMTInterpol-fixedⁿ, SMTInterpol, 2019-Par4ⁿ, OpenSMT, 2019-SPASS-SATTⁿ, 2019-Yices 2.6.2ⁿ
SAT Performance	Yices2	Yices2-fixedⁿ, Yices2, CVC4, z3ⁿ, veriT, SMTInterpol-fixedⁿ, MathSAT5ⁿ, SMTInterpol, 2019-Par4ⁿ, 2019-SPASS-SATTⁿ, OpenSMT, 2019-Yices 2.6.2ⁿ
UNSAT Performance	CVC4	CVC4, Yices2, Yices2-fixedⁿ, z3ⁿ, veriT, MathSAT5ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, 2019-Par4ⁿ, OpenSMT, 2019-SPASS-SATTⁿ, 2019-Yices 2.6.2ⁿ
24s Performance	Yices2	Yices2-fixedⁿ, Yices2, z3ⁿ, veriT, CVC4, MathSAT5ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, 2019-SPASS-SATTⁿ, OpenSMT, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ

QF_Equality+BVArith (QF_ABV, QF_UFBV, QF_AUFBV)

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices2	Yices2, Yices2-fixedⁿ, Bitwuzla, Bitwuzla-fixedⁿ, MathSAT5ⁿ, CVC4, z3ⁿ, 2019-Boolectorⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ
Parallel Performance	Yices2	Yices2, Yices2-fixedⁿ, Bitwuzla, Bitwuzla-fixedⁿ, MathSAT5ⁿ, CVC4, z3ⁿ, 2019-Boolectorⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ
SAT Performance	Bitwuzla	Bitwuzla-fixedⁿ, Bitwuzla, Yices2, Yices2-fixedⁿ, CVC4, MathSAT5ⁿ, z3ⁿ, 2019-Boolectorⁿ, 2019-Par4ⁿ, 2019-Yices 2.6.2ⁿ
UNSAT Performance	Yices2	Yices2, Yices2-fixedⁿ, Bitwuzla, Bitwuzla-fixedⁿ, MathSAT5ⁿ, CVC4, z3ⁿ, 2019-Par4ⁿ, 2019-Boolectorⁿ, 2019-Yices 2.6.2ⁿ
24s Performance	Bitwuzla	Bitwuzla, Bitwuzla-fixedⁿ, Yices2, Yices2-fixedⁿ, CVC4, MathSAT5ⁿ, z3ⁿ, 2019-Par4ⁿ, 2019-Boolectorⁿ, 2019-Yices 2.6.2ⁿ

QF_FPArith (QF_FP, QF_UFFP, QF_FPLRA, QF_BVFP, QF_ABVFP, QF_BVFPLRA, QF_ABVFPLRA)

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

QF_NonLinearIntArith (QF_NIA, QF_NIRA)

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2019-Par4ⁿ, CVC4, MathSAT5ⁿ, Yices2, Yices2-fixedⁿ, z3ⁿ, AProVE, SMT-RAT, 2018-SMTRAT-Ratⁿ
Parallel Performance	CVC4	2019-Par4ⁿ, CVC4, MathSAT5ⁿ, Yices2, Yices2-fixedⁿ, z3ⁿ, AProVE, SMT-RAT, 2018-SMTRAT-Ratⁿ
SAT Performance	CVC4	2019-Par4ⁿ, CVC4, MathSAT5ⁿ, z3ⁿ, Yices2, Yices2-fixedⁿ, AProVE, SMT-RAT, 2018-SMTRAT-Ratⁿ
UNSAT Performance	Yices2	2019-Par4ⁿ, Yices2, Yices2-fixedⁿ, MathSAT5ⁿ, CVC4, z3ⁿ, SMT-RAT, 2018-SMTRAT-Ratⁿ, AProVE
24s Performance	Yices2	2019-Par4ⁿ, Yices2, Yices2-fixedⁿ, MathSAT5ⁿ, z3ⁿ, CVC4, AProVE, SMT-RAT, 2018-SMTRAT-Ratⁿ

QF_NRA

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

QF_Strings (QF_S, QF_SLIA)

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, Z3str4
Parallel Performance	CVC4	CVC4, Z3str4
SAT Performance	CVC4	CVC4, Z3str4
UNSAT Performance	CVC4	CVC4, Z3str4
24s Performance	CVC4	CVC4, Z3str4

Arith (LRA, LIA, NIA, NRA)

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

Equality (UF, UFDT)

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, 2019-CVC4ⁿ, Vampire, 2018-Vampireⁿ, Alt-Ergo, veriT, veriT+viteⁿ, z3ⁿ, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT, SMTInterpol
Parallel Performance	CVC4	CVC4, 2019-CVC4ⁿ, Vampire, 2018-Vampireⁿ, Alt-Ergo, veriT, veriT+viteⁿ, z3ⁿ, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT, SMTInterpol
SAT Performance	CVC4	CVC4, Vampire, 2019-CVC4ⁿ, 2018-Vampireⁿ, z3ⁿ, SMTInterpol, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT, veriT, Alt-Ergo, veriT+viteⁿ
UNSAT Performance	CVC4	CVC4, 2019-CVC4ⁿ, Vampire, Alt-Ergo, veriT, 2018-Vampireⁿ, veriT+viteⁿ, z3ⁿ, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT, SMTInterpol
24s Performance	Vampire	Vampire, 2019-CVC4ⁿ, CVC4, Alt-Ergo, 2018-Vampireⁿ, veriT+viteⁿ, veriT, z3ⁿ, SMTInterpol-fixedⁿ, UltimateEliminator+MathSAT, SMTInterpol

Equality+LinearArith (ALIA, AUFLIA, UFLIA, UFIDL, AUFLIRA, UFLRA, UFDTLIA, UFDTLIRA, AUFDTLIA, AUFDTLIRA)

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

Equality+MachineArith (AUFFPDTLIRA, UFFPDTLIRA, UFFPDTNIRA, ABVFP, ABVFPLRA, UFBV, AUFBVDTLIA)

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

Equality+NonLinearArith (AUFDTNIRA, UFDTNIA, UFDTNIRA, AUFNIA, AUFNIRA, UFNIA)

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, 2019-Par4ⁿ, Vampire, z3ⁿ, Alt-Ergo, 2018-Vampireⁿ, UltimateEliminator+MathSAT, 2019-Vampireⁿ
Parallel Performance	CVC4	CVC4, Vampire, 2019-Par4ⁿ, z3ⁿ, Alt-Ergo, UltimateEliminator+MathSAT, 2019-Vampireⁿ, 2018-Vampireⁿ
SAT Performance	CVC4	2019-Par4ⁿ, CVC4, z3ⁿ, UltimateEliminator+MathSAT, 2019-Vampireⁿ, Alt-Ergo, Vampire, 2018-Vampireⁿ
UNSAT Performance	CVC4	CVC4, Vampire, 2018-Vampireⁿ, 2019-Par4ⁿ, z3ⁿ, Alt-Ergo, UltimateEliminator+MathSAT, 2019-Vampireⁿ
24s Performance	CVC4	CVC4, 2019-Par4ⁿ, z3ⁿ, Vampire, Alt-Ergo, 2018-Vampireⁿ, UltimateEliminator+MathSAT, 2019-Vampireⁿ

FPArith (BVFP, FP, BVFPLRA, FPLRA)

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