SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

SMT-COMP 2020 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 SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, 2018-CVC4n, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, 2018-CVC4n, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, 2018-CVC4n, UltimateEliminator+MathSAT
UNSAT PerformanceCVC42018-CVC4n, CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, 2018-CVC4n, UltimateEliminator+MathSAT

ABVFPLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

ALIA

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpol2018-Z3n, z3n, SMTInterpol-fixedn, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT, veriT+viten, UltimateEliminator+MathSAT
Parallel PerformanceSMTInterpol2018-Z3n, z3n, SMTInterpol-fixedn, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT, veriT+viten, UltimateEliminator+MathSAT
SAT PerformanceSMTInterpolz3n, 2018-Z3n, SMTInterpol, SMTInterpol-fixedn, CVC4, Alt-Ergo, UltimateEliminator+MathSAT, veriT, veriT+viten, Vampire
UNSAT PerformanceCVC42018-Z3n, z3n, CVC4, Alt-Ergo, SMTInterpol-fixedn, SMTInterpol, Vampire, veriT+viten, veriT, UltimateEliminator+MathSAT
24s PerformanceSMTInterpol2018-Z3n, z3n, SMTInterpol-fixedn, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT+viten, veriT, UltimateEliminator+MathSAT

AUFBVDTLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

AUFDTLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42018-CVC4n, CVC4, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
Parallel PerformanceCVC42018-CVC4n, CVC4, Alt-Ergo, Vampire, UltimateEliminator+MathSAT
SAT PerformanceCVC42018-CVC4n, CVC4, UltimateEliminator+MathSAT, Alt-Ergo, Vampire
UNSAT PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo, UltimateEliminator+MathSAT

AUFDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Alt-Ergo, Vampire, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
SAT Performance-Alt-Ergo, Vampire, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, Alt-Ergo, Vampire, UltimateEliminator+MathSAT

AUFDTNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceVampireVampire, Alt-Ergo, CVC4, UltimateEliminator+MathSAT
Parallel PerformanceVampireVampire, Alt-Ergo, CVC4, UltimateEliminator+MathSAT
SAT Performance-Alt-Ergo, Vampire, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceVampireVampire, Alt-Ergo, CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, Alt-Ergo, Vampire, UltimateEliminator+MathSAT

AUFFPDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT Performance-CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceVampire2018-CVC4n, Vampire, CVC4, z3n, veriT, Alt-Ergo, veriT+viten, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT
Parallel PerformanceVampireVampire, 2018-CVC4n, CVC4, z3n, veriT, Alt-Ergo, veriT+viten, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT
SAT PerformanceCVC4z3n, 2018-CVC4n, CVC4, Vampire, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT, veriT+viten, Alt-Ergo, veriT
UNSAT PerformanceVampireVampire, 2018-CVC4n, CVC4, veriT, Alt-Ergo, veriT+viten, z3n, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT
24s PerformanceVampireVampire, z3n, 2018-CVC4n, CVC4, veriT+viten, Alt-Ergo, veriT, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT

AUFLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, CVC4, z3n, Vampire, Alt-Ergo, veriT, veriT+viten, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT
Parallel PerformanceVampire2019-Par4n, Vampire, CVC4, z3n, Alt-Ergo, veriT, veriT+viten, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
SAT Performance-2019-Par4n, UltimateEliminator+MathSAT, z3n, SMTInterpol-fixedn, Alt-Ergo, SMTInterpol, CVC4, veriT, veriT+viten, Vampire
UNSAT PerformanceVampireVampire, CVC4, 2019-Par4n, z3n, Alt-Ergo, veriT, veriT+viten, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
24s PerformanceVampire2019-Par4n, z3n, Vampire, CVC4, Alt-Ergo, veriT+viten, veriT, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT

AUFNIA

Scoring SchemeWinnerRanking
Sequential Performance-UltimateEliminator+MathSAT, CVC4, z3n, Alt-Ergo, Vampire
Parallel Performance-UltimateEliminator+MathSAT, Alt-Ergo, Vampire, CVC4, z3n
SAT Performance-Alt-Ergo, Vampire, CVC4, z3n, UltimateEliminator+MathSAT
UNSAT Performance-UltimateEliminator+MathSAT, Alt-Ergo, Vampire, CVC4, z3n
24s Performance-UltimateEliminator+MathSAT, Alt-Ergo, Vampire, CVC4, z3n

AUFNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Vampire, 2019-Par4n, Alt-Ergo, z3n, UltimateEliminator+MathSAT
Parallel PerformanceVampireVampire, CVC4, 2019-Par4n, Alt-Ergo, z3n, UltimateEliminator+MathSAT
SAT Performance-z3n, 2019-Par4n, UltimateEliminator+MathSAT, CVC4, Alt-Ergo, Vampire
UNSAT PerformanceVampireVampire, CVC4, 2019-Par4n, Alt-Ergo, z3n, UltimateEliminator+MathSAT
24s PerformanceVampireVampire, 2019-Par4n, CVC4, z3n, Alt-Ergo, UltimateEliminator+MathSAT

BV

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, CVC4, Bitwuzla-fixedn, z3n, UltimateEliminator+MathSAT, Bitwuzla
Parallel PerformanceCVC42019-Par4n, CVC4, Bitwuzla-fixedn, z3n, UltimateEliminator+MathSAT, Bitwuzla
SAT PerformanceCVC42019-Par4n, Bitwuzla-fixedn, z3n, CVC4, UltimateEliminator+MathSAT, Bitwuzla
UNSAT PerformanceCVC42019-Par4n, CVC4, Bitwuzla-fixedn, z3n, UltimateEliminator+MathSAT, Bitwuzla
24s PerformanceCVC42019-Par4n, Bitwuzla-fixedn, z3n, CVC4, UltimateEliminator+MathSAT, Bitwuzla

BVFP

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Z3n, CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-Z3n, CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC42019-Z3n, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC42019-Z3n, CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC42019-Z3n, CVC4, UltimateEliminator+MathSAT

BVFPLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

FP

The division has disagreements

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Z3n, z3n, CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-Z3n, z3n, CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC42019-Z3n, z3n, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC42019-Z3n, z3n, CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT

FPLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
UNSAT Performance-CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

LIA

The division has disagreements

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol-fixedn, SMTInterpol, veriT, veriT+viten
Parallel PerformanceCVC4z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol-fixedn, SMTInterpol, veriT, veriT+viten
SAT PerformanceCVC4z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, SMTInterpol-fixedn, SMTInterpol, Vampire, veriT, veriT+viten
UNSAT PerformanceCVC4z3n, 2019-Z3n, CVC4, Vampire, UltimateEliminator+MathSAT, SMTInterpol-fixedn, SMTInterpol, veriT, veriT+viten
24s PerformanceCVC4z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol-fixedn, SMTInterpol, veriT+viten, veriT

LRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceCVC42019-Par4n, z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol, SMTInterpol-fixedn
SAT PerformanceCVC42019-Par4n, 2019-Z3n, z3n, CVC4, UltimateEliminator+MathSAT, SMTInterpol, SMTInterpol-fixedn, Vampire
UNSAT PerformanceCVC42019-Par4n, z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol-fixedn, SMTInterpol
24s PerformanceCVC42019-Par4n, z3n, 2019-Z3n, CVC4, UltimateEliminator+MathSAT, Vampire, SMTInterpol-fixedn, SMTInterpol

NIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42018-Z3n, z3n, CVC4, UltimateEliminator+MathSAT, Vampire
Parallel PerformanceCVC42018-Z3n, z3n, CVC4, UltimateEliminator+MathSAT, Vampire
SAT PerformanceCVC42018-Z3n, z3n, CVC4, UltimateEliminator+MathSAT, Vampire
UNSAT PerformanceVampire2018-Z3n, Vampire, z3n, UltimateEliminator+MathSAT, CVC4
24s PerformanceCVC42018-Z3n, z3n, CVC4, UltimateEliminator+MathSAT, Vampire

NRA

Scoring SchemeWinnerRanking
Sequential PerformanceVampirez3n, 2019-Par4n, Vampire, CVC4, UltimateEliminator+MathSAT
Parallel PerformanceVampirez3n, 2019-Par4n, Vampire, CVC4, UltimateEliminator+MathSAT
SAT Performance-z3n, 2019-Par4n, UltimateEliminator+MathSAT, Vampire, CVC4
UNSAT PerformanceVampirez3n, 2019-Par4n, Vampire, CVC4, UltimateEliminator+MathSAT
24s PerformanceVampirez3n, 2019-Par4n, Vampire, CVC4, UltimateEliminator+MathSAT

QF_ABV

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, 2019-Boolectorn, 2019-Par4n, Yices2, Yices2-fixedn, MathSAT5n, CVC4, z3n
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, 2019-Boolectorn, 2019-Par4n, Yices2, Yices2-fixedn, MathSAT5n, CVC4, z3n
SAT PerformanceBitwuzla2019-Boolectorn, Bitwuzla-fixedn, Bitwuzla, 2019-Par4n, Yices2, Yices2-fixedn, CVC4, MathSAT5n, z3n
UNSAT PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, 2019-Par4n, 2019-Boolectorn, Yices2-fixedn, Yices2, MathSAT5n, CVC4, z3n
24s PerformanceBitwuzla2019-Par4n, Bitwuzla, Bitwuzla-fixedn, 2019-Boolectorn, Yices2-fixedn, Yices2, CVC4, z3n, MathSAT5n

QF_ABVFP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4, COLIBRI
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4, COLIBRI
SAT PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4, COLIBRI
UNSAT PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4, COLIBRI
24s PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, MathSAT5n, CVC4, COLIBRI

