QF_LinearRealArith (Proof Exhibition Track)

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

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

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

Logics:

• QF_LRA : 349 benchmarks
• QF_RDL : 113 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
veriT	0	411	44856.387	44723.286	51	0	20	0
smtinterpol	0	392	127193.655	119049.625	70	0	73	0
cvc5-lfsc	0	358	164361.016	164319.133	104	0	104	0
OpenSMT	0	344	16751.743	16726.595	5	113	5	0
cvc5	0	122	399948.695	399921.196	340	0	325	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Unsolved	Abstained	Timeout	Memout
veriT	0	411	44862.247	44704.536	51	0	19	0
smtinterpol	0	392	127624.725	118590.84	70	0	70	0
cvc5-lfsc	0	358	164387.126	164315.063	104	0	104	0
OpenSMT	0	344	16752.553	16726.285	5	113	5	0
cvc5	0	122	400020.795	399904.276	340	0	325	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.