QF_LinearIntArith (Model Validation Track)

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

Page generated on 2022-08-10 11:19:11 +0000

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

Logics:

• QF_IDL : 743 benchmarks
• QF_LIA : 4196 benchmarks
• QF_LIRA : 1 benchmarks

Winners

Sequential Performance	Parallel Performance
Z3++	Z3++

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Z3++	0	4762	332828.245	333903.963		165	6
2020-z3n	0	4733	394915.693	394789.006		188	2
z3-4.8.17n	0	4698	409492.92	409192.407		240	2
OpenSMT	0	4590	708462.598	708387.132		348	0
Yices2	0	4557	536617.987	536595.394		383	0
cvc5	0	4554	631309.776	631299.719		385	0
MathSATn	0	4477	667617.179	667610.936		437	0
smtinterpol	0	4262	1014716.304	984274.658		678	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Z3++	0	4762	332852.845	333897.413		165	6
2020-z3n	0	4733	394945.643	394780.196		188	2
z3-4.8.17n	0	4698	409514.15	409184.857		240	2
OpenSMT	0	4590	708497.928	708374.352		348	0
Yices2	0	4557	536651.157	536583.814		383	0
cvc5	0	4554	631377.756	631283.769		385	0
MathSATn	0	4477	667673.659	667593.876		437	0
smtinterpol	0	4262	1014716.304	984274.658		678	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.