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 - Unsat Core Track (Summary)

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

AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

AUFLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

AUFNIA

Scoring SchemeWinnerRanking
Sequential Performance-UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, Z3n, CVC4-uc
Parallel Performance-UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, CVC4-uc, Z3n

AUFNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, 2018-CVC4 (unsat core)n, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4-ucCVC4-uc, 2018-CVC4 (unsat core)n, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

BV

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, Z3n, 2018-Z3 (unsat core)n, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4-ucCVC4-uc, Z3n, 2018-Z3 (unsat core)n, UltimateEliminator+MathSAT-5.5.4

LIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1
Parallel PerformanceCVC4-uc2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1

NIA

Scoring SchemeWinnerRanking
Sequential Performance-CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, 2018-CVC4 (unsat core)n, UltimateEliminator+MathSAT-5.5.4
Parallel Performance-CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, 2018-CVC4 (unsat core)n, UltimateEliminator+MathSAT-5.5.4

QF_ABV

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Z3n, 2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc
Parallel PerformanceYices 2.6.2Z3n, 2018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc

QF_ALIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.22018-Z3 (unsat core)n, Z3n, Yices 2.6.2, SMTInterpol, CVC4-uc
Parallel PerformanceYices 2.6.22018-Z3 (unsat core)n, Z3n, Yices 2.6.2, SMTInterpol, CVC4-uc

QF_ANIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n

QF_AUFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, Z3n, 2018-MathSAT (unsat core)n, CVC4-uc
Parallel PerformanceYices 2.6.2Yices 2.6.2, Z3n, 2018-MathSAT (unsat core)n, CVC4-uc

QF_AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, Yices 2.6.2, SMTInterpol
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, Yices 2.6.2, SMTInterpol

QF_AUFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceMathSAT-default2018-Z3 (unsat core)n, Z3n, MathSAT-default, CVC4-uc, MathSAT-na-ext
Parallel PerformanceMathSAT-default2018-Z3 (unsat core)n, Z3n, MathSAT-default, CVC4-uc, MathSAT-na-ext

QF_AX

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.22018-Yices (unsat core)n, Yices 2.6.2, Z3n, CVC4-uc, SMTInterpol
Parallel PerformanceYices 2.6.22018-Yices (unsat core)n, Yices 2.6.2, Z3n, CVC4-uc, SMTInterpol

QF_BV

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.22018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc, Z3n
Parallel PerformanceYices 2.6.22018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc, Z3n

QF_LIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, Z3n, 2018-SMTInterpol (unsat core)n, SMTInterpol, CVC4-uc
Parallel PerformanceYices 2.6.2Yices 2.6.2, Z3n, 2018-SMTInterpol (unsat core)n, SMTInterpol, CVC4-uc

QF_LIRA

Scoring SchemeWinnerRanking
Sequential Performance-Z3n, 2018-Z3 (unsat core)n, Yices 2.6.2, CVC4-uc, SMTInterpol
Parallel Performance-Z3n, 2018-Z3 (unsat core)n, Yices 2.6.2, CVC4-uc, SMTInterpol

QF_LRA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, CVC4-uc, 2018-SMTInterpol (unsat core)n, Z3n, SMTInterpol
Parallel PerformanceYices 2.6.2Yices 2.6.2, CVC4-uc, 2018-SMTInterpol (unsat core)n, Z3n, SMTInterpol

QF_NIA

Scoring SchemeWinnerRanking
Sequential PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, 2018-Z3 (unsat core)n, Z3n, CVC4-uc
Parallel PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, 2018-Z3 (unsat core)n, Z3n, CVC4-uc

QF_NIRA

Scoring SchemeWinnerRanking
Sequential PerformanceMathSAT-na-extMathSAT-na-ext, MathSAT-default, Z3n, 2018-Z3 (unsat core)n, CVC4-uc
Parallel PerformanceMathSAT-na-extMathSAT-na-ext, MathSAT-default, Z3n, 2018-Z3 (unsat core)n, CVC4-uc

QF_NRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, MathSAT-default, MathSAT-na-ext, Z3n

QF_UF

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, SMTInterpol, Z3n, CVC4-uc, 2018-CVC4 (unsat core)n
Parallel PerformanceYices 2.6.2Yices 2.6.2, SMTInterpol, Z3n, CVC4-uc, 2018-CVC4 (unsat core)n

QF_UFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.22018-Z3 (unsat core)n, Z3n, Yices 2.6.2, CVC4-uc
Parallel PerformanceYices 2.6.22018-Z3 (unsat core)n, Z3n, Yices 2.6.2, CVC4-uc

QF_UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Yices (unsat core)n, CVC4-uc, Z3n, SMTInterpol
Parallel PerformanceYices 2.6.22018-Yices (unsat core)n, Yices 2.6.2, CVC4-uc, Z3n, SMTInterpol

QF_UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices 2.6.2Yices 2.6.2, 2018-Z3 (unsat core)n, Z3n, SMTInterpol, CVC4-uc
Parallel PerformanceYices 2.6.2Yices 2.6.2, 2018-Z3 (unsat core)n, Z3n, SMTInterpol, CVC4-uc

QF_UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucZ3n, 2018-MathSAT (unsat core)n, CVC4-uc, Yices 2.6.2, SMTInterpol
Parallel PerformanceCVC4-ucZ3n, 2018-MathSAT (unsat core)n, CVC4-uc, Yices 2.6.2, SMTInterpol

QF_UFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceMathSAT-default2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc
Parallel PerformanceMathSAT-default2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc

QF_UFNRA

Scoring SchemeWinnerRanking
Sequential PerformanceMathSAT-default2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc
Parallel PerformanceMathSAT-default2018-Z3 (unsat core)n, Z3n, MathSAT-default, MathSAT-na-ext, CVC4-uc

UF

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+SMTInterpol
Parallel PerformanceCVC4-ucCVC4-uc, 2018-CVC4 (unsat core)n, Z3n, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4

UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4-uc2018-Z3 (unsat core)n, Z3n, CVC4-uc, UltimateEliminator+SMTInterpol, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4

UFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4
Parallel PerformanceCVC4-uc2018-CVC4 (unsat core)n, CVC4-uc, Z3n, UltimateEliminator+Yices-2.6.1, UltimateEliminator+MathSAT-5.5.4