SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

SMT-COMP 2020 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_BV

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, Yices2-fixed Model Validationn, 2019-Boolectorn, CVC4-mv, STP + MergeSAT, STP + CMS, z3n, Yices2 Model Validation, MathSAT5-mvn
Parallel PerformanceBitwuzlaBitwuzla, Bitwuzla-fixedn, Yices2-fixed Model Validationn, 2019-Boolectorn, STP + CMS, CVC4-mv, STP + MergeSAT, z3n, Yices2 Model Validation, MathSAT5-mvn

QF_IDL

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

Scoring SchemeRanking
Sequential PerformanceYices2 Model Validation, Yices2-fixed Model Validationn, z3n, CVC4-mv, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn
Parallel PerformanceYices2 Model Validation, Yices2-fixed Model Validationn, z3n, CVC4-mv, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn

QF_LIA

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

Scoring SchemeRanking
Sequential Performancez3n, CVC4-mv, Yices2 Model Validation, Yices2-fixed Model Validationn, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn
Parallel Performancez3n, CVC4-mv, Yices2 Model Validation, Yices2-fixed Model Validationn, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn

QF_LIRA

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

Scoring SchemeRanking
Sequential PerformanceYices2-fixed Model Validationn, Yices2 Model Validation, z3n, CVC4-mv, MathSAT5-mvn, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceYices2-fixed Model Validationn, Yices2 Model Validation, z3n, CVC4-mv, MathSAT5-mvn, SMTInterpol, SMTInterpol-fixedn

QF_LRA

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

Scoring SchemeRanking
Sequential PerformanceOpenSMT, Yices2 Model Validation, Yices2-fixed Model Validationn, z3n, CVC4-mv, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn
Parallel PerformanceOpenSMT, Yices2 Model Validation, Yices2-fixed Model Validationn, z3n, CVC4-mv, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn

QF_RDL

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

Scoring SchemeRanking
Sequential PerformanceYices2-fixed Model Validationn, Yices2 Model Validation, CVC4-mv, MathSAT5-mvn, z3n, SMTInterpol, SMTInterpol-fixedn
Parallel PerformanceYices2-fixed Model Validationn, Yices2 Model Validation, CVC4-mv, MathSAT5-mvn, z3n, SMTInterpol, SMTInterpol-fixedn