SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

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 SchemeWinnerRanking
Sequential PerformanceCVC42018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
Parallel PerformanceCVC42018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
SAT PerformanceCVC42018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
UNSAT Performance-2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n
24s PerformanceCVC42018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4, Z3n

ALIA

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpol2018-Z3n, Z3n, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceSMTInterpol2018-Z3n, Z3n, SMTInterpol, CVC4, Alt-Ergo, Vampire, veriT, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
SAT PerformanceSMTInterpol2018-Z3n, Z3n, SMTInterpol, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, Vampire, veriT
UNSAT PerformanceAlt-Ergo2018-Z3n, Z3n, Alt-Ergo, CVC4, SMTInterpol, Vampire, veriT, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
24s PerformanceCVC42018-Z3n, Z3n, CVC4, Alt-Ergo, SMTInterpol, Vampire, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

AUFDTLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42018-CVC4n, CVC4, Alt-Ergo, Vampire
Parallel PerformanceCVC42018-CVC4n, CVC4, Vampire, Alt-Ergo
SAT PerformanceCVC42018-CVC4n, CVC4, Alt-Ergo, Vampire
UNSAT PerformanceCVC42018-CVC4n, CVC4, Vampire, Alt-Ergo
24s PerformanceCVC42018-CVC4n, CVC4, Alt-Ergo, Vampire

AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42018-CVC4n, CVC4-SymBreakn, CVC4, Vampire, Z3n, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel PerformanceVampire2018-CVC4n, Vampire, CVC4-SymBreakn, CVC4, Z3n, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT PerformanceCVC4Z3n, 2018-CVC4n, CVC4-SymBreakn, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, veriT, Alt-Ergo
UNSAT PerformanceVampireVampire, 2018-CVC4n, CVC4-SymBreakn, CVC4, Alt-Ergo, veriT, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s PerformanceVampireVampire, Z3n, 2018-CVC4n, CVC4-SymBreakn, CVC4, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

AUFLIRA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, Vampire, CVC4-SymBreakn, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel PerformancePar4Par4, Z3n, 2018-Z3n, Vampire, CVC4, CVC4-SymBreakn, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT PerformancePar4Par4, 2018-Z3n, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, CVC4, CVC4-SymBreakn, veriT, Alt-Ergo, Vampire, SMTInterpol
UNSAT PerformanceVampireVampire, CVC4, CVC4-SymBreakn, Par4, Z3n, 2018-Z3n, Alt-Ergo, veriT, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s PerformancePar4Par4, 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 SchemeWinnerRanking
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 SchemeWinnerRanking
Sequential PerformancePar4Par4, CVC4, 2018-CVC4n, Vampire, Z3n, Alt-Ergo, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel PerformancePar4Par4, CVC4, 2018-CVC4n, Vampire, Z3n, Alt-Ergo, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
SAT PerformancePar4Par4, Z3n, 2018-CVC4n, CVC4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, Vampire
UNSAT PerformancePar4Par4, Vampire, CVC4, 2018-CVC4n, Z3n, Alt-Ergo, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s PerformancePar4Par4, Vampire, Z3n, 2018-CVC4n, Alt-Ergo, CVC4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

BV

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, Q3B, 2018-CVC4n, CVC4, Poolector, Boolector, Z3n, UltimateEliminator+MathSAT-5.5.4
Parallel PerformancePar4Par4, Q3B, 2018-CVC4n, CVC4, Poolector, Boolector, Z3n, UltimateEliminator+MathSAT-5.5.4
SAT PerformancePar4Par4, Q3B, Poolector, Boolector, Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
UNSAT PerformancePar4Par4, CVC4, 2018-CVC4n, Q3B, Z3n, Poolector, Boolector, UltimateEliminator+MathSAT-5.5.4
24s PerformancePar4Par4, Q3B, Poolector, Z3n, Boolector, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4

BVFP

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4
SAT PerformanceCVC4Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4
UNSAT PerformanceCVC4CVC4, 2018-CVC4n, Z3n, UltimateEliminator+MathSAT-5.5.4
24s PerformanceCVC4Z3n, CVC4, 2018-CVC4n, UltimateEliminator+MathSAT-5.5.4

FP

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
SAT PerformanceCVC4Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
UNSAT PerformanceCVC4Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4
24s PerformanceCVC4Z3n, 2018-CVC4n, CVC4, UltimateEliminator+MathSAT-5.5.4

LIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4Z3n, 2018-Z3n, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, veriT, ProB, UltimateEliminator+Yices-2.6.1
Parallel PerformanceCVC4Z3n, 2018-Z3n, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, veriT, ProB, UltimateEliminator+Yices-2.6.1
SAT PerformanceCVC4Z3n, 2018-Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, ProB, UltimateEliminator+Yices-2.6.1, SMTInterpol, Vampire, veriT
UNSAT PerformanceCVC4Z3n, CVC4, 2018-Z3n, Vampire, SMTInterpol, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, ProB
24s PerformanceCVC4Z3n, 2018-Z3n, CVC4, Vampire, SMTInterpol, veriT, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1

LRA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Z3n, Par4, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Vampire, SMTInterpol
Parallel PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Vampire, SMTInterpol
SAT PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, SMTInterpol, Vampire
UNSAT PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, Vampire, UltimateEliminator+Yices-2.6.1, SMTInterpol
24s PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, SMTInterpol, Vampire

NIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC42018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire
Parallel PerformanceCVC42018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire
SAT PerformanceCVC42018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire
UNSAT PerformanceCVC42018-Z3n, CVC4, Z3n, Vampire, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, ProB
24s PerformanceCVC42018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4, ProB, UltimateEliminator+Yices-2.6.1, Vampire

NRA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, Vampire, 2018-Z3n, Z3n, 2018-Vampiren, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel PerformancePar4Par4, Vampire, 2018-Z3n, Z3n, 2018-Vampiren, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT PerformancePar4Z3n, 2018-Z3n, Par4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, 2018-Vampiren, CVC4, Vampire
UNSAT PerformancePar4Par4, Vampire, 2018-Z3n, Z3n, 2018-Vampiren, CVC4, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s PerformancePar4Par4, Z3n, 2018-Z3n, Vampire, CVC4, 2018-Vampiren, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

QF_ABV

Scoring SchemeWinnerRanking
Sequential PerformanceBoolectorBoolector, Par4, 2018-Boolectorn, Yices 2.6.2, Poolector, CVC4, Z3n
Parallel PerformancePar4Par4, Poolector, Boolector, 2018-Boolectorn, Yices 2.6.2, CVC4, Z3n
SAT PerformancePoolectorPoolector, Boolector, Par4, Yices 2.6.2, 2018-Boolectorn, CVC4, Z3n
UNSAT PerformancePar4Par4, Boolector, 2018-Boolectorn, Poolector, Yices 2.6.2, Z3n, CVC4
24s PerformancePar4Par4, Poolector, Boolector, Yices 2.6.2, 2018-Boolectorn, CVC4, Z3n

QF_ALIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, SMTInterpol, CVC4, Z3n, Alt-Ergo, veriT
Parallel PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, SMTInterpol, CVC4, Z3n, Alt-Ergo, veriT
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, SMTInterpol, CVC4, Z3n, veriT, Alt-Ergo
UNSAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT
24s PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, SMTInterpol, Z3n, CVC4, Alt-Ergo, veriT

QF_ANIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, MathSAT-na-ext, MathSAT-default, 2018-Z3n, Z3n, Alt-Ergo
Parallel PerformanceCVC4CVC4, MathSAT-na-ext, MathSAT-default, 2018-Z3n, Z3n, Alt-Ergo
SAT Performance-2018-Z3n, Alt-Ergo, CVC4, MathSAT-default, MathSAT-na-ext, Z3n
UNSAT PerformanceCVC4CVC4, MathSAT-na-ext, MathSAT-default, 2018-Z3n, Z3n, Alt-Ergo
24s PerformanceMathSAT-na-ext2018-Z3n, Z3n, MathSAT-na-ext, MathSAT-default, CVC4, Alt-Ergo

QF_AUFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, Z3n, Boolector, Poolector, 2018-CVC4n, CVC4
Parallel PerformanceYices 2.6.2Yices 2.6.2, Z3n, Boolector, Poolector, 2018-CVC4n, CVC4
SAT PerformanceYices 2.6.2Yices 2.6.2, Boolector, Poolector, Z3n, 2018-CVC4n, CVC4
UNSAT PerformanceYices 2.6.2Z3n, Yices 2.6.2, Boolector, Poolector, 2018-CVC4n, CVC4
24s PerformanceYices 2.6.2Yices 2.6.2, Boolector, Poolector, CVC4, 2018-CVC4n, Z3n

