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

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

QF_ADT+BitVec

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential PerformanceBitwuzla Fixedn, Bitwuzla, cvc5, Yices2
Parallel PerformanceBitwuzla Fixedn, Bitwuzla, cvc5, Yices2

QF_ADT+LinArith

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential PerformanceSMTInterpol, cvc5, Yices2
Parallel PerformanceSMTInterpol, cvc5, Yices2

QF_Array+Bitvec+LinArith

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential Performancecvc5, Bitwuzla Fixedn, Bitwuzla, SMTInterpol, Yices2
Parallel Performancecvc5, Bitwuzla Fixedn, Bitwuzla, SMTInterpol, Yices2

QF_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceSTPBitwuzla Fixedn, STP, Bitwuzla, 2020-Bitwuzlan, Yices2, cvc5
Parallel PerformanceSTPSTP, Bitwuzla Fixedn, Bitwuzla, 2020-Bitwuzlan, Yices2, cvc5

QF_Datatypes

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential PerformanceSMTInterpol, cvc5
Parallel PerformanceSMTInterpol, cvc5

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, Yices2, cvc5
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, Yices2, cvc5

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpol2022-smtinterpoln, SMTInterpol, OpenSMT, cvc5, Yices2
Parallel PerformanceSMTInterpol2022-smtinterpoln, SMTInterpol, OpenSMT, cvc5, Yices2

QF_Equality+NonLinearArith

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential Performancecvc5, Yices2
Parallel Performancecvc5, Yices2

QF_Equality

Scoring SchemeWinnerRanking
Sequential PerformanceYices22021-Yices2 model-validationn, 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol
Parallel PerformanceYices22021-Yices2 model-validationn, 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol

QF_FPArith

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential PerformanceBitwuzla, Bitwuzla Fixedn, cvc5, 2022-Bitwuzlan
Parallel PerformanceBitwuzla, Bitwuzla Fixedn, cvc5, 2022-Bitwuzlan

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceZ3++Z3++, 2022-Z3++n, OpenSMT, cvc5, Yices2, SMTInterpol
Parallel PerformanceZ3++Z3++, 2022-Z3++n, OpenSMT, cvc5, Yices2, SMTInterpol

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceOpenSMT2022-OpenSMTn, OpenSMT, Yices2, cvc5, SMTInterpol, Yaga
Parallel PerformanceOpenSMT2022-OpenSMTn, OpenSMT, Yices2, cvc5, SMTInterpol, Yaga

QF_NonLinearIntArith

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential PerformanceZ3++, ismt, Yices2, cvc5
Parallel PerformanceZ3++, ismt, Yices2, cvc5

QF_NonLinearRealArith

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Scoring SchemeRanking
Sequential PerformanceZ3++, SMT-RAT-MCSAT, Yices2, cvc5, cvc5-NRA-LS
Parallel PerformanceZ3++, SMT-RAT-MCSAT, Yices2, cvc5, cvc5-NRA-LS