QF_RDL (Single Query Track)

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

Page generated on 2021-07-18 17:29:07 +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
2019-Yices 2.6.2n	0	213	43046.864	43118.994	213	105	108	34	34	0
Yices2	0	213	43312.727	43315.66	213	105	108	34	34	0
veriT	0	210	51525.208	51526.307	210	104	106	37	37	0
cvc5	0	210	52166.457	52124.298	210	103	107	37	37	0
z3n	0	206	54112.389	54315.905	206	99	107	41	41	0
MathSAT5n	0	202	64018.317	64166.195	202	103	99	45	45	0
OpenSMT	0	188	84754.447	84702.863	188	97	91	59	59	0
SMTInterpol	0	187	87373.294	85309.402	187	99	88	60	60	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Yices 2.6.2n	0	213	43120.354	43118.114	213	105	108	34	34	0
Yices2	0	213	43314.657	43314.95	213	105	108	34	34	0
veriT	0	210	51528.878	51525.037	210	104	106	37	37	0
cvc5	0	210	52171.597	52122.798	210	103	107	37	37	0
z3n	0	206	54311.779	54314.045	206	99	107	41	41	0
MathSAT5n	0	202	64162.777	64164.395	202	103	99	45	45	0
OpenSMT	0	188	84757.877	84701.333	188	97	91	59	59	0
SMTInterpol	0	187	87373.294	85309.402	187	99	88	60	60	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2019-Yices 2.6.2n	0	105	767.8	766.953	105	105	0	0	142	34	0
Yices2	0	105	793.33	793.434	105	105	0	0	142	34	0
veriT	0	104	4426.711	4422.509	104	104	0	1	142	37	0
cvc5	0	103	6366.137	6328.27	103	103	0	2	142	37	0
MathSAT5n	0	103	6753.942	6754.413	103	103	0	2	142	45	0
z3n	0	99	10808.274	10807.577	99	99	0	6	142	41	0
SMTInterpol	0	99	14011.684	13099.557	99	99	0	6	142	60	0
OpenSMT	0	97	16129.505	16096.271	97	97	0	8	142	59	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2019-Yices 2.6.2n	0	108	2752.554	2751.162	108	0	108	1	138	34	0
Yices2	0	108	2921.327	2921.516	108	0	108	1	138	34	0
z3n	0	107	3903.505	3906.469	107	0	107	2	138	41	0
cvc5	0	107	6205.46	6194.529	107	0	107	2	138	37	0
veriT	0	106	7502.167	7502.528	106	0	106	3	138	37	0
MathSAT5n	0	99	17808.835	17809.982	99	0	99	10	138	45	0
OpenSMT	0	91	29028.372	29005.062	91	0	91	18	138	59	0
SMTInterpol	0	88	33761.609	32609.845	88	0	88	21	138	60	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Yices 2.6.2n	0	195	1624.893	1622.445	195	100	95	52	52	0
Yices2	0	194	1643.916	1644.071	194	100	94	53	53	0
z3n	0	181	2144.795	2146.55	181	89	92	66	66	0
veriT	0	170	2251.589	2246.819	170	83	87	77	77	0
cvc5	0	166	2570.676	2559.076	166	84	82	81	81	0
MathSAT5n	0	163	2486.948	2487.032	163	86	77	84	84	0
OpenSMT	0	137	3049.673	3018.463	137	74	63	110	110	0
SMTInterpol	0	127	4262.338	3511.891	127	69	58	120	120	0

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