QF_AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, Alt-Ergo, veriT
Parallel PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
UNSAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT
24s PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, CVC4, Alt-Ergo, veriT

QF_AUFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, 2018-Z3n, CVC4, Z3n, Alt-Ergo
Parallel PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, 2018-Z3n, CVC4, Z3n, Alt-Ergo
SAT PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, CVC4, 2018-Z3n, Z3n, Alt-Ergo
UNSAT PerformanceMathSAT-na-ext2018-Z3n, Z3n, MathSAT-na-ext, MathSAT-default, CVC4, Alt-Ergo
24s PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, 2018-Z3n, CVC4, Z3n, Alt-Ergo

QF_AX

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, Alt-Ergo
Parallel PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, Alt-Ergo
SAT PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, CVC4, Z3n, SMTInterpol, Alt-Ergo
UNSAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, Alt-Ergo
24s PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, Alt-Ergo

QF_BV

Scoring SchemeWinnerRanking
Sequential PerformanceBoolectorBoolector, 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 PerformancePoolectorPoolector, 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 PerformancePoolectorPoolector, 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 PerformancePoolectorPoolector, 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 PerformancePar4Par4, 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 SchemeWinnerRanking
Sequential PerformancePar4Par4, 2018-CVC4n, CVC4, Z3n
Parallel PerformancePar4Par4, 2018-CVC4n, CVC4, Z3n
SAT PerformancePar4Par4, 2018-CVC4n, CVC4, Z3n
UNSAT PerformancePar4Par4, CVC4, 2018-CVC4n, Z3n
24s PerformancePar4Par4, CVC4, 2018-CVC4n, Z3n

QF_DT

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

QF_FP

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, COLIBRI, CVC4, 2018-COLIBRIn, Z3n
Parallel PerformancePar4Par4, COLIBRI, CVC4, 2018-COLIBRIn, Z3n
SAT PerformancePar4Par4, CVC4, COLIBRI, 2018-COLIBRIn, Z3n
UNSAT PerformancePar4Par4, COLIBRI, 2018-COLIBRIn, CVC4, Z3n
24s PerformanceCOLIBRICOLIBRI, Par4, 2018-COLIBRIn, CVC4, Z3n

QF_IDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Z3n, 2018-Yicesn, Yices 2.6.2, Par4, CVC4, veriT, SMTInterpol, ProB
Parallel PerformancePar4Par4, Z3n, 2018-Yicesn, Yices 2.6.2, CVC4, veriT, SMTInterpol, ProB
SAT PerformancePar4Par4, Z3n, 2018-Yicesn, Yices 2.6.2, CVC4, veriT, SMTInterpol, ProB
UNSAT PerformancePar4Z3n, Par4, CVC4, 2018-Yicesn, Yices 2.6.2, veriT, SMTInterpol, ProB
24s PerformancePar4Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, veriT, SMTInterpol, ProB

QF_LIA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, SPASS-SATT, 2018-SPASS-SATTn, Z3n, CVC4, Ctrl-Ergo, Yices 2.6.2, SMTInterpol, CVC4-SymBreakn, veriT, ProB
Parallel PerformancePar4Par4, SPASS-SATT, 2018-SPASS-SATTn, Z3n, CVC4, Ctrl-Ergo, Yices 2.6.2, SMTInterpol, CVC4-SymBreakn, veriT, ProB
SAT PerformancePar4Par4, 2018-SPASS-SATTn, SPASS-SATT, Z3n, CVC4, Ctrl-Ergo, Yices 2.6.2, SMTInterpol, CVC4-SymBreakn, veriT, ProB
UNSAT PerformancePar4Par4, SPASS-SATT, SMTInterpol, 2018-SPASS-SATTn, Ctrl-Ergo, CVC4, CVC4-SymBreakn, Z3n, Yices 2.6.2, veriT, ProB
24s PerformancePar4Par4, SPASS-SATT, Yices 2.6.2, 2018-SPASS-SATTn, Z3n, Ctrl-Ergo, CVC4, SMTInterpol, CVC4-SymBreakn, veriT, ProB