QF_ABVFPLRA

The division has disagreements

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, COLIBRI, MathSAT5n
Parallel PerformanceCVC4CVC4, COLIBRI, MathSAT5n
SAT PerformanceCVC4CVC4, COLIBRI, MathSAT5n
UNSAT PerformanceCVC4CVC4, COLIBRI, MathSAT5n
24s PerformanceCOLIBRICOLIBRI, CVC4, MathSAT5n

QF_ALIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, MathSAT5n, z3n, SMTInterpol, SMTInterpol-fixedn, CVC4, Alt-Ergo, veriT
Parallel PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, MathSAT5n, SMTInterpol, SMTInterpol-fixedn, z3n, CVC4, Alt-Ergo, veriT
SAT PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, MathSAT5n, SMTInterpol, SMTInterpol-fixedn, z3n, CVC4, veriT, Alt-Ergo
UNSAT PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, MathSAT5n, z3n, SMTInterpol, SMTInterpol-fixedn, CVC4, Alt-Ergo, veriT
24s PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, MathSAT5n, SMTInterpol, SMTInterpol-fixedn, z3n, CVC4, Alt-Ergo, veriT

QF_ANIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-CVC4n, CVC4, MathSAT5n, z3n, Alt-Ergo
Parallel PerformanceCVC42019-CVC4n, CVC4, MathSAT5n, z3n, Alt-Ergo
SAT PerformanceCVC42019-CVC4n, CVC4, MathSAT5n, z3n, Alt-Ergo
UNSAT PerformanceCVC4MathSAT5n, z3n, CVC4, 2019-CVC4n, Alt-Ergo
24s PerformanceCVC4MathSAT5n, 2019-CVC4n, CVC4, z3n, Alt-Ergo

QF_AUFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2-fixedn, 2019-Yices 2.6.2n, Yices2, z3n, MathSAT5n, Bitwuzla, Bitwuzla-fixedn, CVC4
Parallel PerformanceYices2Yices2-fixedn, 2019-Yices 2.6.2n, Yices2, z3n, MathSAT5n, Bitwuzla, Bitwuzla-fixedn, CVC4
SAT PerformanceYices2Yices2-fixedn, 2019-Yices 2.6.2n, Yices2, Bitwuzla, Bitwuzla-fixedn, z3n, MathSAT5n, CVC4
UNSAT PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, z3n, MathSAT5n, Bitwuzla, Bitwuzla-fixedn, CVC4
24s PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, z3n, MathSAT5n, Bitwuzla, Bitwuzla-fixedn, CVC4

QF_AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, z3n, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn, Alt-Ergo, veriT
Parallel PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, z3n, MathSAT5n, CVC4, SMTInterpol-fixedn, SMTInterpol, Alt-Ergo, veriT
SAT PerformanceYices2Yices2, 2019-Yices 2.6.2n, Yices2-fixedn, z3n, MathSAT5n, CVC4, SMTInterpol-fixedn, SMTInterpol, veriT, Alt-Ergo
UNSAT PerformanceYices22019-Yices 2.6.2n, z3n, Yices2, Yices2-fixedn, CVC4, MathSAT5n, SMTInterpol-fixedn, SMTInterpol, Alt-Ergo, veriT
24s PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, z3n, MathSAT5n, CVC4, SMTInterpol-fixedn, SMTInterpol, Alt-Ergo, veriT

QF_AUFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-MathSAT-defaultn, MathSAT5n, z3n, CVC4, Alt-Ergo
Parallel PerformanceCVC42019-MathSAT-defaultn, MathSAT5n, z3n, CVC4, Alt-Ergo
SAT PerformanceCVC42019-MathSAT-defaultn, MathSAT5n, CVC4, z3n, Alt-Ergo
UNSAT PerformanceCVC4z3n, 2019-MathSAT-defaultn, MathSAT5n, CVC4, Alt-Ergo
24s PerformanceCVC42019-MathSAT-defaultn, MathSAT5n, z3n, CVC4, Alt-Ergo

QF_AX

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2-fixedn, Yices2, 2019-Yices 2.6.2n, 2018-Yicesn, MathSAT5n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, Alt-Ergo
Parallel PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, 2018-Yicesn, MathSAT5n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, Alt-Ergo
SAT PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, 2018-Yicesn, MathSAT5n, z3n, CVC4, SMTInterpol-fixedn, SMTInterpol, Alt-Ergo
UNSAT PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, 2018-Yicesn, MathSAT5n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, Alt-Ergo
24s PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, 2018-Yicesn, MathSAT5n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, Alt-Ergo

