QF_RDL (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

Benchmarks: 247
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
2021-Yices2n	0	213	41878.171	43623.15	213	105	108	34	34	0
Yices2	0	213	43317.737	43289.871	213	105	108	34	34	0
cvc5	0	209	52266.313	52240.032	209	103	106	38	38	0
veriT	0	208	53737.981	53731.978	208	102	106	39	39	0
z3-4.8.17n	0	206	54738.847	54727.548	206	98	108	41	41	0
MathSATn	0	199	64495.44	64502.617	199	101	98	48	48	0
OpenSMT	0	192	80568.953	80516.88	192	99	93	55	55	0
smtinterpol	0	179	95158.908	91973.228	179	98	81	68	68	0
solsmt	0	77	189686.241	193981.307	77	41	36	170	120	18

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	213	43320.117	43288.991	213	105	108	34	34	0
2021-Yices2n	0	213	43536.639	43621.41	213	105	108	34	34	0
cvc5	0	209	52272.063	52238.572	209	103	106	38	38	0
veriT	0	208	53741.171	53730.588	208	102	106	39	39	0
z3-4.8.17n	0	206	54746.287	54725.988	206	98	108	41	41	0
MathSATn	0	199	64500.71	64500.577	199	101	98	48	48	0
OpenSMT	0	192	80571.883	80515.17	192	99	93	55	55	0
smtinterpol	0	180	95473.258	91850.408	180	98	82	67	67	0
solsmt	0	77	189710.621	193975.837	77	41	36	170	120	18

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	105	669.324	667.338	105	105	0	0	142	34	0
2021-Yices2n	0	105	725.282	750.754	105	105	0	0	142	34	0
cvc5	0	103	6127.437	6127.914	103	103	0	2	142	38	0
veriT	0	102	6805.503	6794.472	102	102	0	3	142	39	0
MathSATn	0	101	6776.132	6776.492	101	101	0	4	142	48	0
OpenSMT	0	99	14985.506	14986.249	99	99	0	6	142	55	0
z3-4.8.17n	0	98	11320.656	11320.887	98	98	0	7	142	41	0
smtinterpol	0	98	14629.602	13662.096	98	98	0	7	142	67	0
solsmt	0	41	73942.828	76024.926	41	41	0	64	142	120	18

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	108	3050.793	3021.653	108	0	108	1	138	34	0
2021-Yices2n	0	108	3211.357	3270.657	108	0	108	1	138	34	0
z3-4.8.17n	0	108	3825.631	3805.102	108	0	108	1	138	41	0
cvc5	0	106	6544.626	6510.658	106	0	106	3	138	38	0
veriT	0	106	7335.668	7336.116	106	0	106	3	138	39	0
MathSATn	0	98	18124.578	18124.085	98	0	98	11	138	48	0
OpenSMT	0	93	25986.377	25928.92	93	0	93	16	138	55	0
smtinterpol	0	82	41243.656	38588.312	82	0	82	27	138	67	0
solsmt	0	36	76167.793	78350.911	36	0	36	73	138	120	18

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	193	1700.406	1669.113	193	99	94	54	54	0
2021-Yices2n	0	192	1703.017	1704.035	192	98	94	55	55	0
z3-4.8.17n	0	178	2196.543	2175.512	178	87	91	69	69	0
veriT	0	169	2247.022	2235.427	169	82	87	78	78	0
MathSATn	0	166	2428.119	2426.12	166	88	78	81	81	0
cvc5	0	164	2724.396	2723.48	164	85	79	83	83	0
OpenSMT	0	147	2891.932	2882.724	147	81	66	100	100	0
smtinterpol	0	130	4506.638	3583.233	130	72	58	117	117	0
solsmt	0	22	5532.835	5548.622	22	4	18	225	206	18

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