SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_NonLinearIntArith (Unsat Core Track)

Competition results for the QF_NonLinearIntArith division in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Logics:

QF_NIA : 2475 benchmarks
QF_NIRA : 2 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	29446	25902.02	26168.97	2160	2160	317	0	317	0
cvc5	0	26614	86637.44	86895.43	1978	1978	499	0	499	0
SMTInterpol	0	430	451.78	285.45	27	27	2450	0	2	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	29446	25902.02	26168.97	2160	2160	317	0	317	0
cvc5	0	26614	86637.44	86895.43	1978	1978	499	0	499	0
SMTInterpol	0	430	451.78	285.45	27	27	2450	0	2	0

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	29446	25902.02	26168.97	2160	2160	317	0	317	0
cvc5	0	26614	86637.44	86895.43	1978	1978	499	0	499	0
SMTInterpol	0	430	451.78	285.45	27	27	2450	0	2	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	28124	3313.41	3562.45	2041	2041	0	436	0	0
cvc5	0	22164	4316.47	4517.66	1630	1630	0	847	0	0
SMTInterpol	0	423	47.37	27.75	23	23	2442	12	0	0