QF_LinearIntArith (Model Validation Track)

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

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

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

Logics:

• QF_IDL : 691 benchmarks
• QF_LIA : 1923 benchmarks
• QF_LIRA : 1 benchmarks

Winners

Sequential Performance	Parallel Performance
cvc5-mv	cvc5-mv

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
2020-z3n	0	2449	331938.894	331798.953		151	0
z3-mvn	0	2341	457166.028	457088.896		274	0
cvc5-mv	0	2307	530224.611	530212.91		308	0
2020-Yices2-fixed Model Validationn	0	2264	469273.287	469284.686		351	0
2020-Yices2 Model Validationn	0	2264	469313.415	469252.339		351	0
Yices2 model-validation	0	2259	475170.794	475163.536		356	0
MathSAT5n	0	2252	557628.331	557629.529		340	0
SMTInterpol	0	2042	866663.53	840408.306		573	0
OpenSMT	0	1752	1107591.294	1213206.21		389	0
YicesLS	0	646	88765.195	88693.45		26	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
2020-z3n	0	2449	331961.694	331792.963		151	0
z3-mvn	0	2341	457203.268	457077.756		274	0
cvc5-mv	0	2307	530266.721	530203.05		308	0
2020-Yices2 Model Validationn	0	2264	469342.955	469240.789		351	0
2020-Yices2-fixed Model Validationn	0	2264	469300.027	469273.246		351	0
Yices2 model-validation	0	2259	475198.484	475155.116		356	0
MathSAT5n	0	2252	557681.151	557616.019		340	0
SMTInterpol	0	2045	867407.81	840160.806		570	0
OpenSMT	0	1752	1133519.268	1213191.6		389	0
YicesLS	0	646	88774.955	88692.42		34	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.