QF_LIRA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, 2018-Z3n, Yices 2.6.2, Z3n, CVC4, SMTInterpol
Parallel PerformancePar4Par4, 2018-Z3n, Yices 2.6.2, Z3n, CVC4, SMTInterpol
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Z3n, Par4, Z3n, CVC4, SMTInterpol
UNSAT PerformancePar4Par4, 2018-Z3n, Yices 2.6.2, Z3n, CVC4, SMTInterpol
24s PerformanceYices 2.6.2Yices 2.6.2, 2018-Z3n, Par4, Z3n, CVC4, SMTInterpol

QF_LRA

Scoring SchemeWinnerRanking
Sequential PerformanceSPASS-SATTSPASS-SATT, 2018-CVC4n, Par4, Yices 2.6.2, CVC4, CVC4-SymBreakn, veriT, SMTInterpol, Z3n, OpenSMT2, Ctrl-Ergo
Parallel PerformancePar4Par4, SPASS-SATT, 2018-CVC4n, Yices 2.6.2, CVC4, CVC4-SymBreakn, veriT, SMTInterpol, Z3n, Ctrl-Ergo, OpenSMT2
SAT PerformancePar4Par4, SPASS-SATT, 2018-CVC4n, Yices 2.6.2, CVC4, CVC4-SymBreakn, SMTInterpol, veriT, Ctrl-Ergo, Z3n, OpenSMT2
UNSAT PerformancePar4Par4, SPASS-SATT, 2018-CVC4n, CVC4, Yices 2.6.2, veriT, CVC4-SymBreakn, OpenSMT2, Z3n, SMTInterpol, Ctrl-Ergo
24s PerformanceYices 2.6.2Yices 2.6.2, Par4, SPASS-SATT, CVC4, veriT, 2018-CVC4n, Z3n, OpenSMT2, SMTInterpol, Ctrl-Ergo, CVC4-SymBreakn

QF_NIA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, CVC4, CVC4-SymBreakn, Yices 2.6.2, 2018-CVC4n, Z3n, AProVE, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext
Parallel PerformancePar4Par4, CVC4, CVC4-SymBreakn, Yices 2.6.2, 2018-CVC4n, Z3n, AProVE, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext
SAT PerformancePar4Par4, CVC4, CVC4-SymBreakn, Yices 2.6.2, 2018-CVC4n, AProVE, Z3n, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext
UNSAT PerformancePar4Par4, MathSAT-default, Yices 2.6.2, MathSAT-na-ext, CVC4, CVC4-SymBreakn, 2018-CVC4n, Z3n, SMT-RAT, ProB, AProVE
24s PerformancePar4Par4, Yices 2.6.2, CVC4, 2018-CVC4n, CVC4-SymBreakn, Z3n, AProVE, SMT-RAT, ProB, MathSAT-default, MathSAT-na-ext

QF_NIRA

Scoring SchemeWinnerRanking
Sequential PerformanceSMT-RAT2018-SMTRAT-Ratn, SMT-RAT, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Yices 2.6.2
Parallel PerformanceSMT-RAT2018-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 PerformanceSMT-RAT2018-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 SchemeWinnerRanking
Sequential PerformancePar4Par4, Yices 2.6.2, Z3n, 2018-Z3n, SMTRAT-MCSAT, veriT+raSAT+Redlog, CVC4, CVC4-SymBreakn, MathSAT-default, SMT-RAT, MathSAT-na-ext
Parallel PerformancePar4Par4, Yices 2.6.2, Z3n, 2018-Z3n, SMTRAT-MCSAT, veriT+raSAT+Redlog, CVC4, CVC4-SymBreakn, MathSAT-default, SMT-RAT, MathSAT-na-ext
SAT PerformancePar4Par4, Z3n, Yices 2.6.2, 2018-Z3n, SMTRAT-MCSAT, veriT+raSAT+Redlog, SMT-RAT, CVC4, MathSAT-default, CVC4-SymBreakn, MathSAT-na-ext
UNSAT PerformancePar4Par4, CVC4, CVC4-SymBreakn, MathSAT-default, MathSAT-na-ext, Yices 2.6.2, Z3n, veriT+raSAT+Redlog, 2018-Z3n, SMTRAT-MCSAT, SMT-RAT
24s PerformancePar4Par4, 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 SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, CVC4, veriT, Z3n, SMTInterpol
Parallel PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, CVC4, veriT, Z3n, SMTInterpol
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, veriT, CVC4, Z3n, SMTInterpol
UNSAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, CVC4, Z3n, veriT, SMTInterpol
24s PerformanceYices 2.6.2Yices 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 SchemeRanking
Sequential PerformanceCVC4
Parallel PerformanceCVC4
SAT PerformanceCVC4
UNSAT PerformanceCVC4
24s PerformanceCVC4

