SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Datatypes (Single Query Track)

Competition results for the QF_Datatypes division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

QF_DT : 352 benchmarks
QF_UFDT : 200 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	cvc5	cvc5	SMTInterpol

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	332	80124.05	80175.55	332	137	195	220	0	220	0
SMTInterpol	0	194	31652.88	21838.44	195	46	149	357	0	327	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	332	80124.05	80175.55	332	137	195	220	0	220	0
SMTInterpol	0	195	32866.26	23018.30	195	46	149	357	0	327	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	137	16437.24	16456.65	137	137	0	25	390	25	0
SMTInterpol	0	46	10297.99	9696.23	46	46	0	116	390	116	0

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	195	63686.82	63718.90	195	0	195	92	265	92	0
SMTInterpol	0	149	22568.28	13322.07	149	0	149	138	265	112	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	117	1031.62	502.14	117	16	101	0	435	0	0
cvc5	0	102	485.80	498.39	102	35	67	0	450	0	0