SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Equality_NonLinearArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_ANIA : 121 benchmarks
QF_AUFNIA : 5 benchmarks
QF_UFDTNIA : 18 benchmarks
QF_UFNIA : 300 benchmarks
QF_UFNRA : 31 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	352	22055.20	22101.14	352	352	123	0	79	0
SMTInterpol	0	281	20495.15	18339.72	281	281	194	0	2	0
Yices2	109	168	1835.55	1856.88	168	168	163	144	0	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	352	22055.20	22101.14	352	352	123	0	79	0
SMTInterpol	0	281	20495.15	18339.72	281	281	194	0	2	0
Yices2	109	168	1835.55	1856.88	168	168	163	144	0	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	352	22055.20	22101.14	352	352	123	0	79	0
SMTInterpol	0	281	20495.15	18339.72	281	281	194	0	2	0
Yices2	109	168	1835.55	1856.88	168	168	163	144	0	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	271	308.40	341.35	271	271	41	163	0	0
SMTInterpol	0	209	675.92	331.22	209	209	181	85	0	0
Yices2	102	154	258.81	278.14	154	154	155	166	0	0