QF_UFLRA (Single Query Track)

Competition results for the QF_UFLRA logic in the Single Query Track.

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	539	2488.817	2491.54	539	326	213	2	2	0
2019-SMTInterpoln	0	539	5163.662	3823.686	539	326	213	2	2	0
SMTInterpol	0	539	7844.063	4982.973	539	326	213	2	2	0
veriT	0	538	3745.645	3746.327	538	325	213	3	3	0
MathSAT5n	0	538	3773.64	3774.429	538	325	213	3	3	0
cvc5 - fixedn	0	538	4723.753	4724.741	538	325	213	3	3	0
cvc5	0	538	4738.141	4739.324	538	325	213	3	3	0
z3n	0	529	19578.101	19578.846	529	318	211	12	12	0
mc2	0	522	1326.472	1326.805	522	314	208	19	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	539	2488.997	2491.48	539	326	213	2	2	0
2019-SMTInterpoln	0	539	5163.662	3823.686	539	326	213	2	2	0
SMTInterpol	0	539	7844.063	4982.973	539	326	213	2	2	0
veriT	0	538	3746.095	3746.187	538	325	213	3	3	0
MathSAT5n	0	538	3774.15	3774.389	538	325	213	3	3	0
cvc5 - fixedn	0	538	4724.643	4724.571	538	325	213	3	3	0
cvc5	0	538	4739.051	4739.164	538	325	213	3	3	0
z3n	0	529	19579.751	19578.276	529	318	211	12	12	0
mc2	0	522	1326.472	1326.805	522	314	208	19	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Yices2	0	326	1274.956	1276.41	326	326	0	1	214	2	0
2019-SMTInterpoln	0	326	2947.918	2101.65	326	326	0	1	214	2	0
SMTInterpol	0	326	4684.38	2818.041	326	326	0	1	214	2	0
veriT	0	325	2498.476	2498.553	325	325	0	2	214	3	0
MathSAT5n	0	325	2526.239	2526.463	325	325	0	2	214	3	0
cvc5 - fixedn	0	325	3266.404	3266.404	325	325	0	2	214	3	0
cvc5	0	325	3278.14	3278.255	325	325	0	2	214	3	0
z3n	0	318	13097.958	13095.991	318	318	0	9	214	12	0
mc2	0	314	832.002	832.218	314	314	0	13	214	0	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Yices2	0	213	14.041	15.07	213	0	213	0	328	2	0
veriT	0	213	47.619	47.634	213	0	213	0	328	3	0
MathSAT5n	0	213	47.911	47.926	213	0	213	0	328	3	0
cvc5 - fixedn	0	213	258.239	258.167	213	0	213	0	328	3	0
cvc5	0	213	260.911	260.909	213	0	213	0	328	3	0
2019-SMTInterpoln	0	213	1015.744	522.036	213	0	213	0	328	2	0
SMTInterpol	0	213	1959.683	964.932	213	0	213	0	328	2	0
z3n	0	211	5281.793	5282.285	211	0	211	2	328	12	0
mc2	0	208	408.103	408.216	208	0	208	5	328	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	538	129.858	132.338	538	325	213	3	3	0
veriT	0	538	218.095	218.187	538	325	213	3	3	0
MathSAT5n	0	536	241.312	241.545	536	323	213	5	5	0
cvc5 - fixedn	0	531	415.92	415.73	531	320	211	10	10	0
cvc5	0	531	417.289	417.045	531	320	211	10	10	0
2019-SMTInterpoln	0	531	1960.273	892.372	531	321	210	10	10	0
SMTInterpol	0	529	2391.436	1043.883	529	319	210	12	12	0
mc2	0	521	502.539	502.759	521	314	207	20	13	0
z3n	0	513	895.095	892.912	513	308	205	28	28	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.