QF_Equality (Model Validation Track)

Competition results for the QF_Equality division in the Model Validation Track.

Page generated on 2021-07-18 17:31:50 +0000

Benchmarks: 1571
Time Limit: 1200 seconds
Memory Limit: 60 GB

Logics:

• QF_UF : 1571 benchmarks

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Yices2 model-validation	0	1571	73.098	77.224		0	0
OpenSMT	0	1571	562.781	572.429		0	0
cvc5-mv	0	1571	731.025	728.436		0	0
SMTInterpol	0	1571	4841.795	1974.791		0	0
z3-mvn	0	1555	243.214	232.262		0	0
MathSAT5n	0	640	227.882	226.947		0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Yices2 model-validation	0	1571	73.098	77.224		0	0
OpenSMT	0	1571	562.781	572.429		0	0
cvc5-mv	0	1571	731.025	728.436		0	0
SMTInterpol	0	1571	4841.795	1974.791		0	0
z3-mvn	0	1555	243.214	232.262		0	0
MathSAT5n	0	640	227.882	226.947		0	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.