QF_LinearRealArith (Single Query Track)

Competition results for the QF_LinearRealArith division in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

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

Logics:

• QF_LRA : 578 benchmarks
• QF_RDL : 247 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices2	Yices2	OpenSMT	cvc5	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2021-Yices2n	0	748	36425.096	36381.061	748	417	331	77	0	77	0
2022-Yices2n	0	748	36530.075	36456.995	748	417	331	77	0	77	0
Yices2	0	748	37997.879	37988.53	748	417	331	77	0	77	0
OpenSMT	0	746	41154.822	41118.111	746	419	327	79	0	79	0
cvc5	0	746	44456.811	44609.493	746	411	335	79	0	79	0
SMTInterpol	0	650	80410.649	68597.328	650	382	268	175	0	175	0
Yaga	0	408	31066.564	31072.422	408	243	165	170	247	170	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2021-Yices2n	0	748	36425.096	36381.061	748	417	331	77	0	77	0
2022-Yices2n	0	748	36530.075	36456.995	748	417	331	77	0	77	0
Yices2	0	748	37997.879	37988.53	748	417	331	77	0	77	0
OpenSMT	0	746	41154.822	41118.111	746	419	327	79	0	79	0
cvc5	0	746	44456.811	44609.493	746	411	335	79	0	79	0
SMTInterpol	0	654	86622.889	73016.908	654	384	270	171	0	171	0
Yaga	0	408	31066.564	31072.422	408	243	165	170	247	170	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	419	24762.591	24745.159	419	419	0	22	384	79	0
2021-Yices2n	0	417	16302.853	16303.618	417	417	0	24	384	77	0
2022-Yices2n	0	417	16433.655	16411.886	417	417	0	24	384	77	0
Yices2	0	417	16755.819	16758.314	417	417	0	24	384	77	0
cvc5	0	411	24457.327	24597.904	411	411	0	30	384	79	0
SMTInterpol	0	384	44633.246	39333.018	384	384	0	57	384	171	0
Yaga	0	243	18681.405	18684.858	243	243	0	92	490	170	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	335	19999.484	20011.589	335	0	335	14	476	79	0
2022-Yices2n	0	331	20096.42	20045.11	331	0	331	18	476	77	0
2021-Yices2n	0	331	20122.243	20077.443	331	0	331	18	476	77	0
Yices2	0	331	21242.06	21230.215	331	0	331	18	476	77	0
OpenSMT	0	327	16392.231	16372.952	327	0	327	22	476	79	0
SMTInterpol	0	270	41989.643	33683.89	270	0	270	79	476	171	0
Yaga	0	165	12385.159	12387.564	165	0	165	75	585	170	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2022-Yices2n	0	607	1406.18	1353.21	607	357	250	218	0	218	0
2021-Yices2n	0	606	1352.783	1328.763	606	357	249	219	0	219	0
Yices2	0	606	1373.24	1359.849	606	357	249	219	0	219	0
OpenSMT	0	570	1910.144	1868.463	570	316	254	255	0	255	0
cvc5	0	514	1888.902	1885.022	514	289	225	311	0	311	0
SMTInterpol	0	398	4378.156	1895.025	398	245	153	427	0	427	0
Yaga	0	292	830.658	831.445	292	175	117	286	247	286	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.