QF_LinearRealArith (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +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	Yices2	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	750	117940.692	119643.153	750	429	321	75	0	75	0
Yices2	0	750	119545.138	119459.514	750	429	321	75	0	75	0
cvc5	0	745	144008.508	144362.489	745	420	325	80	0	80	0
OpenSMT	0	738	137400.525	137303.554	738	423	315	87	0	87	0
z3-4.8.17n	0	726	162780.461	162770.83	726	416	310	99	0	99	0
veriT	0	705	189366.081	189335.755	705	394	311	120	0	120	0
MathSATn	0	672	229157.873	229176.488	672	398	274	153	0	153	0
smtinterpol	0	655	289759.718	277705.373	655	401	254	170	0	170	0
solsmt	0	237	711620.364	715932.75	237	131	106	588	0	325	224

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	750	119550.888	119457.254	750	429	321	75	0	75	0
2021-Yices2n	0	750	119604.94	119639.733	750	429	321	75	0	75	0
cvc5	0	745	144284.078	144359.309	745	420	325	80	0	80	0
OpenSMT	0	738	137406.665	137300.614	738	423	315	87	0	87	0
z3-4.8.17n	0	726	162795.611	162766.91	726	416	310	99	0	99	0
veriT	0	705	189379.141	189331.475	705	394	311	120	0	120	0
MathSATn	0	672	229177.313	229170.688	672	398	274	153	0	153	0
smtinterpol	0	661	290658.688	277169.233	661	401	260	164	0	164	0
solsmt	0	237	711686.784	715918.01	237	131	106	588	0	325	224

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	429	33391.522	33348.462	429	429	0	18	378	75	0
2021-Yices2n	0	429	33491.05	33477.559	429	429	0	18	378	75	0
OpenSMT	0	423	48248.249	48228.196	423	423	0	24	378	87	0
cvc5	0	420	58777.351	58888.077	420	420	0	27	378	80	0
z3-4.8.17n	0	416	60462.571	60452.537	416	416	0	31	378	99	0
smtinterpol	0	401	100331.098	94881.004	401	401	0	46	378	164	0
MathSATn	0	398	81556.747	81551.959	398	398	0	49	378	153	0
veriT	0	394	87212.053	87176.343	394	394	0	53	378	120	0
solsmt	0	131	390182.871	392231.265	131	131	0	316	378	325	224

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	325	36306.727	36271.232	325	0	325	12	488	80	0
Yices2	0	321	36959.366	36908.792	321	0	321	16	488	75	0
2021-Yices2n	0	321	36913.89	36962.173	321	0	321	16	488	75	0
OpenSMT	0	315	39958.415	39872.418	315	0	315	22	488	87	0
veriT	0	311	52967.088	52955.132	311	0	311	26	488	120	0
z3-4.8.17n	0	310	53133.04	53114.373	310	0	310	27	488	99	0
MathSATn	0	274	98420.566	98418.729	274	0	274	63	488	153	0
smtinterpol	0	260	141127.59	133088.228	260	0	260	77	488	164	0
solsmt	0	106	272303.913	274486.745	106	0	106	231	488	325	224

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	621	6622.755	6524.964	621	372	249	204	0	204	0
2021-Yices2n	0	620	6586.721	6560.627	620	371	249	205	0	205	0
OpenSMT	0	591	7837.474	7801.839	591	346	245	234	0	234	0
z3-4.8.17n	0	520	9040.998	9005.41	520	299	221	305	0	305	0
veriT	0	512	9106.362	9053.122	512	291	221	313	0	313	0
MathSATn	0	496	9228.349	9212.943	496	303	193	329	0	329	0
cvc5	0	495	9965.581	9952.369	495	293	202	330	0	330	0
smtinterpol	0	408	15067.218	12135.221	408	263	145	417	0	417	0
solsmt	0	105	17559.103	17573.423	105	46	59	720	0	488	224

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.