QF_UFLRA (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +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	smtinterpol	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2021-SMTInterpoln	0	537	10152.075	7740.32	537	317	220	4	4	0
Yices2	0	536	6341.562	6343.575	536	316	220	5	5	0
smtinterpol	0	536	10911.859	8770.383	536	317	219	5	5	0
MathSATn	0	535	7334.254	7335.425	535	315	220	6	6	0
veriT	0	535	7358.851	7358.676	535	315	220	6	6	0
OpenSMT	0	534	9879.854	9882.476	534	314	220	7	7	0
cvc5	0	534	10242.038	10244.348	534	314	220	7	7	0
z3-4.8.17n	0	532	11701.239	11702.457	532	313	219	9	9	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2021-SMTInterpoln	0	538	10358.645	7738.86	538	318	220	3	3	0
Yices2	0	536	6342.282	6343.345	536	316	220	5	5	0
smtinterpol	0	536	10911.859	8770.383	536	317	219	5	5	0
MathSATn	0	535	7335.124	7335.235	535	315	220	6	6	0
veriT	0	535	7359.691	7358.546	535	315	220	6	6	0
OpenSMT	0	534	9881.754	9882.066	534	314	220	7	7	0
cvc5	0	534	10243.878	10244.078	534	314	220	7	7	0
z3-4.8.17n	0	532	11703.709	11701.957	532	313	219	9	9	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2021-SMTInterpoln	0	318	6311.081	4570.422	318	318	0	1	222	3	0
smtinterpol	0	317	6107.683	4736.969	317	317	0	2	222	5	0
Yices2	0	316	3932.076	3932.669	316	316	0	3	222	5	0
MathSATn	0	315	4903.693	4903.778	315	315	0	4	222	6	0
veriT	0	315	4931.905	4930.79	315	315	0	4	222	6	0
OpenSMT	0	314	7436.575	7436.853	314	314	0	5	222	7	0
cvc5	0	314	7659.989	7660.199	314	314	0	5	222	7	0
z3-4.8.17n	0	313	7911.512	7910.117	313	313	0	6	222	9	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	220	10.206	10.676	220	0	220	0	321	5	0
veriT	0	220	27.786	27.756	220	0	220	0	321	6	0
MathSATn	0	220	31.431	31.457	220	0	220	0	321	6	0
OpenSMT	0	220	45.178	45.213	220	0	220	0	321	7	0
cvc5	0	220	183.889	183.879	220	0	220	0	321	7	0
2021-SMTInterpoln	0	220	1647.564	768.438	220	0	220	0	321	3	0
z3-4.8.17n	0	219	1392.196	1391.84	219	0	219	1	321	9	0
smtinterpol	0	219	2404.176	1633.414	219	0	219	1	321	5	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	535	187.4	188.439	535	315	220	6	6	0
MathSATn	0	534	272.736	272.845	534	314	220	7	7	0
veriT	0	533	269.195	268.038	533	313	220	8	8	0
2021-SMTInterpoln	0	529	2269.516	996.133	529	311	218	12	12	0
smtinterpol	0	529	2521.324	1082.897	529	311	218	12	12	0
cvc5	0	528	502.846	502.779	528	309	219	13	13	0
z3-4.8.17n	0	525	549.056	547.197	525	308	217	16	16	0
OpenSMT	0	523	704.222	704.343	523	304	219	18	18	0

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