SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_LRA (Single Query Track)

Competition results for the QF_LRA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
OpenSMT	OpenSMT	OpenSMT	OpenSMT	OpenSMT

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	578	19618.61	19693.28	578	326	252	17	0	17	0
Yices2	0	561	25527.85	25600.28	561	320	241	34	0	34	0
cvc5	0	549	26942.01	27013.30	549	309	240	46	0	46	0
Z3-alpha	0	514 (base -33)	64169.74	16445.90	549	312	237	46	0	46	0
SMTInterpol	0	476	51585.82	44844.68	479	295	184	116	0	111	0
Z3-alpha-base ⁿ	0	547	31112.89	31185.34	547	315	232	48	0	48	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	578	19618.61	19693.28	578	326	252	17	0	17	0
Yices2	0	561	25527.85	25600.28	561	320	241	34	0	34	0
cvc5	0	549	26942.01	27013.30	549	309	240	46	0	46	0
Z3-alpha	0	549 (base +2)	157972.00	39949.93	549	312	237	46	0	46	0
SMTInterpol	0	479	55577.07	48040.64	479	295	184	116	0	111	0
Z3-alpha-base ⁿ	0	547	31112.89	31185.34	547	315	232	48	0	48	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	326	14009.48	14052.30	326	326	0	9	260	9	0
Yices2	0	320	11051.56	11092.59	320	320	0	15	260	15	0
Z3-alpha	0	312 (base -3)	80314.24	20415.71	312	312	0	23	260	23	0
cvc5	0	309	13979.69	14019.58	309	309	0	26	260	26	0
SMTInterpol	0	295	30818.38	27232.72	295	295	0	40	260	40	0
Z3-alpha-base ⁿ	0	315	12960.71	13001.68	315	315	0	20	260	20	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	252	5609.12	5640.98	252	0	252	3	340	3	0
Yices2	0	241	14476.28	14507.69	241	0	241	14	340	14	0
cvc5	0	240	12962.32	12993.72	240	0	240	15	340	15	0
Z3-alpha	0	237 (base +5)	77657.77	19534.22	237	0	237	18	340	18	0
SMTInterpol	0	184	24758.69	20807.92	184	0	184	71	340	66	0
Z3-alpha-base ⁿ	0	232	18152.18	18183.67	232	0	232	23	340	23	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	488	1533.60	1594.23	488	271	217	0	107	0	0
Yices2	0	464	1086.75	1144.13	464	277	187	0	131	0	0
cvc5	0	407	1596.52	1646.72	407	232	175	0	188	0	0
Z3-alpha	0	353 (base -33)	4148.52	1186.60	353	205	148	0	242	0	0
SMTInterpol	0	313	2924.42	1333.15	313	196	117	0	282	0	0
Z3-alpha-base ⁿ	0	386	1227.25	1275.30	386	233	153	0	209	0	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver