QF_LinearIntArith (Proof Exhibition Track)

Competition results for the QF_LinearIntArith division in the Proof Exhibition Track.

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

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

Logics:

• QF_IDL : 458 benchmarks
• QF_LIA : 2377 benchmarks
• QF_LIRA : 5 benchmarks

This track 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	Unsolved	Abstained	Timeout	Memout
smtinterpol	0	2534	634348.529	564671.468	306	0	317	0
OpenSMT	0	2023	229537.564	229128.362	354	463	68	0
veriT	0	1786	1188627.8	1188370.693	1054	0	923	1
cvc5-lfsc	0	1542	1618509.902	1618912.915	1298	0	1290	0
cvc5	0	899	2302105.063	2302394.657	1941	0	1898	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Unsolved	Abstained	Timeout	Memout
smtinterpol	0	2534	656059.149	560314.077	306	0	293	0
OpenSMT	0	2023	229554.504	229126.082	354	463	68	0
veriT	0	1786	1188722.09	1188334.613	1054	0	923	1
cvc5-lfsc	0	1542	1618958.092	1618843.995	1298	0	1290	0
cvc5	0	899	2302658.513	2302289.887	1941	0	1897	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.