QF_Equality+LinearArith (Proof Exhibition Track)

Competition results for the QF_Equality+LinearArith division in the Proof Exhibition Track.

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

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

Logics:

• QF_ALIA : 72 benchmarks
• QF_AUFLIA : 380 benchmarks
• QF_UFDTLIRA : 66 benchmarks
• QF_UFIDL : 300 benchmarks
• QF_UFLIA : 183 benchmarks
• QF_UFLRA : 300 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	1213	123812.858	116123.787	88	0	89	0
cvc5-lfsc	0	1029	355020.373	355027.728	272	0	271	0
veriT	0	610	133882.861	133734.519	625	66	93	6
cvc5	0	423	1041022.744	1040986.558	878	0	860	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Unsolved	Abstained	Timeout	Memout
smtinterpol	0	1213	127133.528	115536.361	88	0	86	0
cvc5-lfsc	0	1029	355067.953	355017.788	272	0	271	0
veriT	0	610	133911.351	133723.439	625	66	92	6
cvc5	0	423	1041155.484	1040946.028	878	0	860	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.