QF_BV

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, Yices2-fixedn, 2019-Boolectorn, 2019-Poolectorn, MinkeyRink-fixedn, STP + CMS, CVC4, MathSAT5n, z3n, LazyBV2Int, MinkeyRink, STP + MergeSAT, Yices2
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, 2019-Poolectorn, Yices2-fixedn, 2019-Boolectorn, MinkeyRink-fixedn, STP + CMS, CVC4, MathSAT5n, z3n, LazyBV2Int, MinkeyRink, STP + MergeSAT, Yices2
SAT PerformanceBitwuzlaBitwuzla-fixedn, MinkeyRink-fixedn, Bitwuzla, 2019-Poolectorn, 2019-Boolectorn, Yices2-fixedn, STP + CMS, CVC4, STP + MergeSAT, z3n, MathSAT5n, LazyBV2Int, MinkeyRink, Yices2
UNSAT PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, Yices2-fixedn, 2019-Poolectorn, 2019-Boolectorn, STP + CMS, Yices2, MinkeyRink-fixedn, CVC4, MathSAT5n, z3n, LazyBV2Int, MinkeyRink, STP + MergeSAT
24s PerformanceBitwuzla2019-Poolectorn, MinkeyRink-fixedn, Bitwuzla, Bitwuzla-fixedn, Yices2-fixedn, 2019-Boolectorn, STP + CMS, STP + MergeSAT, CVC4, MathSAT5n, z3n, LazyBV2Int, MinkeyRink, Yices2

QF_BVFP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, CVC4, 2019-Par4n, MathSAT5n, z3n, COLIBRI
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, CVC4, 2019-Par4n, MathSAT5n, z3n, COLIBRI
SAT PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4, 2019-Par4n, z3n, COLIBRI
UNSAT PerformanceBitwuzla2019-Par4n, Bitwuzla, Bitwuzla-fixedn, CVC4, MathSAT5n, z3n, COLIBRI
24s PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, 2019-Par4n, CVC4, MathSAT5n, z3n, COLIBRI

QF_BVFPLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4MathSAT5n, CVC4, COLIBRI
Parallel PerformanceCVC4MathSAT5n, CVC4, COLIBRI
SAT PerformanceCVC4MathSAT5n, CVC4, COLIBRI
UNSAT PerformanceCOLIBRICOLIBRI, MathSAT5n, CVC4
24s PerformanceCVC4CVC4, MathSAT5n, COLIBRI

QF_DT

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4z3n, 2018-CVC4n, CVC4, Alt-Ergo
Parallel PerformanceCVC4z3n, 2018-CVC4n, CVC4, Alt-Ergo
SAT PerformanceCVC42018-CVC4n, CVC4, z3n, Alt-Ergo
UNSAT PerformanceCVC4z3n, 2018-CVC4n, CVC4, Alt-Ergo
24s PerformanceCVC4z3n, 2018-CVC4n, CVC4, Alt-Ergo

QF_FP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, 2019-Par4n, COLIBRI, MathSAT5n, CVC4, z3n
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, 2019-Par4n, COLIBRI, MathSAT5n, CVC4, z3n
SAT PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, 2019-Par4n, MathSAT5n, CVC4, COLIBRI, z3n
UNSAT PerformanceBitwuzla2019-Par4n, Bitwuzla-fixedn, Bitwuzla, COLIBRI, CVC4, MathSAT5n, z3n
24s PerformanceCOLIBRICOLIBRI, 2019-Par4n, Bitwuzla, Bitwuzla-fixedn, CVC4, MathSAT5n, z3n

QF_FPLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCOLIBRICOLIBRI, MathSAT5n, z3n, CVC4
Parallel PerformanceCOLIBRICOLIBRI, MathSAT5n, z3n, CVC4
SAT PerformanceCOLIBRICOLIBRI, MathSAT5n, z3n, CVC4
UNSAT PerformanceCOLIBRICOLIBRI, CVC4, z3n, MathSAT5n
24s PerformanceCOLIBRICOLIBRI, CVC4, MathSAT5n, z3n

QF_IDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, Yices2-fixedn, 2019-Z3n, 2019-Par4n, z3n, CVC4, veriT, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, 2019-Z3n, z3n, CVC4, veriT, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
SAT PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, z3n, 2019-Z3n, CVC4, veriT, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
UNSAT PerformanceCVC42019-Par4n, 2019-Z3n, CVC4, Yices2, Yices2-fixedn, veriT, MathSAT5n, z3n, SMTInterpol, SMTInterpol-fixedn
24s PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, 2019-Z3n, z3n, CVC4, MathSAT5n, veriT, SMTInterpol-fixedn, SMTInterpol

