SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Equality_LinearArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_ALIA : 176 benchmarks
QF_AUFLIA : 534 benchmarks
QF_UFDTLIA : 76 benchmarks
QF_UFDTLIRA : 9 benchmarks
QF_UFIDL : 300 benchmarks
QF_UFLIA : 300 benchmarks
QF_UFLRA : 541 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1798	29410.55	21874.66	1798	1064	734	138	0	117	0
cvc5	0	1795	40758.29	40986.45	1795	1031	764	141	0	141	0
OpenSMT	0	1778	30357.19	30581.04	1778	1002	776	73	85	73	0
Yices2	0	1744	19780.59	19999.59	1744	982	762	107	85	107	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1798	29410.55	21874.66	1798	1064	734	138	0	117	0
cvc5	0	1795	40758.29	40986.45	1795	1031	764	141	0	141	0
OpenSMT	0	1778	30357.19	30581.04	1778	1002	776	73	85	73	0
Yices2	0	1744	19780.59	19999.59	1744	982	762	107	85	107	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1064	17863.19	13942.77	1064	1064	0	19	853	16	0
cvc5	0	1031	20983.36	21113.94	1031	1031	0	52	853	52	0
OpenSMT	0	1002	11021.72	11146.88	1002	1002	0	31	903	31	0
Yices2	0	982	10579.41	10702.92	982	982	0	51	903	51	0

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	776	19335.47	19434.16	776	0	776	25	1135	25	0
cvc5	0	764	19774.93	19872.52	764	0	764	54	1118	54	0
Yices2	0	762	9201.17	9296.68	762	0	762	39	1135	39	0
SMTInterpol	0	734	11547.37	7931.89	734	0	734	84	1118	70	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	1709	7246.87	3178.66	1709	1007	702	4	223	0	0
Yices2	0	1693	592.95	802.92	1693	956	737	0	243	0	0
cvc5	0	1645	1437.68	1640.89	1645	952	693	0	291	0	0
OpenSMT	0	1645	1806.62	2009.77	1645	937	708	0	291	0	0