SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

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

SMT-COMP 2023 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, 2022-cvc5n, SMTInterpol, Vampire, UltimateEliminator+MathSAT
Parallel Performancecvc5cvc5, 2022-cvc5n, SMTInterpol, Vampire, UltimateEliminator+MathSAT

Bitvec

Scoring SchemeWinnerRanking
Sequential Performancecvc52020-CVC4-ucn, cvc5, Bitwuzla, Bitwuzla Fixedn, UltimateEliminator+MathSAT
Parallel Performancecvc52020-CVC4-ucn, cvc5, Bitwuzla, Bitwuzla Fixedn, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc52021-cvc5-ucn, cvc5, SMTInterpol, Vampire, UltimateEliminator+MathSAT
Parallel Performancecvc52021-cvc5-ucn, cvc5, SMTInterpol, Vampire, UltimateEliminator+MathSAT

Equality+MachineArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, 2022-z3-4.8.17n, Bitwuzla Fixedn, Bitwuzla, UltimateEliminator+MathSAT
Parallel Performancecvc5cvc5, 2022-z3-4.8.17n, Bitwuzla Fixedn, Bitwuzla, UltimateEliminator+MathSAT

Equality+NonLinearArith

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

Equality

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, 2020-CVC4-ucn, 2022-Vampiren, SMTInterpol, Yices2, UltimateEliminator+MathSAT, Vampire
Parallel Performancecvc52022-Vampiren, cvc5, 2020-CVC4-ucn, SMTInterpol, Yices2, UltimateEliminator+MathSAT, Vampire

FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzla2020-CVC4-ucn, Bitwuzla, Bitwuzla Fixedn, cvc5, UltimateEliminator+MathSAT
Parallel PerformanceBitwuzla2020-CVC4-ucn, Bitwuzla, Bitwuzla Fixedn, cvc5, UltimateEliminator+MathSAT

QF_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceYices22022-Bitwuzlan, Bitwuzla Fixedn, Yices2, cvc5, Bitwuzla
Parallel PerformanceYices22022-Bitwuzlan, Bitwuzla Fixedn, Yices2, cvc5, Bitwuzla

QF_Datatypes

Scoring SchemeWinnerRanking
Sequential Performancecvc52022-z3-4.8.17n, cvc5, SMTInterpol
Parallel PerformanceSMTInterpol2022-z3-4.8.17n, SMTInterpol, cvc5

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceYices22022-Bitwuzlan, Yices2, Bitwuzla Fixedn, cvc5, Bitwuzla
Parallel PerformanceYices22022-Bitwuzlan, Yices2, Bitwuzla Fixedn, cvc5, Bitwuzla

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices22022-Yices2n, Yices2, cvc5, SMTInterpol
Parallel PerformanceYices22022-Yices2n, Yices2, cvc5, SMTInterpol

QF_Equality+NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc52021-cvc5-ucn, cvc5, SMTInterpol
Parallel Performancecvc52021-cvc5-ucn, cvc5, SMTInterpol

QF_Equality

Scoring SchemeWinnerRanking
Sequential PerformanceYices22022-z3-4.8.17n, Yices2, SMTInterpol, cvc5
Parallel PerformanceYices22022-z3-4.8.17n, Yices2, SMTInterpol, cvc5

QF_FPArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5Bitwuzla Fixedn, cvc5, 2022-z3-4.8.17n, Bitwuzla
Parallel Performancecvc5Bitwuzla Fixedn, cvc5, 2022-z3-4.8.17n, Bitwuzla

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, 2022-MathSATn, cvc5, SMTInterpol
Parallel PerformanceYices2Yices2, 2022-MathSATn, cvc5, SMTInterpol

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices22020-Yices2n, Yices2, cvc5, SMTInterpol
Parallel PerformanceYices22020-Yices2n, Yices2, cvc5, SMTInterpol