SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Equality (Model Validation Track)

Competition results for the QF_Equality division in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Logics:

QF_UF : 1571 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
OpenSMT	OpenSMT	OpenSMT	-	OpenSMT

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	1571	383.74	577.16	1571	1571	0	0	0	0
cvc5	0	1571	498.38	688.26	1571	1571	0	0	0	0
SMTInterpol	0	1571	3564.11	1596.37	1571	1571	0	0	0	0
Yices2	0	1570	278.69	472.78	1570	1570	1	0	0	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	1571	383.74	577.16	1571	1571	0	0	0	0
cvc5	0	1571	498.38	688.26	1571	1571	0	0	0	0
SMTInterpol	0	1571	3564.11	1596.37	1571	1571	0	0	0	0
Yices2	0	1570	278.69	472.78	1570	1570	1	0	0	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	1571	383.74	577.16	1571	1571	0	0	0	0
cvc5	0	1571	498.38	688.26	1571	1571	0	0	0	0
SMTInterpol	0	1571	3564.11	1596.37	1571	1571	0	0	0	0
Yices2	0	1570	278.69	472.78	1570	1570	1	0	0	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	1571	383.74	577.16	1571	1571	0	0	0	0
cvc5	0	1571	498.38	688.26	1571	1571	0	0	0	0
SMTInterpol	0	1571	3564.11	1596.37	1571	1571	0	0	0	0
Yices2	0	1570	278.69	472.78	1570	1570	1	0	0	0