SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Equality_LinearArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_UFIDL : 206 benchmarks
QF_UFLIA : 300 benchmarks
QF_UFLRA : 385 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	875	10359.08	10469.75	875	875	16	0	16	0
SMTInterpol	0	863	14112.21	10956.23	863	863	28	0	28	0
cvc5	0	857	26524.00	26633.68	857	857	34	0	34	0
Yices2	0	823	15704.73	15809.28	823	823	68	0	68	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	875	10359.08	10469.75	875	875	16	0	16	0
SMTInterpol	0	863	14112.21	10956.23	863	863	28	0	28	0
cvc5	0	857	26524.00	26633.68	857	857	34	0	34	0
Yices2	0	823	15704.73	15809.28	823	823	68	0	68	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	875	10359.08	10469.75	875	875	16	0	16	0
SMTInterpol	0	863	14112.21	10956.23	863	863	28	0	28	0
cvc5	0	857	26524.00	26633.68	857	857	34	0	34	0
Yices2	0	823	15704.73	15809.28	823	823	68	0	68	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	835	3380.24	1472.30	835	835	0	56	0	0
OpenSMT	0	824	1228.24	1331.02	824	824	0	67	0	0
Yices2	0	785	261.28	358.75	785	785	0	106	0	0
cvc5	0	778	454.33	550.04	778	778	0	113	0	0