SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

SMT-COMP 2021 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_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzla2020-Bitwuzlan, Bitwuzla, Yices2 model-validation, STP, cvc5-mv, z3-mvn, MathSAT5n
Parallel PerformanceBitwuzla2020-Bitwuzlan, Bitwuzla, Yices2 model-validation, STP, cvc5-mv, z3-mvn, MathSAT5n

QF_Equality+Bitvec

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

Scoring SchemeRanking
Sequential PerformanceYices2 model-validation, Bitwuzla, MathSAT5n, cvc5-mv, z3-mvn
Parallel PerformanceYices2 model-validation, Bitwuzla, MathSAT5n, cvc5-mv, z3-mvn

QF_Equality+LinearArith

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

Scoring SchemeRanking
Sequential PerformanceSMTInterpol, cvc5-mv, Yices2 model-validation, z3-mvn, MathSAT5n
Parallel PerformanceSMTInterpol, cvc5-mv, Yices2 model-validation, z3-mvn, MathSAT5n

QF_Equality

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

Scoring SchemeRanking
Sequential PerformanceYices2 model-validation, OpenSMT, cvc5-mv, SMTInterpol, z3-mvn, MathSAT5n
Parallel PerformanceYices2 model-validation, OpenSMT, cvc5-mv, SMTInterpol, z3-mvn, MathSAT5n

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5-mv2020-z3n, z3-mvn, cvc5-mv, 2020-Yices2-fixed Model Validationn, 2020-Yices2 Model Validationn, Yices2 model-validation, MathSAT5n, SMTInterpol, OpenSMT, YicesLS
Parallel Performancecvc5-mv2020-z3n, z3-mvn, cvc5-mv, 2020-Yices2 Model Validationn, 2020-Yices2-fixed Model Validationn, Yices2 model-validation, MathSAT5n, SMTInterpol, OpenSMT, YicesLS

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2 model-validationYices2 model-validation, OpenSMT, z3-mvn, 2020-Yices2-fixed Model Validationn, cvc5-mv, SMTInterpol, MathSAT5n, 2020-OpenSMTn
Parallel PerformanceYices2 model-validationYices2 model-validation, OpenSMT, z3-mvn, 2020-Yices2-fixed Model Validationn, cvc5-mv, SMTInterpol, MathSAT5n, 2020-OpenSMTn