QF_LIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, MathSAT5n, CVC4, z3n, Yices2, Yices2-fixedn, SMTInterpol, SMTInterpol-fixedn, veriT
Parallel PerformanceCVC42019-Par4n, MathSAT5n, CVC4, z3n, Yices2, Yices2-fixedn, SMTInterpol, SMTInterpol-fixedn, veriT
SAT PerformanceCVC42019-Par4n, z3n, MathSAT5n, CVC4, Yices2, Yices2-fixedn, SMTInterpol, SMTInterpol-fixedn, veriT
UNSAT PerformanceSMTInterpol2019-Par4n, SMTInterpol, SMTInterpol-fixedn, CVC4, MathSAT5n, Yices2-fixedn, Yices2, z3n, veriT
24s PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, CVC4, z3n, MathSAT5n, SMTInterpol, SMTInterpol-fixedn, veriT

QF_LIRA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Par4n, z3n, Yices2, Yices2-fixedn, MathSAT5n, CVC4, SMTInterpol-fixedn, SMTInterpol
Parallel PerformanceYices22019-Par4n, z3n, Yices2, Yices2-fixedn, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn
SAT PerformanceYices2Yices2, Yices2-fixedn, MathSAT5n, z3n, 2019-Par4n, CVC4, SMTInterpol-fixedn, SMTInterpol
UNSAT PerformanceYices22019-Par4n, z3n, Yices2, Yices2-fixedn, CVC4, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
24s PerformanceYices2Yices2-fixedn, Yices2, z3n, 2019-Par4n, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn

QF_LRA

Scoring SchemeWinnerRanking
Sequential PerformanceOpenSMTOpenSMT, 2019-SPASS-SATTn, 2019-Par4n, CVC4, Yices2, Yices2-fixedn, z3n, veriT, SMTInterpol-fixedn, SMTInterpol, MathSAT5n
Parallel PerformanceOpenSMT2019-Par4n, OpenSMT, 2019-SPASS-SATTn, CVC4, Yices2, Yices2-fixedn, z3n, veriT, SMTInterpol-fixedn, SMTInterpol, MathSAT5n
SAT PerformanceOpenSMT2019-Par4n, 2019-SPASS-SATTn, OpenSMT, Yices2-fixedn, Yices2, z3n, CVC4, SMTInterpol-fixedn, SMTInterpol, veriT, MathSAT5n
UNSAT PerformanceOpenSMT2019-Par4n, OpenSMT, 2019-SPASS-SATTn, CVC4, Yices2, Yices2-fixedn, veriT, z3n, MathSAT5n, SMTInterpol-fixedn, SMTInterpol
24s PerformanceYices2Yices2-fixedn, Yices2, 2019-SPASS-SATTn, OpenSMT, 2019-Par4n, z3n, CVC4, veriT, MathSAT5n, SMTInterpol-fixedn, SMTInterpol

QF_NIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, CVC4, MathSAT5n, Yices2, Yices2-fixedn, z3n, AProVE, SMT-RAT
Parallel PerformanceCVC42019-Par4n, CVC4, MathSAT5n, Yices2, Yices2-fixedn, z3n, AProVE, SMT-RAT
SAT PerformanceCVC42019-Par4n, CVC4, MathSAT5n, z3n, Yices2, Yices2-fixedn, AProVE, SMT-RAT
UNSAT PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, MathSAT5n, CVC4, z3n, SMT-RAT, AProVE
24s PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, MathSAT5n, z3n, CVC4, AProVE, SMT-RAT

QF_NIRA

Scoring SchemeWinnerRanking
Sequential PerformanceSMT-RATSMT-RAT, 2018-SMTRAT-Ratn, z3n, CVC4, MathSAT5n, Yices2, Yices2-fixedn
Parallel PerformanceSMT-RATSMT-RAT, 2018-SMTRAT-Ratn, z3n, CVC4, MathSAT5n, Yices2, Yices2-fixedn
SAT Performance-2018-SMTRAT-Ratn, SMT-RAT, CVC4, z3n, Yices2, MathSAT5n, Yices2-fixedn
UNSAT PerformanceSMT-RATSMT-RAT, 2018-SMTRAT-Ratn, z3n, CVC4, MathSAT5n, Yices2, Yices2-fixedn
24s Performance-z3n, 2018-SMTRAT-Ratn, SMT-RAT, CVC4, Yices2, MathSAT5n, Yices2-fixedn

QF_NRA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Par4n, Yices2-fixedn, Yices2, z3n, SMT-RAT-MCSAT, veriT+raSAT+Redlog, SMT-RAT-CAlC, CVC4, MathSAT5n
Parallel PerformanceYices22019-Par4n, Yices2-fixedn, Yices2, z3n, SMT-RAT-MCSAT, veriT+raSAT+Redlog, SMT-RAT-CAlC, CVC4, MathSAT5n
SAT PerformanceYices22019-Par4n, z3n, Yices2, Yices2-fixedn, SMT-RAT-MCSAT, SMT-RAT-CAlC, veriT+raSAT+Redlog, CVC4, MathSAT5n
UNSAT PerformanceYices22019-Par4n, Yices2-fixedn, Yices2, CVC4, MathSAT5n, z3n, SMT-RAT-MCSAT, veriT+raSAT+Redlog, SMT-RAT-CAlC
24s PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, z3n, SMT-RAT-MCSAT, veriT+raSAT+Redlog, SMT-RAT-CAlC, MathSAT5n, CVC4

