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 - 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, SMTInterpol

Bitvec

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

Equality+LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc52021-z3n, cvc5, SMTInterpol, UltimateEliminator+MathSAT

Equality+MachineArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, cvc5, 2022-UltimateEliminator+MathSATn, UltimateEliminator+MathSAT

Equality+NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc52022-z3-4.8.17n, cvc5, SMTInterpol, UltimateEliminator+MathSAT

Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc52020-z3n, cvc5, SMTInterpol, UltimateEliminator+MathSAT, Yices2, Yices2 Fixedn

FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, 2022-Bitwuzlan, cvc5, UltimateEliminator+MathSAT

QF_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Yices2 Fixedn, Yices2, 2022-Yices2n, STP, cvc5

QF_Equality+Bitvec+Arith

Scoring SchemeWinnerRanking
Parallel Performancecvc5Yices2 Fixedn, cvc5, Yices2

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Yices2 Fixedn, Yices2, 2022-Yices2n, cvc5

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpol2020-z3n, SMTInterpol, cvc5, Yices2 Fixedn, Yices2, OpenSMT

QF_Equality+NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc52022-z3-4.8.17n, cvc5, SMTInterpol, Yices2, Yices2 Fixedn

QF_Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, Yices2 Fixedn, Yices2, 2022-Yices2n, OpenSMT

QF_FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, 2022-Bitwuzlan, cvc5

QF_LinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceYices22021-Yices2 incrementaln, Yices2 Fixedn, Yices2, SMTInterpol, cvc5, OpenSMT

QF_LinearRealArith

Scoring SchemeWinnerRanking
Parallel PerformanceOpenSMT2018-MathSAT-incrementaln, OpenSMT, Yices2 Fixedn, Yices2, cvc5, SMTInterpol

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpol2021-MathSAT5n, SMTInterpol, cvc5, Yices2 Fixedn, Yices2