SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

LRA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
YicesQS	0	1002	295.71	418.07	1002	408	594	11	0	11	0
Z3-alpha	0	909 (base -40)	27366.04	7144.37	948	395	553	65	0	59	6
UltimateEliminator+MathSAT	0	864	12006.23	8235.00	864	345	519	149	0	149	0
cvc5	0	847	23380.45	23488.45	847	346	501	166	0	166	0
SMTInterpol	0	159	2506.71	1834.22	159	2	157	854	0	37	0
iProver v3.9.3	0	157	24515.90	6428.01	217	0	217	796	0	796	0
Z3-alpha-base ⁿ	0	949	40598.12	40719.62	949	397	552	64	0	64	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
YicesQS	0	1002	295.71	418.07	1002	408	594	11	0	11	0
Z3-alpha	0	948 (base -1)	136229.10	34387.24	948	395	553	65	0	59	6
UltimateEliminator+MathSAT	0	864	12006.23	8235.00	864	345	519	149	0	149	0
cvc5	0	847	23380.45	23488.45	847	346	501	166	0	166	0
iProver v3.9.3	0	217	199987.31	50738.47	217	0	217	796	0	796	0
SMTInterpol	0	159	2506.71	1834.22	159	2	157	854	0	37	0
Z3-alpha-base ⁿ	0	949	40598.12	40719.62	949	397	552	64	0	64	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
YicesQS	0	408	123.38	173.23	408	408	0	4	601	4	0
Z3-alpha	0	395 (base -2)	19463.43	4997.79	395	395	0	17	601	15	2
cvc5	0	346	6051.92	6095.53	346	346	0	66	601	66	0
UltimateEliminator+MathSAT	0	345	4650.25	3082.08	345	345	0	67	601	67	0
SMTInterpol	0	2	0.86	0.90	2	2	0	410	601	23	0
iProver v3.9.3	0	0	0.00	0.00	0	0	0	412	601	412	0
Z3-alpha-base ⁿ	0	397	5946.24	5995.70	397	397	0	15	601	15	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
YicesQS	0	594	172.34	244.84	594	0	594	7	412	7	0
Z3-alpha	0	553 (base +1)	116765.67	29389.45	553	0	553	48	412	44	4
UltimateEliminator+MathSAT	0	519	7355.97	5152.92	519	0	519	82	412	82	0
cvc5	0	501	17328.53	17392.92	501	0	501	100	412	100	0
iProver v3.9.3	0	217	199987.31	50738.47	217	0	217	384	412	384	0
SMTInterpol	0	157	2505.85	1833.33	157	0	157	444	412	14	0
Z3-alpha-base ⁿ	0	552	34651.88	34723.93	552	0	552	49	412	49	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
YicesQS	0	1002	295.71	418.07	1002	408	594	0	11	0	0
Z3-alpha	0	855 (base +12)	4613.57	1434.84	855	380	475	0	158	0	0
UltimateEliminator+MathSAT	0	822	5721.96	2469.27	822	332	490	0	191	0	0
cvc5	0	718	301.65	390.64	718	291	427	0	295	0	0
SMTInterpol	0	156	1005.85	413.47	156	2	154	793	64	0	0
iProver v3.9.3	0	97	1997.31	599.82	97	0	97	0	916	0	0
Z3-alpha-base ⁿ	0	843	1504.32	1608.47	843	376	467	0	170	0	0

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