QF_SLIA

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

Scoring SchemeRanking
Sequential PerformanceCVC4, 2018-CVC4n
Parallel PerformanceCVC4, 2018-CVC4n
SAT PerformanceCVC4, 2018-CVC4n
UNSAT PerformanceCVC4, 2018-CVC4n
24s PerformanceCVC4, 2018-CVC4n

QF_UF

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Par4, veriT, CVC4, OpenSMT2, Z3n, SMTInterpol, Alt-Ergo
Parallel PerformancePar4Par4, Yices 2.6.2, 2018-Yicesn, veriT, CVC4, OpenSMT2, Z3n, SMTInterpol, Alt-Ergo
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Par4, veriT, Z3n, SMTInterpol, CVC4, OpenSMT2, Alt-Ergo
UNSAT PerformancePar4Par4, Yices 2.6.2, 2018-Yicesn, veriT, OpenSMT2, CVC4, Z3n, SMTInterpol, Alt-Ergo
24s PerformancePar4Par4, Yices 2.6.2, 2018-Yicesn, veriT, OpenSMT2, CVC4, Z3n, SMTInterpol, Alt-Ergo

QF_UFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, Boolector, 2018-Boolectorn, CVC4, Poolector, Z3n
Parallel PerformanceYices 2.6.2Yices 2.6.2, Poolector, Boolector, 2018-Boolectorn, CVC4, Z3n
SAT PerformanceYices 2.6.2Yices 2.6.2, Poolector, Boolector, 2018-Boolectorn, Z3n, CVC4
UNSAT PerformanceYices 2.6.2Yices 2.6.2, Poolector, Boolector, 2018-Boolectorn, CVC4, Z3n
24s PerformanceYices 2.6.22018-Boolectorn, Yices 2.6.2, Boolector, Poolector, CVC4, Z3n

QF_UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4
Parallel PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, SMTInterpol
UNSAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4
24s PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, SMTInterpol, veriT, CVC4

QF_UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
Parallel PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
SAT PerformanceYices 2.6.2Yices 2.6.2, 2018-Yicesn, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo
UNSAT PerformanceYices 2.6.2Z3n, 2018-Yicesn, Yices 2.6.2, SMTInterpol, CVC4, veriT, Alt-Ergo
24s PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, Z3n, CVC4, SMTInterpol, veriT, Alt-Ergo

QF_UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpolSMTInterpol, Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, Alt-Ergo
Parallel PerformanceSMTInterpolSMTInterpol, Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, Alt-Ergo
SAT PerformanceSMTInterpolSMTInterpol, Yices 2.6.2, 2018-Yicesn, Z3n, veriT, CVC4, Alt-Ergo
UNSAT PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, Z3n, veriT, CVC4, SMTInterpol, Alt-Ergo
24s PerformanceYices 2.6.22018-Yicesn, Yices 2.6.2, veriT, Z3n, CVC4, SMTInterpol, Alt-Ergo

QF_UFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, MathSAT-default, 2018-Yicesn, Yices 2.6.2, Z3n, MathSAT-na-ext, Alt-Ergo
Parallel PerformanceCVC4CVC4, MathSAT-default, 2018-Yicesn, Yices 2.6.2, Z3n, MathSAT-na-ext, Alt-Ergo
SAT PerformanceCVC4CVC4, 2018-Yicesn, Yices 2.6.2, MathSAT-default, Z3n, MathSAT-na-ext, Alt-Ergo
UNSAT PerformanceCVC4CVC4, Z3n, MathSAT-default, MathSAT-na-ext, 2018-Yicesn, Yices 2.6.2, Alt-Ergo
24s PerformanceCVC4CVC4, 2018-Yicesn, Yices 2.6.2, MathSAT-default, Z3n, MathSAT-na-ext, Alt-Ergo

