SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_IDL (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Yices2	Z3-alpha	Z3-alpha	cvc5	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	977	30949.40	31074.60	977	642	335	231	0	231	0
Z3-alpha	0	969 (base -67)	72399.51	19081.93	1039	668	371	169	0	164	5
cvc5	0	921	66905.67	67029.12	921	544	377	287	0	282	5
OpenSMT	0	892	45637.59	45754.08	892	571	321	316	0	316	0
SMTInterpol	0	594	40514.47	31639.81	594	331	263	614	0	353	0
Z3-alpha-base ⁿ	0	1036	50978.99	51115.07	1036	654	382	172	0	172	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
Z3-alpha	0	1039 (base +3)	252103.06	64197.56	1039	668	371	169	0	164	5
Yices2	0	977	30949.40	31074.60	977	642	335	231	0	231	0
cvc5	0	921	66905.67	67029.12	921	544	377	287	0	282	5
OpenSMT	0	892	45637.59	45754.08	892	571	321	316	0	316	0
SMTInterpol	0	594	40514.47	31639.81	594	331	263	614	0	353	0
Z3-alpha-base ⁿ	0	1036	50978.99	51115.07	1036	654	382	172	0	172	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
Z3-alpha	0	668 (base +14)	144769.18	36954.77	668	668	0	59	481	54	5
Yices2	0	642	21714.34	21796.82	642	642	0	85	481	85	0
OpenSMT	0	571	36735.79	36811.38	571	571	0	156	481	156	0
cvc5	0	544	42463.89	42537.22	544	544	0	183	481	178	5
SMTInterpol	0	331	24845.47	21151.41	331	331	0	396	481	242	0
Z3-alpha-base ⁿ	0	654	26643.64	26728.86	654	654	0	73	481	73	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
cvc5	0	377	24441.78	24491.91	377	0	377	49	782	49	0
Z3-alpha	0	371 (base -11)	107333.88	27242.79	371	0	371	55	782	55	0
Yices2	0	335	9235.07	9277.79	335	0	335	91	782	91	0
OpenSMT	0	321	8901.79	8942.70	321	0	321	105	782	105	0
SMTInterpol	0	263	15669.00	10488.40	263	0	263	163	782	95	0
Z3-alpha-base ⁿ	0	382	24335.35	24386.20	382	0	382	44	782	44	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	864	1274.14	1381.42	864	564	300	0	344	0	0
Z3-alpha	0	806 (base -14)	7535.96	2264.46	806	531	275	0	402	0	0
OpenSMT	0	644	2068.53	2148.57	644	371	273	0	564	0	0
cvc5	0	634	2227.57	2305.68	634	343	291	0	574	0	0
SMTInterpol	0	423	4705.07	2186.80	423	227	196	173	612	0	0
Z3-alpha-base ⁿ	0	820	2024.01	2125.71	820	528	292	0	388	0	0

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