QF_RDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, CVC4, z3n, veriT, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, CVC4, z3n, veriT, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
SAT PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, veriT, CVC4, MathSAT5n, z3n, SMTInterpol, SMTInterpol-fixedn
UNSAT PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, z3n, CVC4, veriT, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
24s PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, z3n, veriT, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn

QF_S

The division has disagreements

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Z3str4
Parallel PerformanceCVC4CVC4, Z3str4
SAT PerformanceCVC4CVC4, Z3str4
UNSAT PerformanceCVC4CVC4, Z3str4
24s PerformanceCVC4CVC4, Z3str4

QF_SLIA

The division has disagreements

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Z3str4
Parallel PerformanceCVC4CVC4, Z3str4
SAT PerformanceCVC4CVC4, Z3str4
UNSAT PerformanceCVC4CVC4, Z3str4
24s PerformanceCVC4CVC4, Z3str4

QF_UF

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, 2019-Par4n, veriT, z3n, OpenSMT, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, Alt-Ergo
Parallel PerformanceYices22019-Par4n, Yices2, 2019-Yices 2.6.2n, Yices2-fixedn, veriT, z3n, OpenSMT, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, Alt-Ergo
SAT PerformanceYices2Yices2, 2019-Par4n, 2019-Yices 2.6.2n, Yices2-fixedn, veriT, z3n, OpenSMT, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, Alt-Ergo
UNSAT PerformanceYices22019-Par4n, Yices2, 2019-Yices 2.6.2n, Yices2-fixedn, veriT, z3n, OpenSMT, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, Alt-Ergo
24s PerformanceYices22019-Par4n, Yices2, 2019-Yices 2.6.2n, Yices2-fixedn, veriT, z3n, OpenSMT, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, Alt-Ergo

QF_UFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, Bitwuzla, Bitwuzla-fixedn, MathSAT5n, CVC4, z3n
Parallel PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, Bitwuzla, Bitwuzla-fixedn, MathSAT5n, CVC4, z3n
SAT PerformanceYices2Yices2, 2019-Yices 2.6.2n, Yices2-fixedn, Bitwuzla, Bitwuzla-fixedn, MathSAT5n, CVC4, z3n
UNSAT PerformanceYices2Yices2, Yices2-fixedn, 2019-Yices 2.6.2n, Bitwuzla, Bitwuzla-fixedn, MathSAT5n, CVC4, z3n
24s PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, 2019-Yices 2.6.2n, Yices2, Yices2-fixedn, CVC4, MathSAT5n, z3n

QF_UFFP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, COLIBRI, CVC4, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, COLIBRI, CVC4, MathSAT5n
SAT Performance-COLIBRI, CVC4, Bitwuzla, MathSAT5n, Bitwuzla-fixedn
UNSAT PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, COLIBRI, CVC4, MathSAT5n
24s PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, COLIBRI, CVC4, MathSAT5n

QF_UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, z3n, SMTInterpol-fixedn, SMTInterpol, MathSAT5n, veriT, CVC4
Parallel PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, z3n, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, veriT, CVC4
SAT PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, veriT, MathSAT5n, z3n, SMTInterpol, SMTInterpol-fixedn, CVC4
UNSAT PerformanceYices22019-Yices 2.6.2n, Yices2-fixedn, Yices2, z3n, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, veriT, CVC4
24s PerformanceYices22019-Yices 2.6.2n, Yices2, Yices2-fixedn, z3n, SMTInterpol, SMTInterpol-fixedn, veriT, MathSAT5n, CVC4

QF_UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22018-Yicesn, Yices2-fixedn, Yices2, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, veriT, Alt-Ergo
Parallel PerformanceYices22018-Yicesn, Yices2, Yices2-fixedn, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, veriT, Alt-Ergo
SAT PerformanceYices2Yices2, Yices2-fixedn, 2018-Yicesn, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, veriT, Alt-Ergo
UNSAT PerformanceYices22018-Yicesn, Yices2, Yices2-fixedn, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, veriT, Alt-Ergo
24s PerformanceYices22018-Yicesn, Yices2, Yices2-fixedn, z3n, CVC4, SMTInterpol-fixedn, SMTInterpol, MathSAT5n, veriT, Alt-Ergo

