SMT-COMP 2019 Results - Single Query Track (Summary)

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

ABVFP

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
Parallel Performance	CVC4	2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
SAT Performance	CVC4	2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
UNSAT Performance	-	2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
24s Performance	CVC4	2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n

ALIA

Scoring Scheme	Winner	Ranking
Sequential Performance	SMTInterpol	2018-Z3n, Z3n, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	SMTInterpol	2018-Z3n, Z3n, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
SAT Performance	SMTInterpol	2018-Z3n, Z3n, SMTInterpol, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, Vampire, veriT
UNSAT Performance	Alt-Ergo	2018-Z3n, Z3n, Alt-Ergo, CVC4, SMTInterpol, Vampire, veriT, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
24s Performance	CVC4	2018-Z3n, Z3n, CVC4, Alt-Ergo, SMTInterpol, Vampire, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

AUFDTLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo, Vampire
Parallel Performance	CVC4	2018-CVC4n, CVC4, Vampire, Alt-Ergo
SAT Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo, Vampire
UNSAT Performance	CVC4	2018-CVC4n, CVC4, Vampire, Alt-Ergo
24s Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo, Vampire

AUFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2018-CVC4n, CVC4-SymBreakn, CVC4, Vampire, Z3n, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel Performance	Vampire	2018-CVC4n, Vampire, CVC4-SymBreakn, CVC4, Z3n, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT Performance	CVC4	Z3n, 2018-CVC4n, CVC4-SymBreakn, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, veriT, Alt-Ergo
UNSAT Performance	Vampire	Vampire, 2018-CVC4n, CVC4-SymBreakn, CVC4, Alt-Ergo, veriT, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s Performance	Vampire	Vampire, Z3n, 2018-CVC4n, CVC4-SymBreakn, CVC4, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

AUFLIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, Vampire, CVC4-SymBreakn, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel Performance	Par4	Par4, Z3n, 2018-Z3n, Vampire, CVC4, CVC4-SymBreakn, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT Performance	Par4	Par4, 2018-Z3n, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, CVC4, CVC4-SymBreakn, veriT, Alt-Ergo, Vampire, SMTInterpol
UNSAT Performance	Vampire	Vampire, CVC4, CVC4-SymBreakn, Par4, Z3n, 2018-Z3n, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s Performance	Par4	Par4, Z3n, 2018-Z3n, Vampire, CVC4-SymBreakn, CVC4, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

AUFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	-	CVC4-SymBreakn, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, CVC4, Z3n, Alt-Ergo, Vampire
Parallel Performance	-	CVC4-SymBreakn, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, CVC4, Vampire, Z3n
SAT Performance	-	Alt-Ergo, CVC4, CVC4-SymBreakn, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Vampire, Z3n
UNSAT Performance	-	CVC4-SymBreakn, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, CVC4, Vampire, Z3n
24s Performance	-	CVC4-SymBreakn, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, CVC4, Vampire, Z3n

AUFNIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, CVC4, 2018-CVC4n, Vampire, Z3n, Alt-Ergo, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	Par4	Par4, CVC4, 2018-CVC4n, Vampire, Z3n, Alt-Ergo, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
SAT Performance	Par4	Par4, Z3n, 2018-CVC4n, CVC4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, Vampire
UNSAT Performance	Par4	Par4, Vampire, CVC4, 2018-CVC4n, Z3n, Alt-Ergo, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s Performance	Par4	Par4, Vampire, Z3n, 2018-CVC4n, Alt-Ergo, CVC4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

BV

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, Q3B, 2018-CVC4n, CVC4, Poolector, Boolector, Z3n, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	Par4	Par4, Q3B, 2018-CVC4n, CVC4, Poolector, Boolector, Z3n, UltimateEliminator+MathSAT-5.5.4
SAT Performance	Par4	Par4, Q3B, Poolector, Boolector, Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
UNSAT Performance	Par4	Par4, CVC4, 2018-CVC4n, Q3B, Z3n, Poolector, Boolector, UltimateEliminator+MathSAT-5.5.4
24s Performance	Par4	Par4, Q3B, Poolector, Z3n, Boolector, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4

BVFP

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4	Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4
SAT Performance	CVC4	Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4
UNSAT Performance	CVC4	CVC4, 2018-CVC4n, Z3n, UltimateEliminator+MathSAT-5.5.4
24s Performance	CVC4	Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4

FP

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	CVC4	Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
SAT Performance	CVC4	Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
UNSAT Performance	CVC4	Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
24s Performance	CVC4	Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4

LIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	Z3n, 2018-Z3n, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, veriT, ProB, UltimateEliminator+Yices-2.6.1
Parallel Performance	CVC4	Z3n, 2018-Z3n, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, veriT, ProB, UltimateEliminator+Yices-2.6.1
SAT Performance	CVC4	Z3n, 2018-Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, ProB, UltimateEliminator+Yices-2.6.1, SMTInterpol, Vampire, veriT
UNSAT Performance	CVC4	Z3n, CVC4, 2018-Z3n, Vampire, SMTInterpol, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, ProB
24s Performance	CVC4	Z3n, 2018-Z3n, CVC4, Vampire, SMTInterpol, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1

LRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Z3n, Par4, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Vampire, SMTInterpol
Parallel Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Vampire, SMTInterpol
SAT Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, SMTInterpol, Vampire
UNSAT Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, Vampire, UltimateEliminator+Yices-2.6.1, SMTInterpol
24s Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, SMTInterpol, Vampire

NIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire
Parallel Performance	CVC4	2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire
SAT Performance	CVC4	2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire
UNSAT Performance	CVC4	2018-Z3n, CVC4, Z3n, Vampire, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, ProB
24s Performance	CVC4	2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire

NRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, Vampire, 2018-Z3n, Z3n, 2018-Vampiren, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel Performance	Par4	Par4, Vampire, 2018-Z3n, Z3n, 2018-Vampiren, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT Performance	Par4	Z3n, 2018-Z3n, Par4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, 2018-Vampiren, CVC4, Vampire
UNSAT Performance	Par4	Par4, Vampire, 2018-Z3n, Z3n, 2018-Vampiren, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s Performance	Par4	Par4, Z3n, 2018-Z3n, Vampire, CVC4, 2018-Vampiren, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

QF_ABV

Scoring Scheme	Winner	Ranking
Sequential Performance	Boolector	Boolector, Par4, 2018-Boolectorn, Yices 2.6.2, Poolector, CVC4, Z3n
Parallel Performance	Par4	Par4, Poolector, Boolector, 2018-Boolectorn, Yices 2.6.2, CVC4, Z3n
SAT Performance	Poolector	Poolector, Boolector, Par4, Yices 2.6.2, 2018-Boolectorn, CVC4, Z3n
UNSAT Performance	Par4	Par4, Boolector, 2018-Boolectorn, Poolector, Yices 2.6.2, Z3n, CVC4
24s Performance	Par4	Par4, Poolector, Boolector, Yices 2.6.2, 2018-Boolectorn, CVC4, Z3n

QF_ALIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, SMTInterpol, CVC4, Z3n, Alt-Ergo, veriT
Parallel Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, SMTInterpol, CVC4, Z3n, Alt-Ergo, veriT
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, SMTInterpol, CVC4, Z3n, veriT, Alt-Ergo
UNSAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT
24s Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, SMTInterpol, Z3n, CVC4, Alt-Ergo, veriT

QF_ANIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, MathSAT-na-ext, MathSAT-default, 2018-Z3n, Z3n, Alt-Ergo
Parallel Performance	CVC4	CVC4, MathSAT-na-ext, MathSAT-default, 2018-Z3n, Z3n, Alt-Ergo
SAT Performance	-	2018-Z3n, Alt-Ergo, CVC4, MathSAT-default, MathSAT-na-ext, Z3n
UNSAT Performance	CVC4	CVC4, MathSAT-na-ext, MathSAT-default, 2018-Z3n, Z3n, Alt-Ergo
24s Performance	MathSAT-na-ext	2018-Z3n, Z3n, MathSAT-na-ext, MathSAT-default, CVC4, Alt-Ergo

QF_AUFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, Z3n, Boolector, Poolector, 2018-CVC4n, CVC4
Parallel Performance	Yices 2.6.2	Yices 2.6.2, Z3n, Boolector, Poolector, 2018-CVC4n, CVC4
SAT Performance	Yices 2.6.2	Yices 2.6.2, Boolector, Poolector, Z3n, 2018-CVC4n, CVC4
UNSAT Performance	Yices 2.6.2	Z3n, Yices 2.6.2, Boolector, Poolector, 2018-CVC4n, CVC4
24s Performance	Yices 2.6.2	Yices 2.6.2, Boolector, Poolector, CVC4, 2018-CVC4n, Z3n

QF_AUFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, Alt-Ergo, veriT
Parallel Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
UNSAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT
24s Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT

QF_AUFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, 2018-Z3n, CVC4, Z3n, Alt-Ergo
Parallel Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, 2018-Z3n, CVC4, Z3n, Alt-Ergo
SAT Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, CVC4, 2018-Z3n, Z3n, Alt-Ergo
UNSAT Performance	MathSAT-na-ext	2018-Z3n, Z3n, MathSAT-na-ext, MathSAT-default, CVC4, Alt-Ergo
24s Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, 2018-Z3n, CVC4, Z3n, Alt-Ergo

QF_AX

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, Alt-Ergo
Parallel Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, Alt-Ergo
SAT Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, CVC4, Z3n, SMTInterpol, Alt-Ergo
UNSAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, Alt-Ergo
24s Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, Alt-Ergo

QF_BV

Scoring Scheme	Winner	Ranking
Sequential Performance	Boolector	Boolector, Yices 2.6.2 CaDiCal, Poolector, Par4, Yices 2.6.2 New Bvsolver, Minkeyrink Solver, 2018-Boolectorn, Yices 2.6.2 Cryptominisat, CVC4, Minkeyrink Solver MT, 2018-Minkeyrink MTn, Boolector-ReasonLSn, Yices 2.6.2, STP-incremental, STP, STP-mergesat-fixedn, STP-mt, STP-minisat, Z3n, STP-portfolio-fixedn, Yices 2.6.2 mcsat-bv, STP-riss, STP-mergesat, STP-portfolio
Parallel Performance	Poolector	Poolector, Boolector, Par4, Yices 2.6.2 CaDiCal, Yices 2.6.2 New Bvsolver, Minkeyrink Solver MT, Minkeyrink Solver, 2018-Minkeyrink MTn, 2018-Boolectorn, Yices 2.6.2 Cryptominisat, CVC4, Boolector-ReasonLSn, Yices 2.6.2, STP-mt, STP-incremental, STP, STP-mergesat-fixedn, STP-minisat, Z3n, STP-portfolio-fixedn, Yices 2.6.2 mcsat-bv, STP-riss, STP-mergesat, STP-portfolio
SAT Performance	Poolector	Poolector, Boolector, Par4, CVC4, Yices 2.6.2 CaDiCal, Minkeyrink Solver MT, Minkeyrink Solver, Yices 2.6.2, Yices 2.6.2 New Bvsolver, 2018-Minkeyrink MTn, 2018-Boolectorn, Yices 2.6.2 Cryptominisat, STP-mt, STP-incremental, STP, STP-mergesat-fixedn, Boolector-ReasonLSn, STP-minisat, STP-portfolio-fixedn, Z3n, Yices 2.6.2 mcsat-bv, STP-mergesat, STP-riss, STP-portfolio
UNSAT Performance	Poolector	Poolector, Boolector, Par4, Yices 2.6.2 CaDiCal, Yices 2.6.2 New Bvsolver, 2018-Boolectorn, Yices 2.6.2 Cryptominisat, Minkeyrink Solver MT, Minkeyrink Solver, 2018-Minkeyrink MTn, Boolector-ReasonLSn, CVC4, STP-mt, STP-incremental, STP, Yices 2.6.2, STP-mergesat-fixedn, STP-minisat, Z3n, STP-portfolio-fixedn, Yices 2.6.2 mcsat-bv, STP-riss, STP-mergesat, STP-portfolio
24s Performance	Par4	Par4, Poolector, Yices 2.6.2 New Bvsolver, Boolector, Yices 2.6.2 CaDiCal, Minkeyrink Solver MT, 2018-Minkeyrink MTn, Minkeyrink Solver, 2018-Boolectorn, Yices 2.6.2, Yices 2.6.2 Cryptominisat, CVC4, STP-mt, Boolector-ReasonLSn, STP, STP-incremental, STP-minisat, STP-mergesat-fixedn, STP-portfolio-fixedn, Z3n, Yices 2.6.2 mcsat-bv, STP-riss, STP-mergesat, STP-portfolio

QF_BVFP

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, 2018-CVC4n, CVC4, Z3n
Parallel Performance	Par4	Par4, 2018-CVC4n, CVC4, Z3n
SAT Performance	Par4	Par4, 2018-CVC4n, CVC4, Z3n
UNSAT Performance	Par4	Par4, CVC4, 2018-CVC4n, Z3n
24s Performance	Par4	Par4, CVC4, 2018-CVC4n, Z3n

QF_DT

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo
Parallel Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo
SAT Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo
UNSAT Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo
24s Performance	CVC4	2018-CVC4n, CVC4, Alt-Ergo

QF_FP

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, COLIBRI, CVC4, 2018-COLIBRIn, Z3n
Parallel Performance	Par4	Par4, COLIBRI, CVC4, 2018-COLIBRIn, Z3n
SAT Performance	Par4	Par4, CVC4, COLIBRI, 2018-COLIBRIn, Z3n
UNSAT Performance	Par4	Par4, COLIBRI, 2018-COLIBRIn, CVC4, Z3n
24s Performance	COLIBRI	COLIBRI, Par4, 2018-COLIBRIn, CVC4, Z3n

QF_IDL

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Z3n, 2018-Yicesn, Yices 2.6.2, Par4, CVC4, veriT, SMTInterpol, ProB
Parallel Performance	Par4	Par4, Z3n, 2018-Yicesn, Yices 2.6.2, CVC4, veriT, SMTInterpol, ProB
SAT Performance	Par4	Par4, Z3n, 2018-Yicesn, Yices 2.6.2, CVC4, veriT, SMTInterpol, ProB
UNSAT Performance	Par4	Z3n, Par4, CVC4, 2018-Yicesn, Yices 2.6.2, veriT, SMTInterpol, ProB
24s Performance	Par4	Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, veriT, SMTInterpol, ProB

QF_LIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, SPASS-SATT, 2018-SPASS-SATTn, Z3n, CVC4, Ctrl-Ergo, Yices 2.6.2, SMTInterpol, CVC4-SymBreakn, veriT, ProB
Parallel Performance	Par4	Par4, SPASS-SATT, 2018-SPASS-SATTn, Z3n, CVC4, Ctrl-Ergo, Yices 2.6.2, SMTInterpol, CVC4-SymBreakn, veriT, ProB
SAT Performance	Par4	Par4, 2018-SPASS-SATTn, SPASS-SATT, Z3n, CVC4, Ctrl-Ergo, Yices 2.6.2, SMTInterpol, CVC4-SymBreakn, veriT, ProB
UNSAT Performance	Par4	Par4, SPASS-SATT, SMTInterpol, 2018-SPASS-SATTn, Ctrl-Ergo, CVC4, CVC4-SymBreakn, Z3n, Yices 2.6.2, veriT, ProB
24s Performance	Par4	Par4, SPASS-SATT, Yices 2.6.2, 2018-SPASS-SATTn, Z3n, Ctrl-Ergo, CVC4, SMTInterpol, CVC4-SymBreakn, veriT, ProB

QF_LIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, 2018-Z3n, Yices 2.6.2, Z3n, CVC4, SMTInterpol
Parallel Performance	Par4	Par4, 2018-Z3n, Yices 2.6.2, Z3n, CVC4, SMTInterpol
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Z3n, Par4, Z3n, CVC4, SMTInterpol
UNSAT Performance	Par4	Par4, 2018-Z3n, Yices 2.6.2, Z3n, CVC4, SMTInterpol
24s Performance	Yices 2.6.2	Yices 2.6.2, 2018-Z3n, Par4, Z3n, CVC4, SMTInterpol

QF_LRA

Scoring Scheme	Winner	Ranking
Sequential Performance	SPASS-SATT	SPASS-SATT, 2018-CVC4n, Par4, Yices 2.6.2, CVC4, CVC4-SymBreakn, veriT, SMTInterpol, Z3n, OpenSMT2, Ctrl-Ergo
Parallel Performance	Par4	Par4, SPASS-SATT, 2018-CVC4n, Yices 2.6.2, CVC4, CVC4-SymBreakn, veriT, SMTInterpol, Z3n, Ctrl-Ergo, OpenSMT2
SAT Performance	Par4	Par4, SPASS-SATT, 2018-CVC4n, Yices 2.6.2, CVC4, CVC4-SymBreakn, SMTInterpol, veriT, Ctrl-Ergo, Z3n, OpenSMT2
UNSAT Performance	Par4	Par4, SPASS-SATT, 2018-CVC4n, CVC4, Yices 2.6.2, veriT, CVC4-SymBreakn, OpenSMT2, Z3n, SMTInterpol, Ctrl-Ergo
24s Performance	Yices 2.6.2	Yices 2.6.2, Par4, SPASS-SATT, CVC4, veriT, 2018-CVC4n, Z3n, OpenSMT2, SMTInterpol, Ctrl-Ergo, CVC4-SymBreakn

QF_NIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, CVC4, CVC4-SymBreakn, Yices 2.6.2, 2018-CVC4n, Z3n, AProVE, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext
Parallel Performance	Par4	Par4, CVC4, CVC4-SymBreakn, Yices 2.6.2, 2018-CVC4n, Z3n, AProVE, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext
SAT Performance	Par4	Par4, CVC4, CVC4-SymBreakn, Yices 2.6.2, 2018-CVC4n, AProVE, Z3n, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext
UNSAT Performance	Par4	Par4, MathSAT-default, Yices 2.6.2, MathSAT-na-ext, CVC4, CVC4-SymBreakn, 2018-CVC4n, Z3n, SMT-RAT, ProB, AProVE
24s Performance	Par4	Par4, Yices 2.6.2, CVC4, 2018-CVC4n, CVC4-SymBreakn, Z3n, AProVE, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext

QF_NIRA

Scoring Scheme	Winner	Ranking
Sequential Performance	SMT-RAT	2018-SMTRAT-Ratn, SMT-RAT, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Yices 2.6.2
Parallel Performance	SMT-RAT	2018-SMTRAT-Ratn, SMT-RAT, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Yices 2.6.2
SAT Performance	-	2018-SMTRAT-Ratn, CVC4, MathSAT-default, MathSAT-na-ext, SMT-RAT, Yices 2.6.2, Z3n
UNSAT Performance	SMT-RAT	2018-SMTRAT-Ratn, SMT-RAT, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Yices 2.6.2
24s Performance	-	Z3n, 2018-SMTRAT-Ratn, CVC4, MathSAT-default, MathSAT-na-ext, SMT-RAT, Yices 2.6.2

QF_NRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, Yices 2.6.2, Z3n, 2018-Z3n, SMTRAT-MCSAT, veriT+raSAT+Redlog, CVC4, CVC4-SymBreakn, MathSAT-default, SMT-RAT, MathSAT-na-ext
Parallel Performance	Par4	Par4, Yices 2.6.2, Z3n, 2018-Z3n, SMTRAT-MCSAT, veriT+raSAT+Redlog, CVC4, CVC4-SymBreakn, MathSAT-default, SMT-RAT, MathSAT-na-ext
SAT Performance	Par4	Par4, Z3n, Yices 2.6.2, 2018-Z3n, SMTRAT-MCSAT, veriT+raSAT+Redlog, SMT-RAT, CVC4, MathSAT-default, CVC4-SymBreakn, MathSAT-na-ext
UNSAT Performance	Par4	Par4, CVC4, CVC4-SymBreakn, MathSAT-default, MathSAT-na-ext, Yices 2.6.2, Z3n, veriT+raSAT+Redlog, 2018-Z3n, SMTRAT-MCSAT, SMT-RAT
24s Performance	Par4	Par4, Z3n, 2018-Z3n, Yices 2.6.2, veriT+raSAT+Redlog, SMTRAT-MCSAT, SMT-RAT, MathSAT-default, MathSAT-na-ext, CVC4, CVC4-SymBreakn

QF_RDL

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, CVC4, veriT, Z3n, SMTInterpol
Parallel Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, CVC4, veriT, Z3n, SMTInterpol
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, veriT, CVC4, Z3n, SMTInterpol
UNSAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, CVC4, Z3n, veriT, SMTInterpol
24s Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, veriT, SMTInterpol

QF_S

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring Scheme	Ranking
Sequential Performance	CVC4
Parallel Performance	CVC4
SAT Performance	CVC4
UNSAT Performance	CVC4
24s Performance	CVC4

QF_SLIA

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring Scheme	Ranking
Sequential Performance	CVC4, 2018-CVC4n
Parallel Performance	CVC4, 2018-CVC4n
SAT Performance	CVC4, 2018-CVC4n
UNSAT Performance	CVC4, 2018-CVC4n
24s Performance	CVC4, 2018-CVC4n

QF_UF

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Par4, veriT, CVC4, OpenSMT2, Z3n, SMTInterpol, Alt-Ergo
Parallel Performance	Par4	Par4, Yices 2.6.2, 2018-Yicesn, veriT, CVC4, OpenSMT2, Z3n, SMTInterpol, Alt-Ergo
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Par4, veriT, Z3n, SMTInterpol, CVC4, OpenSMT2, Alt-Ergo
UNSAT Performance	Par4	Par4, Yices 2.6.2, 2018-Yicesn, veriT, OpenSMT2, CVC4, Z3n, SMTInterpol, Alt-Ergo
24s Performance	Par4	Par4, Yices 2.6.2, 2018-Yicesn, veriT, OpenSMT2, CVC4, Z3n, SMTInterpol, Alt-Ergo

QF_UFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, Boolector, 2018-Boolectorn, CVC4, Poolector, Z3n
Parallel Performance	Yices 2.6.2	Yices 2.6.2, Poolector, Boolector, 2018-Boolectorn, CVC4, Z3n
SAT Performance	Yices 2.6.2	Yices 2.6.2, Poolector, Boolector, 2018-Boolectorn, Z3n, CVC4
UNSAT Performance	Yices 2.6.2	Yices 2.6.2, Poolector, Boolector, 2018-Boolectorn, CVC4, Z3n
24s Performance	Yices 2.6.2	2018-Boolectorn, Yices 2.6.2, Boolector, Poolector, CVC4, Z3n

QF_UFIDL

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4
Parallel Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, SMTInterpol
UNSAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4
24s Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4

QF_UFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
Parallel Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
SAT Performance	Yices 2.6.2	Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
UNSAT Performance	Yices 2.6.2	Z3n, 2018-Yicesn, Yices 2.6.2, SMTInterpol, CVC4, veriT, Alt-Ergo
24s Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo

QF_UFLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	SMTInterpol	SMTInterpol, Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, Alt-Ergo
Parallel Performance	SMTInterpol	SMTInterpol, Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, Alt-Ergo
SAT Performance	SMTInterpol	SMTInterpol, Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, Alt-Ergo
UNSAT Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, Z3n, veriT, CVC4, SMTInterpol, Alt-Ergo
24s Performance	Yices 2.6.2	2018-Yicesn, Yices 2.6.2, veriT, Z3n, CVC4, SMTInterpol, Alt-Ergo

QF_UFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, MathSAT-default, 2018-Yicesn, Yices 2.6.2, Z3n, MathSAT-na-ext, Alt-Ergo
Parallel Performance	CVC4	CVC4, MathSAT-default, 2018-Yicesn, Yices 2.6.2, Z3n, MathSAT-na-ext, Alt-Ergo
SAT Performance	CVC4	CVC4, 2018-Yicesn, Yices 2.6.2, MathSAT-default, Z3n, MathSAT-na-ext, Alt-Ergo
UNSAT Performance	CVC4	CVC4, Z3n, MathSAT-default, MathSAT-na-ext, 2018-Yicesn, Yices 2.6.2, Alt-Ergo
24s Performance	CVC4	CVC4, 2018-Yicesn, Yices 2.6.2, MathSAT-default, Z3n, MathSAT-na-ext, Alt-Ergo

QF_UFNRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, veriT+raSAT+Redlog, Alt-Ergo
Parallel Performance	Par4	Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Alt-Ergo, veriT+raSAT+Redlog
SAT Performance	Par4	Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Alt-Ergo, veriT+raSAT+Redlog
UNSAT Performance	MathSAT-default	MathSAT-default, MathSAT-na-ext, Z3n, Par4, 2018-Yicesn, Yices 2.6.2, CVC4, Alt-Ergo, veriT+raSAT+Redlog
24s Performance	Par4	Z3n, Par4, MathSAT-default, MathSAT-na-ext, 2018-Yicesn, Yices 2.6.2, CVC4, Alt-Ergo, veriT+raSAT+Redlog

