QF_IDL (Model Validation Track)

Competition results for the QF_IDL logic in the Model Validation Track.

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

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

Winners

Sequential Performance	Parallel Performance
YicesLS	YicesLS

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
YicesLS	0	646	88765.195	88693.45	26	0
z3-mvn	0	634	92263.746	92237.453	57	0
2020-z3n	0	629	92759.529	92761.639	58	0
2020-Yices2-fixed Model Validationn	0	625	92467.129	92464.807	66	0
2020-Yices2 Model Validationn	0	625	92499.602	92456.038	66	0
Yices2 model-validation	0	624	94214.12	94184.718	67	0
cvc5-mv	0	552	232814.633	232838.647	139	0
OpenSMT	0	530	236298.731	236266.01	161	0
SMTInterpol	0	437	367153.366	361140.083	254	0
MathSAT5n	0	421	353395.498	353438.915	260	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
YicesLS	0	646	88774.955	88692.42	34	0
z3-mvn	0	634	92271.066	92235.063	57	0
2020-z3n	0	629	92769.049	92758.949	58	0
2020-Yices2 Model Validationn	0	625	92506.742	92453.688	66	0
2020-Yices2-fixed Model Validationn	0	625	92472.049	92462.617	66	0
Yices2 model-validation	0	624	94221.29	94182.838	67	0
cvc5-mv	0	552	232842.693	232833.567	139	0
OpenSMT	0	530	236312.521	236261.39	161	0
SMTInterpol	0	439	367199.626	361056.673	252	0
MathSAT5n	0	421	353438.898	353428.475	260	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.