SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_NonLinearRealArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_NRA : 2777 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
SMT-RAT	SMT-RAT	SMT-RAT	-	SMT-RAT

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
SMT-RAT	0	2090	22988.57	23250.71	2090	2090	687	0	161	0
cvc5	0	2017	10890.68	11139.67	2017	2017	760	0	188	0
SMTInterpol	0	13	1893.89	1712.80	13	13	2764	0	0	0
Yices2	435	2105	7970.61	8234.82	2105	2105	672	0	103	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
SMT-RAT	0	2090	22988.57	23250.71	2090	2090	687	0	161	0
cvc5	0	2017	10890.68	11139.67	2017	2017	760	0	188	0
SMTInterpol	0	13	1893.89	1712.80	13	13	2764	0	0	0
Yices2	435	2105	7970.61	8234.82	2105	2105	672	0	103	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
SMT-RAT	0	2090	22988.57	23250.71	2090	2090	687	0	161	0
cvc5	0	2017	10890.68	11139.67	2017	2017	760	0	188	0
SMTInterpol	0	13	1893.89	1712.80	13	13	2764	0	0	0
Yices2	435	2105	7970.61	8234.82	2105	2105	672	0	103	0

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
SMT-RAT	0	2024	628.55	879.06	2024	2024	520	233	0	0
cvc5	0	2000	525.22	770.78	2000	2000	550	227	0	0
SMTInterpol	0	7	38.25	17.37	7	7	2759	11	0	0
Yices2	431	2075	646.72	905.88	2075	2075	561	141	0	0