QF_RDL (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices 2.6.2	Yices 2.6.2	Yices 2.6.2	Yices 2.6.2	Yices 2.6.2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	214	83405.108	83410.595	214	105	109	33		33	0
2018-Yicesn	0	214	83634.304	83638.751	214	105	109	33		33	0
CVC4	0	211	95504.663	95417.951	211	103	108	36		36	0
veriT	0	210	102696.7	102704.268	210	104	106	37		37	0
Z3n	0	209	99844.008	99850.138	209	102	107	38		38	0
SMTInterpol	0	194	153890.186	152250.169	194	101	93	53		53	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	214	83409.238	83409.455	214	105	109	33		33	0
2018-Yicesn	0	214	83637.364	83637.771	214	105	109	33		33	0
CVC4	0	211	95511.093	95416.691	211	103	108	36		36	0
veriT	0	210	102701.87	102703.108	210	104	106	37		37	0
Z3n	0	209	99848.198	99848.648	209	102	107	38		38	0
SMTInterpol	0	194	153890.186	152250.169	194	101	93	53		53	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices 2.6.2	0	105	741.918	741.942	105	105	0	142	33	0
2018-Yicesn	0	105	775.591	775.666	105	105	0	142	33	0
veriT	0	104	9130.002	9130.602	104	104	0	143	37	0
CVC4	0	103	9458.873	9441.467	103	103	0	144	36	0
Z3n	0	102	13437.537	13437.757	102	102	0	145	38	0
SMTInterpol	0	101	22736.958	21890.126	101	101	0	146	53	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices 2.6.2	0	109	3467.32	3467.513	109	0	109	138	33	0
2018-Yicesn	0	109	3661.773	3662.105	109	0	109	138	33	0
CVC4	0	108	6852.22	6775.224	108	0	108	139	36	0
Z3n	0	107	7210.661	7210.891	107	0	107	140	38	0
veriT	0	106	14371.868	14372.506	106	0	106	141	37	0
SMTInterpol	0	93	51953.228	51160.042	93	0	93	154	53	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	195	1602.044	1602.09	195	100	95	52		52	0
2018-Yicesn	0	194	1623.238	1623.3	194	100	94	53		53	0
Z3n	0	179	2106.94	2106.991	179	91	88	68		68	0
CVC4	0	168	2529.624	2511.837	168	86	82	79		79	0
veriT	0	167	2312.207	2312.181	167	81	86	80		80	0
SMTInterpol	0	135	4030.699	3338.326	135	74	61	112		112	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.