SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

SMT-COMP 2022 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 Performancecvc5cvc5, 2020-CVC4-ucn, z3-4.8.17n, Vampire, smtinterpol, UltimateEliminator+MathSAT
Parallel Performancecvc5cvc5, 2020-CVC4-ucn, z3-4.8.17n, Vampire, smtinterpol, UltimateEliminator+MathSAT

Bitvec

Scoring SchemeWinnerRanking
Sequential Performancecvc52020-CVC4-ucn, cvc5, z3-4.8.17n, UltimateEliminator+MathSAT
Parallel Performancecvc52020-CVC4-ucn, cvc5, z3-4.8.17n, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc52021-cvc5-ucn, z3-4.8.17n, cvc5, Vampire, smtinterpol, UltimateEliminator+MathSAT
Parallel Performancecvc52021-cvc5-ucn, z3-4.8.17n, cvc5, Vampire, smtinterpol, UltimateEliminator+MathSAT

Equality+MachineArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5z3-4.8.17n, cvc5, 2021-cvc5-ucn, UltimateEliminator+MathSAT
Parallel Performancecvc5z3-4.8.17n, cvc5, 2021-cvc5-ucn, UltimateEliminator+MathSAT

Equality+NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc52020-CVC4-ucn, cvc5, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT
Parallel Performancecvc52020-CVC4-ucn, cvc5, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT

Equality

Scoring SchemeWinnerRanking
Sequential Performancecvc52020-CVC4-ucn, cvc5, Vampire, z3-4.8.17n, smtinterpol, UltimateEliminator+MathSAT
Parallel PerformanceVampireVampire, 2020-CVC4-ucn, cvc5, z3-4.8.17n, smtinterpol, UltimateEliminator+MathSAT

FPArith

Scoring SchemeWinnerRanking
Sequential Performance-2020-CVC4-ucn, z3-4.8.17n, UltimateEliminator+MathSAT, cvc5
Parallel Performance-2020-CVC4-ucn, z3-4.8.17n, UltimateEliminator+MathSAT, cvc5

QF_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, 2020-Bitwuzla-fixedn, Yices2, z3-4.8.17n, cvc5, MathSATn
Parallel PerformanceBitwuzlaBitwuzla, 2020-Bitwuzla-fixedn, Yices2, z3-4.8.17n, cvc5, MathSATn

QF_Datatypes

Scoring SchemeWinnerRanking
Sequential Performancecvc5z3-4.8.17n, 2021-z3n, cvc5, smtinterpol
Parallel Performancecvc5z3-4.8.17n, 2021-z3n, cvc5, smtinterpol

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, 2021-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn
Parallel PerformanceBitwuzlaBitwuzla, 2021-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, MathSATn, 2021-MathSAT5n, z3-4.8.17n, smtinterpol, cvc5
Parallel PerformanceYices2Yices2, MathSATn, 2021-MathSAT5n, z3-4.8.17n, smtinterpol, cvc5

QF_Equality+NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancesmtinterpol2021-cvc5-ucn, smtinterpol, MathSATn, z3-4.8.17n, cvc5
Parallel Performancesmtinterpol2021-cvc5-ucn, smtinterpol, MathSATn, z3-4.8.17n, cvc5

QF_Equality

Scoring SchemeWinnerRanking
Sequential PerformanceYices2z3-4.8.17n, 2021-z3n, Yices2, MathSATn, smtinterpol, cvc5
Parallel PerformanceYices2z3-4.8.17n, 2021-z3n, Yices2, MathSATn, smtinterpol, cvc5

QF_FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaz3-4.8.17n, Bitwuzla, 2021-Bitwuzlan, cvc5, MathSATn
Parallel PerformanceBitwuzlaz3-4.8.17n, Bitwuzla, 2021-Bitwuzlan, cvc5, MathSATn

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2MathSATn, Yices2, z3-4.8.17n, 2021-cvc5-ucn, smtinterpol, cvc5
Parallel PerformanceYices2MathSATn, Yices2, z3-4.8.17n, 2021-cvc5-ucn, smtinterpol, cvc5

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices22020-Yices2n, Yices2, cvc5, z3-4.8.17n, MathSATn, smtinterpol
Parallel PerformanceYices22020-Yices2n, Yices2, cvc5, z3-4.8.17n, smtinterpol, MathSATn