QF_LinearIntArith (Model Validation Track)

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

Page generated on 2023-07-06 16:06:00 +0000

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

Logics:

• QF_IDL : 745 benchmarks
• QF_LIA : 4212 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	4767	115200.111	114984.689		171	8
2022-Z3++n	0	4766	113200.285	113027.729		171	8
OpenSMT	0	4597	265005.021	264957.845		355	0
cvc5	0	4568	154352.175	154195.064		386	0
Yices2	0	4565	82018.756	81906.774		390	0
SMTInterpol	0	4269	216584.218	187123.22		685	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Z3++	0	4767	115200.111	114984.689		171	8
2022-Z3++n	0	4766	113200.285	113027.729		171	8
OpenSMT	0	4597	265005.021	264957.845		355	0
cvc5	0	4568	154352.175	154195.064		386	0
Yices2	0	4565	82018.756	81906.774		390	0
SMTInterpol	0	4271	219014.858	189465.56		683	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.