UF

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, 2018-CVC4n, Par4, Vampire, 2018-Vampiren, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1
Parallel Performance	Vampire	2018-Vampiren, Vampire, Par4, CVC4, 2018-CVC4n, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1
SAT Performance	Vampire	2018-Vampiren, Vampire, CVC4, 2018-CVC4n, Par4, Z3n, SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, Alt-Ergo, veriT
UNSAT Performance	Par4	Par4, CVC4, 2018-CVC4n, 2018-Vampiren, Vampire, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s Performance	Vampire	2018-Vampiren, Vampire, Par4, CVC4, 2018-CVC4n, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

UFBV

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	2018-Z3n, Par4, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	Par4	Par4, 2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4
SAT Performance	Par4	Par4, 2018-Z3n, Z3n, UltimateEliminator+MathSAT-5.5.4, CVC4
UNSAT Performance	Par4	Par4, 2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4
24s Performance	Par4	Par4, 2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4

UFDT

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
Parallel Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
SAT Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
UNSAT Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
24s Performance	Alt-Ergo	Alt-Ergo, 2018-CVC4n, CVC4, Vampire

UFDTLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
Parallel Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
SAT Performance	-	2018-CVC4n, Alt-Ergo, CVC4, Vampire
UNSAT Performance	CVC4	CVC4, 2018-CVC4n, Vampire, Alt-Ergo
24s Performance	Vampire	Vampire, Alt-Ergo, CVC4, 2018-CVC4n

UFDTNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Vampire	Vampire, CVC4, Alt-Ergo
Parallel Performance	Vampire	Vampire, CVC4, Alt-Ergo
SAT Performance	-	Alt-Ergo, CVC4, Vampire
UNSAT Performance	Vampire	Vampire, CVC4, Alt-Ergo
24s Performance	Vampire	Vampire, CVC4, Alt-Ergo

UFIDL

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, veriT, SMTInterpol, Vampire, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel Performance	Par4	Par4, Z3n, 2018-Z3n, CVC4, veriT, SMTInterpol, Vampire, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
SAT Performance	Par4	Par4, 2018-Z3n, Z3n, CVC4, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, veriT, Vampire
UNSAT Performance	Par4	Par4, 2018-Z3n, Z3n, CVC4, veriT, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s Performance	Par4	Par4, 2018-Z3n, Z3n, CVC4, veriT, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

UFLIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, CVC4, 2018-CVC4n, veriT, Vampire, Z3n, Alt-Ergo, SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4
Parallel Performance	Par4	Par4, CVC4, 2018-CVC4n, veriT, Vampire, Z3n, Alt-Ergo, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT Performance	Par4	Par4, Z3n, SMTInterpol, 2018-CVC4n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, veriT, Vampire
UNSAT Performance	Par4	Par4, CVC4, 2018-CVC4n, veriT, Vampire, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s Performance	Par4	Par4, 2018-CVC4n, CVC4, veriT, Z3n, Alt-Ergo, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFLRA

Scoring Scheme	Winner	Ranking
Sequential Performance	Alt-Ergo	2018-Z3n, Z3n, Alt-Ergo, veriT, Vampire, CVC4, SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel Performance	Alt-Ergo	2018-Z3n, Z3n, Alt-Ergo, veriT, Vampire, CVC4, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
SAT Performance	-	2018-Z3n, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, SMTInterpol, veriT, Vampire, CVC4
UNSAT Performance	veriT	veriT, CVC4, Alt-Ergo, 2018-Z3n, Z3n, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s Performance	Alt-Ergo	Z3n, 2018-Z3n, Alt-Ergo, veriT, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFNIA

Scoring Scheme	Winner	Ranking
Sequential Performance	Par4	Par4, CVC4-SymBreakn, CVC4, Z3n, 2018-Z3n, Vampire, 2018-Vampiren, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel Performance	Par4	2018-Vampiren, Par4, CVC4-SymBreakn, CVC4, Vampire, Z3n, 2018-Z3n, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT Performance	Par4	Par4, CVC4, CVC4-SymBreakn, Z3n, 2018-Z3n, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Alt-Ergo, 2018-Vampiren, Vampire
UNSAT Performance	Par4	2018-Vampiren, Par4, CVC4-SymBreakn, CVC4, Vampire, Z3n, 2018-Z3n, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s Performance	Par4	Par4, CVC4, CVC4-SymBreakn, Z3n, 2018-Z3n, 2018-Vampiren, Vampire, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1