SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_LinearRealArith (Single Query Track)

Competition results for the QF_LinearRealArith division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

QF_LRA : 595 benchmarks
QF_RDL : 247 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	776	29318.57	29417.94	776	426	350	66	0	66	0
OpenSMT	0	775	33493.57	33594.38	775	429	346	67	0	67	0
cvc5	0	758	30920.43	31017.99	758	410	348	84	0	84	0
Z3-alpha	0	717 (base -40)	74569.31	19122.77	756	411	345	86	0	86	0
SMTInterpol	0	653	60173.16	51180.97	656	394	262	186	0	176	0
Z3-alpha-base ⁿ	0	757	38522.79	38622.60	757	417	340	85	0	85	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
Yices2	0	776	29318.57	29417.94	776	426	350	66	0	66	0
OpenSMT	0	775	33493.57	33594.38	775	429	346	67	0	67	0
cvc5	0	758	30920.43	31017.99	758	410	348	84	0	84	0
Z3-alpha	0	756 (base -1)	180518.24	45665.82	756	411	345	86	0	86	0
SMTInterpol	0	656	64164.41	54376.94	656	394	262	186	0	176	0
Z3-alpha-base ⁿ	0	757	38522.79	38622.60	757	417	340	85	0	85	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	429	22536.72	22593.32	429	429	0	12	401	12	0
Yices2	0	426	12397.66	12451.93	426	426	0	15	401	15	0
Z3-alpha	0	411 (base -6)	92370.66	23468.30	411	411	0	30	401	30	0
cvc5	0	410	15074.71	15127.09	410	410	0	31	401	31	0
SMTInterpol	0	394	35258.50	30823.23	394	394	0	47	401	47	0
Z3-alpha-base ⁿ	0	417	18842.20	18896.70	417	417	0	24	401	24	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
Yices2	0	350	16920.90	16966.01	350	0	350	14	478	14	0
cvc5	0	348	15845.73	15890.89	348	0	348	16	478	16	0
OpenSMT	0	346	10956.86	11001.06	346	0	346	18	478	18	0
Z3-alpha	0	345 (base +5)	88147.59	22197.52	345	0	345	19	478	19	0
SMTInterpol	0	262	28905.91	23553.71	262	0	262	102	478	93	0
Z3-alpha-base ⁿ	0	340	19680.59	19725.90	340	0	340	24	478	24	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
Yices2	0	661	1418.20	1499.88	661	376	285	0	181	0	0
OpenSMT	0	638	1918.95	1998.14	638	352	286	0	204	0	0
cvc5	0	585	2198.13	2270.28	585	325	260	0	257	0	0
Z3-alpha	0	532 (base -39)	5968.15	1706.25	532	294	238	0	310	0	0
SMTInterpol	0	449	4476.13	2063.29	449	272	177	0	393	0	0
Z3-alpha-base ⁿ	0	571	1651.30	1722.58	571	323	248	0	271	0	0

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