QF_UFNRA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, veriT+raSAT+Redlog, Alt-Ergo
Parallel PerformancePar4Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Alt-Ergo, veriT+raSAT+Redlog
SAT PerformancePar4Par4, 2018-Yicesn, Yices 2.6.2, Z3n, CVC4, MathSAT-default, MathSAT-na-ext, Alt-Ergo, veriT+raSAT+Redlog
UNSAT PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, Z3n, Par4, 2018-Yicesn, Yices 2.6.2, CVC4, Alt-Ergo, veriT+raSAT+Redlog
24s PerformancePar4Z3n, Par4, MathSAT-default, MathSAT-na-ext, 2018-Yicesn, Yices 2.6.2, CVC4, Alt-Ergo, veriT+raSAT+Redlog

UF

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, 2018-CVC4n, Par4, Vampire, 2018-Vampiren, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1
Parallel PerformanceVampire2018-Vampiren, Vampire, Par4, CVC4, 2018-CVC4n, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1
SAT PerformanceVampire2018-Vampiren, Vampire, CVC4, 2018-CVC4n, Par4, Z3n, SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, Alt-Ergo, veriT
UNSAT PerformancePar4Par4, CVC4, 2018-CVC4n, 2018-Vampiren, Vampire, veriT, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s PerformanceVampire2018-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 SchemeWinnerRanking
Sequential PerformancePar42018-Z3n, Par4, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4
Parallel PerformancePar4Par4, 2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4
SAT PerformancePar4Par4, 2018-Z3n, Z3n, UltimateEliminator+MathSAT-5.5.4, CVC4
UNSAT PerformancePar4Par4, 2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4
24s PerformancePar4Par4, 2018-Z3n, Z3n, CVC4, UltimateEliminator+MathSAT-5.5.4

UFDT

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
Parallel PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
SAT PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
UNSAT PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
24s PerformanceAlt-ErgoAlt-Ergo, 2018-CVC4n, CVC4, Vampire

UFDTLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
Parallel PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
SAT Performance-2018-CVC4n, Alt-Ergo, CVC4, Vampire
UNSAT PerformanceCVC4CVC4, 2018-CVC4n, Vampire, Alt-Ergo
24s PerformanceVampireVampire, Alt-Ergo, CVC4, 2018-CVC4n

UFDTNIA

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

UFIDL

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, veriT, SMTInterpol, Vampire, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel PerformancePar4Par4, Z3n, 2018-Z3n, CVC4, veriT, SMTInterpol, Vampire, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
SAT PerformancePar4Par4, 2018-Z3n, Z3n, CVC4, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, veriT, Vampire
UNSAT PerformancePar4Par4, 2018-Z3n, Z3n, CVC4, veriT, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s PerformancePar4Par4, 2018-Z3n, Z3n, CVC4, veriT, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

UFLIA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, CVC4, 2018-CVC4n, veriT, Vampire, Z3n, Alt-Ergo, SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4
Parallel PerformancePar4Par4, CVC4, 2018-CVC4n, veriT, Vampire, Z3n, Alt-Ergo, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT PerformancePar4Par4, Z3n, SMTInterpol, 2018-CVC4n, CVC4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Alt-Ergo, veriT, Vampire
UNSAT PerformancePar4Par4, CVC4, 2018-CVC4n, veriT, Vampire, Alt-Ergo, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s PerformancePar4Par4, 2018-CVC4n, CVC4, veriT, Z3n, Alt-Ergo, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceAlt-Ergo2018-Z3n, Z3n, Alt-Ergo, veriT, Vampire, CVC4, SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel PerformanceAlt-Ergo2018-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 PerformanceveriTveriT, CVC4, Alt-Ergo, 2018-Z3n, Z3n, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
24s PerformanceAlt-ErgoZ3n, 2018-Z3n, Alt-Ergo, veriT, CVC4, Vampire, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFNIA

Scoring SchemeWinnerRanking
Sequential PerformancePar4Par4, CVC4-SymBreakn, CVC4, Z3n, 2018-Z3n, Vampire, 2018-Vampiren, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel PerformancePar42018-Vampiren, Par4, CVC4-SymBreakn, CVC4, Vampire, Z3n, 2018-Z3n, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
SAT PerformancePar4Par4, CVC4, CVC4-SymBreakn, Z3n, 2018-Z3n, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, Alt-Ergo, 2018-Vampiren, Vampire
UNSAT PerformancePar42018-Vampiren, Par4, CVC4-SymBreakn, CVC4, Vampire, Z3n, 2018-Z3n, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
24s PerformancePar4Par4, CVC4, CVC4-SymBreakn, Z3n, 2018-Z3n, 2018-Vampiren, Vampire, Alt-Ergo, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1