QF_UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-SMTInterpoln, Yices2, Yices2-fixedn, veriT, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn, z3n, Alt-Ergo
Parallel PerformanceYices22019-SMTInterpoln, Yices2, Yices2-fixedn, veriT, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn, z3n, Alt-Ergo
SAT PerformanceYices22019-SMTInterpoln, Yices2, Yices2-fixedn, veriT, MathSAT5n, CVC4, SMTInterpol, SMTInterpol-fixedn, z3n, Alt-Ergo
UNSAT PerformanceYices2Yices2, Yices2-fixedn, veriT, MathSAT5n, CVC4, z3n, SMTInterpol, SMTInterpol-fixedn, 2019-SMTInterpoln, Alt-Ergo
24s PerformanceYices2Yices2, Yices2-fixedn, veriT, MathSAT5n, SMTInterpol-fixedn, SMTInterpol, 2019-SMTInterpoln, CVC4, z3n, Alt-Ergo

QF_UFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Yices2-fixedn, Yices2, 2019-CVC4n, MathSAT5n, z3n, Alt-Ergo
Parallel PerformanceCVC4CVC4, Yices2-fixedn, Yices2, 2019-CVC4n, MathSAT5n, z3n, Alt-Ergo
SAT PerformanceYices2Yices2-fixedn, Yices2, CVC4, 2019-CVC4n, MathSAT5n, z3n, Alt-Ergo
UNSAT PerformanceCVC4MathSAT5n, CVC4, 2019-CVC4n, z3n, Yices2, Yices2-fixedn, Alt-Ergo
24s PerformanceCVC4CVC4, 2019-CVC4n, Yices2, Yices2-fixedn, MathSAT5n, z3n, Alt-Ergo

QF_UFNRA

Scoring SchemeWinnerRanking
Sequential PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, z3n, CVC4, MathSAT5n, veriT+raSAT+Redlog, Alt-Ergo
Parallel PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, z3n, CVC4, MathSAT5n, veriT+raSAT+Redlog, Alt-Ergo
SAT PerformanceYices22019-Par4n, Yices2, Yices2-fixedn, z3n, CVC4, MathSAT5n, veriT+raSAT+Redlog, Alt-Ergo
UNSAT PerformanceYices2MathSAT5n, 2019-Par4n, z3n, Yices2-fixedn, Yices2, CVC4, veriT+raSAT+Redlog, Alt-Ergo
24s PerformanceYices22019-Par4n, z3n, Yices2, Yices2-fixedn, MathSAT5n, CVC4, veriT+raSAT+Redlog, Alt-Ergo

UF

Scoring SchemeWinnerRanking
Sequential PerformanceVampireVampire, CVC4, 2019-CVC4n, 2018-Vampiren, veriT, veriT+viten, Alt-Ergo, z3n, SMTInterpol-fixedn, UltimateEliminator+MathSAT, SMTInterpol
Parallel PerformanceVampireVampire, 2018-Vampiren, CVC4, 2019-CVC4n, veriT, veriT+viten, Alt-Ergo, z3n, SMTInterpol-fixedn, UltimateEliminator+MathSAT, SMTInterpol
SAT PerformanceVampireVampire, 2018-Vampiren, CVC4, 2019-CVC4n, z3n, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT, Alt-Ergo, veriT, veriT+viten
UNSAT PerformanceCVC4CVC4, 2019-CVC4n, Vampire, veriT, 2018-Vampiren, veriT+viten, Alt-Ergo, z3n, SMTInterpol-fixedn, UltimateEliminator+MathSAT, SMTInterpol
24s PerformanceVampireVampire, 2018-Vampiren, veriT+viten, 2019-CVC4n, CVC4, veriT, Alt-Ergo, z3n, SMTInterpol-fixedn, UltimateEliminator+MathSAT, SMTInterpol

UFBV

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42018-Z3n, 2019-Par4n, z3n, CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-Par4n, 2018-Z3n, z3n, CVC4, UltimateEliminator+MathSAT
SAT Performance-z3n, 2019-Par4n, 2018-Z3n, UltimateEliminator+MathSAT, CVC4
UNSAT PerformanceCVC42019-Par4n, 2018-Z3n, z3n, CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4z3n, 2019-Par4n, 2018-Z3n, CVC4, UltimateEliminator+MathSAT

UFDT

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, 2019-CVC4n, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, 2019-CVC4n, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, 2019-CVC4n, Vampire, UltimateEliminator+MathSAT, Alt-Ergo
UNSAT PerformanceCVC4CVC4, 2019-CVC4n, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceAlt-ErgoAlt-Ergo, 2019-CVC4n, CVC4, Vampire, UltimateEliminator+MathSAT

UFDTLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-CVC4n, CVC4, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-CVC4n, CVC4, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
SAT Performance-2019-CVC4n, Alt-Ergo, Vampire, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC42019-CVC4n, CVC4, Vampire, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceVampireVampire, Alt-Ergo, CVC4, 2019-CVC4n, UltimateEliminator+MathSAT

UFDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Alt-Ergo, UltimateEliminator+MathSAT, Vampire
Parallel PerformanceCVC4CVC4, Alt-Ergo, UltimateEliminator+MathSAT, Vampire
SAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT, Alt-Ergo, Vampire
UNSAT PerformanceVampireVampire, CVC4, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, Alt-Ergo, UltimateEliminator+MathSAT, Vampire

