QF_LinearRealArith (Single Query Track)

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

Page generated on 2021-07-18 17:29:06 +0000

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

Logics:

• QF_LRA : 582 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
Yices2	0	753	124300.762	124277.033	753	426	327	76	0	76	0
cvc5	0	751	138777.821	140113.786	751	419	332	78	0	78	0
OpenSMT	0	734	151930.267	151783.591	734	412	322	95	0	95	0
z3n	0	733	160613.313	160795.586	733	408	325	96	0	96	0
veriT	0	723	174316.165	174310.083	723	403	320	106	0	106	0
SMTInterpol	0	681	271570.147	261651.158	681	403	278	148	0	148	0
MathSAT5n	0	673	230948.127	231099.068	673	392	281	156	0	156	0
2020-OpenSMTn	0	543	69798.963	69785.788	543	314	229	39	247	39	0
2019-Par4n	0	536	105313.498	67940.747	536	319	217	46	247	46	0
2019-Yices 2.6.2n	0	213	43046.864	43118.994	213	105	108	34	582	34	0
mc2	0	201	49389.939	49245.453	201	123	78	381	247	7	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	753	124307.302	124275.293	753	426	327	76	0	76	0
cvc5	0	751	140063.078	140109.826	751	419	332	78	0	78	0
OpenSMT	0	734	151937.707	151780.841	734	412	322	95	0	95	0
z3n	0	733	160821.683	160791.656	733	408	325	96	0	96	0
veriT	0	723	174326.675	174306.203	723	403	320	106	0	106	0
SMTInterpol	0	684	271764.007	261548.008	684	404	280	145	0	145	0
MathSAT5n	0	673	231110.727	231092.498	673	392	281	156	0	156	0
2019-Par4n	0	565	136198.308	49817.594	565	337	228	17	247	17	0
2020-OpenSMTn	0	543	69805.673	69784.158	543	314	229	39	247	39	0
2019-Yices 2.6.2n	0	213	43120.354	43118.114	213	105	108	34	582	34	0
mc2	0	201	49390.409	49245.183	201	123	78	381	247	7	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	426	36786.771	36751.907	426	426	0	22	381	76	0
cvc5	0	419	60731.125	60777.217	419	419	0	29	381	78	0
OpenSMT	0	412	65000.724	64956.508	412	412	0	36	381	95	0
z3n	0	408	69826.909	69818.719	408	408	0	40	381	96	0
SMTInterpol	0	404	103654.442	97788.263	404	404	0	44	381	145	0
veriT	0	403	80766.863	80765.879	403	403	0	45	381	106	0
MathSAT5n	0	392	89802.293	89780.813	392	392	0	56	381	156	0
2019-Par4n	0	337	76444.162	24807.434	337	337	0	6	486	17	0
2020-OpenSMTn	0	314	50396.725	50399.487	314	314	0	29	486	39	0
mc2	0	123	21834.746	21746.454	123	123	0	220	486	7	0
2019-Yices 2.6.2n	0	105	767.8	766.953	105	105	0	0	724	34	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	332	36131.952	36132.609	332	0	332	13	484	78	0
Yices2	0	327	44320.531	44323.386	327	0	327	18	484	76	0
z3n	0	325	47794.774	47772.937	325	0	325	20	484	96	0
OpenSMT	0	322	43736.984	43624.333	322	0	322	23	484	95	0
veriT	0	320	50359.812	50340.324	320	0	320	25	484	106	0
MathSAT5n	0	281	98108.434	98111.685	281	0	281	64	484	156	0
SMTInterpol	0	280	124909.565	120559.746	280	0	280	65	484	145	0
2020-OpenSMTn	0	229	15808.948	15784.67	229	0	229	7	593	39	0
2019-Par4n	0	228	56154.147	21410.161	228	0	228	8	593	17	0
2019-Yices 2.6.2n	0	108	2752.554	2751.162	108	0	108	1	720	34	0
mc2	0	78	27382.043	27325.08	78	0	78	158	593	7	0

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	618	6604.771	6569.349	618	376	242	211	0	211	0
OpenSMT	0	552	8764.965	8697.809	552	312	240	277	0	277	0
veriT	0	522	8963.189	8936.927	522	292	230	307	0	307	0
z3n	0	520	9023.295	9013.311	520	299	221	309	0	309	0
cvc5	0	503	9637.439	9593.279	503	295	208	326	0	326	0
MathSAT5n	0	497	9265.352	9265.846	497	293	204	332	0	332	0
SMTInterpol	0	411	14610.036	12026.875	411	256	155	418	0	418	0
2020-OpenSMTn	0	403	5989.61	5964.999	403	227	176	179	247	179	0
2019-Par4n	0	402	10611.922	5947.62	402	246	156	180	247	180	0
2019-Yices 2.6.2n	0	195	1624.893	1622.445	195	100	95	52	582	52	0
mc2	0	175	8963.543	8962.922	175	102	73	407	247	273	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.