SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

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

Arith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uc2020-CVC4-ucn, z3n, cvc5-uc, Vampire, SMTInterpol-remus, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performancecvc5-uc2020-CVC4-ucn, z3n, cvc5-uc, Vampire, SMTInterpol-remus, SMTInterpol, UltimateEliminator+MathSAT

Bitvec

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, z3n, UltimateEliminator+MathSAT
Parallel Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, z3n, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uccvc5-uc, 2020-CVC4-ucn, 2020-z3n, z3n, SMTInterpol, SMTInterpol-remus, UltimateEliminator+MathSAT, Vampire
Parallel Performancecvc5-uccvc5-uc, 2020-CVC4-ucn, 2020-z3n, z3n, SMTInterpol, SMTInterpol-remus, UltimateEliminator+MathSAT, Vampire

Equality+MachineArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uccvc5-uc, 2020-CVC4-ucn, z3n, UltimateEliminator+MathSAT
Parallel Performancecvc5-uccvc5-uc, 2020-CVC4-ucn, z3n, UltimateEliminator+MathSAT

Equality+NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, Vampire, z3n, UltimateEliminator+MathSAT, SMTInterpol
Parallel Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, Vampire, z3n, UltimateEliminator+MathSAT, SMTInterpol

Equality

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, z3n, SMTInterpol, SMTInterpol-remus, UltimateEliminator+MathSAT, Vampire
Parallel Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, z3n, SMTInterpol, SMTInterpol-remus, UltimateEliminator+MathSAT, Vampire

FPArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, UltimateEliminator+MathSAT
Parallel Performancecvc5-uc2020-CVC4-ucn, cvc5-uc, UltimateEliminator+MathSAT

QF_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzla2020-Bitwuzla-fixedn, Bitwuzla, cvc5-uc, Yices2, z3n, MathSAT5n
Parallel PerformanceBitwuzla2020-Bitwuzla-fixedn, Bitwuzla, cvc5-uc, Yices2, z3n, MathSAT5n

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, cvc5-uc, z3n, 2020-Yices2n, Yices2, 2020-z3n, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla, cvc5-uc, z3n, 2020-Yices2n, Yices2, 2020-z3n, MathSAT5n

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2MathSAT5n, 2020-Yices2-fixedn, Yices2, 2020-z3n, SMTInterpol, SMTInterpol-remus, z3n, 2020-CVC4-ucn, cvc5-uc
Parallel PerformanceYices2MathSAT5n, 2020-Yices2-fixedn, Yices2, 2020-z3n, SMTInterpol-remus, SMTInterpol, z3n, 2020-CVC4-ucn, cvc5-uc

QF_Equality+NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uccvc5-uc, MathSAT5n, z3n, Yices2
Parallel Performancecvc5-uccvc5-uc, MathSAT5n, z3n, Yices2

QF_Equality

Scoring SchemeWinnerRanking
Sequential Performancecvc5-ucz3n, cvc5-uc, SMTInterpol, 2020-Yices2-fixedn, Yices2, 2020-SMTInterpol-fixedn, MathSAT5n, SMTInterpol-remus
Parallel Performancecvc5-ucz3n, cvc5-uc, SMTInterpol, SMTInterpol-remus, 2020-Yices2-fixedn, Yices2, 2020-SMTInterpol-fixedn, MathSAT5n

QF_FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, 2020-Bitwuzlan, 2020-Bitwuzla-fixedn, cvc5-uc, z3n, MathSAT5n
Parallel PerformanceBitwuzlaBitwuzla, 2020-Bitwuzlan, 2020-Bitwuzla-fixedn, cvc5-uc, z3n, MathSAT5n

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uccvc5-uc, MathSAT5n, SMTInterpol, Yices2, 2020-Yices2-fixedn, z3n, SMTInterpol-remus
Parallel Performancecvc5-uccvc5-uc, MathSAT5n, SMTInterpol, Yices2, 2020-Yices2-fixedn, z3n, SMTInterpol-remus

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices22020-Yices2n, Yices2, cvc5-uc, z3n, MathSAT5n, SMTInterpol, SMTInterpol-remus
Parallel PerformanceYices22020-Yices2n, Yices2, cvc5-uc, z3n, MathSAT5n, SMTInterpol, SMTInterpol-remus

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-ucz3n, MathSAT5n, cvc5-uc, Yices2
Parallel Performancecvc5-ucz3n, MathSAT5n, cvc5-uc, Yices2

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-uccvc5-uc, MathSAT5n, z3n, Yices2
Parallel Performancecvc5-uccvc5-uc, MathSAT5n, z3n, Yices2