UFDTNIA

Scoring SchemeWinnerRanking
Sequential PerformanceVampireVampire, 2019-Vampiren, CVC4, UltimateEliminator+MathSAT, Alt-Ergo
Parallel PerformanceVampireVampire, 2019-Vampiren, CVC4, UltimateEliminator+MathSAT, Alt-Ergo
SAT Performance-2019-Vampiren, Alt-Ergo, Vampire, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceVampireVampire, 2019-Vampiren, CVC4, UltimateEliminator+MathSAT, Alt-Ergo
24s PerformanceVampireVampire, 2019-Vampiren, CVC4, UltimateEliminator+MathSAT, Alt-Ergo

UFDTNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, Alt-Ergo, Vampire, UltimateEliminator+MathSAT
Parallel PerformanceVampireVampire, CVC4, Alt-Ergo, UltimateEliminator+MathSAT
SAT Performance-Alt-Ergo, Vampire, CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceVampireVampire, CVC4, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, Alt-Ergo, Vampire, UltimateEliminator+MathSAT

UFFPDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

UFFPDTNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, UltimateEliminator+MathSAT
Parallel PerformanceCVC4CVC4, UltimateEliminator+MathSAT
SAT Performance-CVC4, UltimateEliminator+MathSAT
UNSAT PerformanceCVC4CVC4, UltimateEliminator+MathSAT
24s PerformanceCVC4CVC4, UltimateEliminator+MathSAT

UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, veriT+viten, veriT, Vampire, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-Par4n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, veriT+viten, Vampire, veriT, UltimateEliminator+MathSAT
SAT PerformanceCVC42019-Par4n, z3n, CVC4, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT, veriT+viten, veriT, Vampire
UNSAT PerformanceCVC42019-Par4n, z3n, CVC4, veriT, veriT+viten, Vampire, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
24s PerformanceCVC42019-Par4n, z3n, CVC4, SMTInterpol, SMTInterpol-fixedn, veriT+viten, veriT, Vampire, UltimateEliminator+MathSAT

UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, CVC4, veriT, Vampire, veriT+viten, Alt-Ergo, z3n, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-Par4n, CVC4, veriT, Vampire, veriT+viten, Alt-Ergo, z3n, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
SAT PerformanceSMTInterpol2019-Par4n, z3n, SMTInterpol, SMTInterpol-fixedn, CVC4, UltimateEliminator+MathSAT, Alt-Ergo, veriT+viten, veriT, Vampire
UNSAT PerformanceCVC42019-Par4n, CVC4, veriT, Vampire, veriT+viten, Alt-Ergo, z3n, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
24s PerformanceCVC42019-Par4n, veriT+viten, CVC4, Vampire, z3n, Alt-Ergo, veriT, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT

UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceAlt-Ergoz3n, 2018-Z3n, veriT+viten, Alt-Ergo, SMTInterpol-fixedn, SMTInterpol, CVC4, veriT, Vampire, UltimateEliminator+MathSAT
Parallel PerformanceAlt-Ergoz3n, 2018-Z3n, veriT+viten, Alt-Ergo, SMTInterpol-fixedn, SMTInterpol, veriT, CVC4, Vampire, UltimateEliminator+MathSAT
SAT Performance-z3n, 2018-Z3n, UltimateEliminator+MathSAT, veriT+viten, Alt-Ergo, SMTInterpol-fixedn, SMTInterpol, veriT, Vampire, CVC4
UNSAT PerformanceveriTveriT, veriT+viten, CVC4, Alt-Ergo, z3n, 2018-Z3n, SMTInterpol-fixedn, SMTInterpol, Vampire, UltimateEliminator+MathSAT
24s PerformanceAlt-Ergo2018-Z3n, z3n, veriT+viten, Alt-Ergo, SMTInterpol-fixedn, SMTInterpol, veriT, CVC4, Vampire, UltimateEliminator+MathSAT

UFNIA

The division has disagreements

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42019-Par4n, CVC4, z3n, Vampire, 2018-Vampiren, Alt-Ergo, UltimateEliminator+MathSAT
Parallel PerformanceCVC42019-Par4n, CVC4, z3n, Vampire, Alt-Ergo, UltimateEliminator+MathSAT, 2018-Vampiren
SAT PerformanceCVC42019-Par4n, CVC4, z3n, UltimateEliminator+MathSAT, Alt-Ergo, Vampire, 2018-Vampiren
UNSAT PerformanceCVC42018-Vampiren, 2019-Par4n, CVC4, Vampire, z3n, Alt-Ergo, UltimateEliminator+MathSAT
24s PerformanceCVC42019-Par4n, CVC4, z3n, Vampire, 2018-Vampiren, Alt-Ergo, UltimateEliminator+MathSAT