SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_LinearRealArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_LRA : 497 benchmarks
QF_RDL : 109 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	591	11946.41	12020.45	591	591	15	0	15	0
OpenSMT	0	590	20671.54	20747.41	590	590	16	0	16	0
SMTInterpol	0	548	31291.92	27288.02	548	548	58	0	58	0
cvc5	0	471	3437.17	3494.40	471	471	135	0	135	0

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	591	11946.41	12020.45	591	591	15	0	15	0
OpenSMT	0	590	20671.54	20747.41	590	590	16	0	16	0
SMTInterpol	0	548	31291.92	27288.02	548	548	58	0	58	0
cvc5	0	471	3437.17	3494.40	471	471	135	0	135	0

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	591	11946.41	12020.45	591	591	15	0	15	0
OpenSMT	0	590	20671.54	20747.41	590	590	16	0	16	0
SMTInterpol	0	548	31291.92	27288.02	548	548	58	0	58	0
cvc5	0	471	3437.17	3494.40	471	471	135	0	135	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	534	675.90	741.46	534	534	0	72	0	0
OpenSMT	0	518	1121.96	1185.93	518	518	0	88	0	0
cvc5	0	448	752.69	806.81	448	448	0	158	0	0
SMTInterpol	0	435	2781.07	1298.27	435	435	0	171	0	0