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 Scheme	Winner	Ranking
Sequential Performance	Bitwuzla	Bitwuzla, Bitwuzla-fixedn, Yices2-fixed Model Validationn, 2019-Boolectorn, CVC4-mv, STP + MergeSAT, STP + CMS, z3n, Yices2 Model Validation, MathSAT5-mvn
Parallel Performance	Bitwuzla	Bitwuzla, 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 Scheme	Ranking
Sequential Performance	Yices2 Model Validation, Yices2-fixed Model Validationn, z3n, CVC4-mv, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn
Parallel Performance	Yices2 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 Scheme	Ranking
Sequential Performance	z3n, CVC4-mv, Yices2 Model Validation, Yices2-fixed Model Validationn, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn
Parallel Performance	z3n, 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 Scheme	Ranking
Sequential Performance	Yices2-fixed Model Validationn, Yices2 Model Validation, z3n, CVC4-mv, MathSAT5-mvn, SMTInterpol, SMTInterpol-fixedn
Parallel Performance	Yices2-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 Scheme	Ranking
Sequential Performance	OpenSMT, Yices2 Model Validation, Yices2-fixed Model Validationn, z3n, CVC4-mv, SMTInterpol-fixedn, SMTInterpol, MathSAT5-mvn
Parallel Performance	OpenSMT, 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 Scheme	Ranking
Sequential Performance	Yices2-fixed Model Validationn, Yices2 Model Validation, CVC4-mv, MathSAT5-mvn, z3n, SMTInterpol, SMTInterpol-fixedn
Parallel Performance	Yices2-fixed Model Validationn, Yices2 Model Validation, CVC4-mv, MathSAT5-mvn, z3n, SMTInterpol, SMTInterpol-fixedn