QF_LinearRealArith (QF_LRA, QF_RDL) - Single Query Track

Competition results for the QF_LinearRealArith (QF_LRA, QF_RDL) division in the Single Query Track.

Page generated on 2020-01-29 22:04:58 +0000

Benchmarks: 676
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices2	Yices2	Yices2	CVC4	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	602	109897.428	109839.849	602	314	288	74	74	0
Yices2-fixedn	0	602	109970.868	109963.235	602	314	288	74	74	0
CVC4	0	600	135856.211	136099.522	600	306	294	76	76	0
z3n	0	592	132193.288	132092.119	592	304	288	84	84	0
veriT	0	583	146451.334	146457.22	583	299	284	93	93	0
MathSAT5n	0	551	188525.403	188508.247	551	298	253	125	125	0
SMTInterpol-fixedn	0	545	229427.96	219846.533	545	299	246	131	131	0
SMTInterpol	0	544	228975.948	219468.762	544	298	246	132	132	0
OpenSMT	0	406	44407.135	44350.538	406	214	192	23	23	0
2019-SPASS-SATTn	0	405	49274.908	49247.21	405	215	190	24	24	0
2019-Par4n	0	404	113602.072	73597.554	404	217	187	25	25	0
2019-Yices 2.6.2n	0	213	42885.764	42889.107	213	105	108	34	34	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	602	109897.428	109839.849	602	314	288	74	74	0
Yices2-fixedn	0	602	109970.868	109963.235	602	314	288	74	74	0
CVC4	0	600	135856.211	136099.522	600	306	294	76	76	0
z3n	0	592	132193.288	132092.119	592	304	288	84	84	0
veriT	0	583	146451.334	146457.22	583	299	284	93	93	0
MathSAT5n	0	551	188525.403	188508.247	551	298	253	125	125	0
SMTInterpol-fixedn	0	545	229427.96	219846.533	545	299	246	131	131	0
SMTInterpol	0	544	228975.948	219468.762	544	298	246	132	132	0
2019-Par4n	0	412	161928.422	40991.768	412	218	194	17	17	0
OpenSMT	0	406	44407.135	44350.538	406	214	192	23	23	0
2019-SPASS-SATTn	0	405	49274.908	49247.21	405	215	190	24	24	0
2019-Yices 2.6.2n	0	213	42885.764	42889.107	213	105	108	34	34	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2-fixedn	0	314	24558.916	24555.841	314	314	0	362	74	0
Yices2	0	314	24626.213	24576.022	314	314	0	362	74	0
CVC4	0	306	51311.725	51484.233	306	306	0	370	76	0
z3n	0	304	40549.0	40468.81	304	304	0	372	84	0
veriT	0	299	53151.441	53145.615	299	299	0	377	93	0
SMTInterpol-fixedn	0	299	66747.543	62490.305	299	299	0	377	131	0
MathSAT5n	0	298	56781.073	56790.637	298	298	0	378	125	0
SMTInterpol	0	298	66367.313	62115.206	298	298	0	378	132	0
2019-Par4n	0	218	52379.12	13273.24	218	218	0	211	17	0
2019-SPASS-SATTn	0	215	17727.018	17717.644	215	215	0	214	24	0
OpenSMT	0	214	20593.338	20589.007	214	214	0	215	23	0
2019-Yices 2.6.2n	0	105	466.779	466.885	105	105	0	142	34	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
CVC4	0	294	40149.235	40213.3	294	0	294	382	76	0
Yices2	0	288	40872.035	40862.146	288	0	288	388	74	0
Yices2-fixedn	0	288	41013.772	41006.004	288	0	288	388	74	0
z3n	0	288	47249.339	47221.869	288	0	288	388	84	0
veriT	0	284	48903.743	48910.014	284	0	284	392	93	0
MathSAT5n	0	253	87350.23	87316.31	253	0	253	423	125	0
SMTInterpol	0	246	117480.855	112951.706	246	0	246	430	132	0
SMTInterpol-fixedn	0	246	117567.477	112953.748	246	0	246	430	131	0
2019-Par4n	0	194	90559.862	22918.128	194	0	194	235	17	0
OpenSMT	0	192	19014.047	18961.421	192	0	192	237	23	0
2019-SPASS-SATTn	0	190	26748.21	26729.366	190	0	190	239	24	0
2019-Yices 2.6.2n	0	108	2820.425	2820.682	108	0	108	139	34	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2-fixedn	0	503	5382.739	5366.472	503	279	224	173	173	0
Yices2	0	502	5380.827	5365.486	502	278	224	174	174	0
z3n	0	439	7115.461	7056.958	439	234	205	237	237	0
veriT	0	425	7239.769	7227.454	425	215	210	251	251	0
CVC4	0	423	7632.01	7618.948	423	227	196	253	253	0
MathSAT5n	0	410	7456.611	7452.889	410	230	180	266	266	0
SMTInterpol	0	344	11402.047	9450.053	344	202	142	332	332	0
SMTInterpol-fixedn	0	344	11383.266	9450.804	344	201	143	332	332	0
2019-SPASS-SATTn	0	306	4150.167	4116.67	306	171	135	123	123	0
OpenSMT	0	305	4144.049	4112.369	305	155	150	124	124	0
2019-Par4n	0	294	7490.423	4341.293	294	162	132	135	135	0
2019-Yices 2.6.2n	0	193	1631.563	1631.729	193	98	95	54	54	0

n Non-competing.