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

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

Arith

Scoring SchemeWinnerRanking
Parallel Performancecvc52021-cvc5-incn, cvc5, UltimateEliminator+MathSAT, z3-4.8.17n, smtinterpol

Bitvec

Scoring SchemeWinnerRanking
Parallel Performancecvc52019-Z3n, z3-4.8.17n, cvc5, Bitwuzla, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc52021-z3n, z3-4.8.17n, cvc5, smtinterpol, UltimateEliminator+MathSAT

Equality+MachineArith

Scoring SchemeWinnerRanking
Parallel PerformanceUltimateEliminator+MathSATUltimateEliminator+MathSAT, cvc5, Bitwuzla

Equality+NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5z3-4.8.17n, 2020-z3n, cvc5, smtinterpol, UltimateEliminator+MathSAT

Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc52020-z3n, z3-4.8.17n, cvc5, smtinterpol, UltimateEliminator+MathSAT

FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, cvc5, UltimateEliminator+MathSAT, 2019-CVC4-incn

QF_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, 2021-STPn, MathSATn, Bitwuzla, STP, cvc5, z3-4.8.17n

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, 2020-Yices2 incrementaln, z3-4.8.17n, MathSATn, cvc5, Bitwuzla

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Parallel Performancesmtinterpol2020-z3n, z3-4.8.17n, smtinterpol, cvc5, Yices2, MathSATn, OpenSMT

QF_Equality+NonLinearArith

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

QF_Equality

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, z3-4.8.17n, 2021-z3n, cvc5, smtinterpol, OpenSMT, MathSATn

QF_FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, MathSATn, cvc5, 2021-Bitwuzla - fixedn, z3-4.8.17n

QF_LinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceYices22021-Yices2 incrementaln, Yices2, z3-4.8.17n, MathSATn, smtinterpol, cvc5, OpenSMT

QF_LinearRealArith

Scoring SchemeWinnerRanking
Parallel PerformanceOpenSMT2018-MathSAT-incrementaln, MathSATn, OpenSMT, Yices2, cvc5, z3-4.8.17n, smtinterpol, solsmt

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Parallel Performancesmtinterpol2021-MathSAT5n, MathSATn, z3-4.8.17n, smtinterpol, cvc5, Yices2