SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

SMT-COMP 2020 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).

AUFBVDTLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

AUFDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

AUFDTNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

AUFFPDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, z3n, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT

AUFLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucz3n, CVC4-uc, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucz3n, CVC4-uc, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT

AUFNIA

Scoring SchemeWinnerRanking
Sequential Performance-UltimateEliminator+MathSAT, CVC4-uc, z3n
Parallel Performance-UltimateEliminator+MathSAT, CVC4-uc, z3n

AUFNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT

BV

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT

BVFPLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

LIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT, SMTInterpol-fixedn, SMTInterpol
Parallel PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT, SMTInterpol-fixedn, SMTInterpol

NIA

Scoring SchemeWinnerRanking
Sequential Performance-CVC4-uc, z3n, UltimateEliminator+MathSAT
Parallel Performance-CVC4-uc, z3n, UltimateEliminator+MathSAT

QF_ABV

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaz3n, Bitwuzla, Yices2-fixedn, Yices2, Bitwuzla-fixedn, CVC4-uc, MathSAT5n
Parallel PerformanceBitwuzlaz3n, Bitwuzla, Yices2-fixedn, Yices2, Bitwuzla-fixedn, CVC4-uc, MathSAT5n

QF_ABVFP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, CVC4-uc, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, CVC4-uc, MathSAT5n

QF_ALIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucz3n, CVC4-uc, SMTInterpol-fixedn, SMTInterpol, MathSAT5n, Yices2-fixedn, Yices2
Parallel PerformanceCVC4-ucz3n, CVC4-uc, SMTInterpol-fixedn, SMTInterpol, MathSAT5n, Yices2-fixedn, Yices2

QF_AUFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, Yices2-fixedn, z3n, Bitwuzla, Bitwuzla-fixedn, CVC4-uc, MathSAT5n
Parallel PerformanceYices2Yices2, Yices2-fixedn, z3n, Bitwuzla, Bitwuzla-fixedn, CVC4-uc, MathSAT5n

QF_AUFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, Yices2-fixedn, Yices2, SMTInterpol, SMTInterpol-fixedn, MathSAT5n
Parallel PerformanceCVC4-ucCVC4-uc, z3n, Yices2-fixedn, Yices2, SMTInterpol-fixedn, SMTInterpol, MathSAT5n

QF_AX

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2-fixedn, Yices2, z3n, CVC4-uc, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceYices2Yices2-fixedn, Yices2, z3n, CVC4-uc, MathSAT5n, SMTInterpol, SMTInterpol-fixedn

QF_BV

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, Yices2-fixedn, Yices2, CVC4-uc, z3n, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, Yices2-fixedn, Yices2, CVC4-uc, z3n, MathSAT5n

QF_BVFP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, z3n, CVC4-uc, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, z3n, CVC4-uc, MathSAT5n

QF_FP

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, CVC4-uc, z3n, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, CVC4-uc, z3n, MathSAT5n

QF_LIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2-fixedn, Yices2, z3n, MathSAT5n, CVC4-uc, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceYices2Yices2-fixedn, Yices2, z3n, MathSAT5n, CVC4-uc, SMTInterpol, SMTInterpol-fixedn

QF_LIRA

Scoring SchemeWinnerRanking
Sequential Performance-z3n, Yices2-fixedn, Yices2, CVC4-uc, MathSAT5n, SMTInterpol, SMTInterpol-fixedn
Parallel Performance-z3n, Yices2-fixedn, Yices2, CVC4-uc, MathSAT5n, SMTInterpol-fixedn, SMTInterpol

QF_LRA

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, Yices2-fixedn, CVC4-uc, z3n, MathSAT5n, SMTInterpol-fixedn, SMTInterpol
Parallel PerformanceYices2Yices2, Yices2-fixedn, CVC4-uc, z3n, MathSAT5n, SMTInterpol-fixedn, SMTInterpol

QF_UF

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpolSMTInterpol-fixedn, SMTInterpol, z3n, Yices2-fixedn, Yices2, CVC4-uc, MathSAT5n
Parallel PerformanceSMTInterpolSMTInterpol-fixedn, SMTInterpol, z3n, Yices2-fixedn, Yices2, CVC4-uc, MathSAT5n

QF_UFBV

Scoring SchemeWinnerRanking
Sequential PerformanceYices2z3n, Yices2, Yices2-fixedn, Bitwuzla-fixedn, Bitwuzla, CVC4-uc, MathSAT5n
Parallel PerformanceYices2z3n, Yices2, Yices2-fixedn, Bitwuzla-fixedn, Bitwuzla, CVC4-uc, MathSAT5n

QF_UFFP

Scoring SchemeWinnerRanking
Sequential Performance-MathSAT5n, Bitwuzla, Bitwuzla-fixedn, CVC4-uc
Parallel Performance-MathSAT5n, Bitwuzla, Bitwuzla-fixedn, CVC4-uc

QF_UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2-fixedn, Yices2, CVC4-uc, MathSAT5n, z3n, SMTInterpol-fixedn, SMTInterpol
Parallel PerformanceYices2Yices2-fixedn, Yices2, CVC4-uc, MathSAT5n, z3n, SMTInterpol-fixedn, SMTInterpol

QF_UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2-fixedn, Yices2, MathSAT5n, z3n, SMTInterpol-fixedn, SMTInterpol, CVC4-uc
Parallel PerformanceYices2Yices2-fixedn, Yices2, MathSAT5n, z3n, SMTInterpol, SMTInterpol-fixedn, CVC4-uc

QF_UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucz3n, MathSAT5n, CVC4-uc, Yices2, Yices2-fixedn, SMTInterpol-fixedn, SMTInterpol
Parallel PerformanceCVC4-ucz3n, MathSAT5n, CVC4-uc, Yices2-fixedn, Yices2, SMTInterpol-fixedn, SMTInterpol

UF

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, z3n, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT

UFDT

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

UFDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

UFDTNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

UFFPDTLIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

UFFPDTNIRA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, UltimateEliminator+MathSAT

UFIDL

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucz3n, CVC4-uc, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucz3n, CVC4-uc, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT

UFLIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, z3n, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT

UFLRA

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpolz3n, SMTInterpol-fixedn, SMTInterpol, CVC4-uc, UltimateEliminator+MathSAT
Parallel PerformanceSMTInterpolz3n, SMTInterpol-fixedn, SMTInterpol, CVC4-uc, UltimateEliminator+MathSAT

UFNIA

Scoring SchemeWinnerRanking
Sequential PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT
Parallel PerformanceCVC4-ucCVC4-uc, z3n, UltimateEliminator+MathSAT