SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_RDL (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 247
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	215	3790.72	3817.66	215	106	109	32	0	32	0
cvc5	0	209	3978.42	4004.69	209	101	108	38	0	38	0
Z3-alpha	0	203 (base -7)	10399.57	2676.86	207	99	108	40	0	40	0
OpenSMT	0	197	13874.97	13901.10	197	103	94	50	0	50	0
SMTInterpol	0	177	8587.34	6336.30	177	99	78	70	0	65	0
Z3-alpha-base ⁿ	0	210	7409.90	7437.26	210	102	108	37	0	37	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	215	3790.72	3817.66	215	106	109	32	0	32	0
cvc5	0	209	3978.42	4004.69	209	101	108	38	0	38	0
Z3-alpha	0	207 (base -3)	22546.24	5715.89	207	99	108	40	0	40	0
OpenSMT	0	197	13874.97	13901.10	197	103	94	50	0	50	0
SMTInterpol	0	177	8587.34	6336.30	177	99	78	70	0	65	0
Z3-alpha-base ⁿ	0	210	7409.90	7437.26	210	102	108	37	0	37	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	106	1346.10	1359.35	106	106	0	0	141	0	0
OpenSMT	0	103	8527.23	8541.02	103	103	0	3	141	3	0
cvc5	0	101	1095.01	1107.51	101	101	0	5	141	5	0
Z3-alpha	0	99 (base -3)	12056.42	3052.59	99	99	0	7	141	7	0
SMTInterpol	0	99	4440.12	3590.50	99	99	0	7	141	7	0
Z3-alpha-base ⁿ	0	102	5881.49	5895.03	102	102	0	4	141	4	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	109	2444.62	2458.32	109	0	109	0	138	0	0
Z3-alpha	0	108 (base +0)	10489.82	2663.30	108	0	108	1	138	1	0
cvc5	0	108	2883.41	2897.18	108	0	108	1	138	1	0
OpenSMT	0	94	5347.74	5360.08	94	0	94	15	138	15	0
SMTInterpol	0	78	4147.22	2745.79	78	0	78	31	138	27	0
Z3-alpha-base ⁿ	0	108	1528.41	1542.24	108	0	108	1	138	1	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	197	331.45	355.76	197	99	98	0	50	0	0
Z3-alpha	0	179 (base -6)	1819.63	519.65	179	89	90	0	68	0	0
cvc5	0	178	601.60	623.56	178	93	85	0	69	0	0
OpenSMT	0	150	385.35	403.90	150	81	69	0	97	0	0
SMTInterpol	0	136	1551.70	730.13	136	76	60	0	111	0	0
Z3-alpha-base ⁿ	0	185	424.05	447.28	185	90	95	0	62	0	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver