QF_Equality+LinearArith (Model Validation Track)

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

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

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

Logics:

• QF_UFIDL : 206 benchmarks
• QF_UFLRA : 385 benchmarks
• QF_UFLIA : 300 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
SMTInterpol	0	881	28445.216	24623.824		10	0
cvc5-mv	0	850	74185.333	74201.757		41	0
Yices2 model-validation	0	823	95678.224	95687.953		68	0
z3-mvn	0	715	61802.643	61576.737		43	0
MathSAT5n	0	553	124758.838	124784.412		102	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
SMTInterpol	0	882	28458.246	24619.214		9	0
cvc5-mv	0	850	74194.323	74199.757		41	0
Yices2 model-validation	0	823	95685.674	95685.633		68	0
z3-mvn	0	715	61807.143	61574.987		43	0
MathSAT5n	0	553	124781.208	124779.912		102	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.