SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_NonLinearIntArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_NIA : 7516 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 SAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	6673	43422.54	44254.28	6673	6673	843	0	838	0
cvc5	0	6221	1570875.68	1571841.93	6221	6221	1295	0	1142	148
SMTInterpol	0	1	225.75	197.92	1	1	7515	0	2	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	6673	43422.54	44254.28	6673	6673	843	0	838	0
cvc5	0	6221	1570875.68	1571841.93	6221	6221	1295	0	1142	148
SMTInterpol	0	1	225.75	197.92	1	1	7515	0	2	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	6673	43422.54	44254.28	6673	6673	843	0	838	0
cvc5	0	6221	1570875.68	1571841.93	6221	6221	1295	0	1142	148
SMTInterpol	0	1	225.75	197.92	1	1	7515	0	2	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	6385	14022.22	14813.49	6385	6385	5	1126	0	0
cvc5	0	2940	7900.50	8259.25	2940	2940	5	4571	0	0
SMTInterpol	0	0	0.00	0.00	0	0	7471	45	0	0