SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

LIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Z3-alpha	Z3-alpha	Z3-alpha	cvc5	Z3-alpha

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Z3-alpha	0	232 (base -2)	633.23	233.32	234	111	123	66	0	66	0
cvc5	0	223	62.53	89.98	223	100	123	77	0	77	0
Amaya	0	190	5109.81	5134.13	190	88	102	110	0	12	93
YicesQS	0	181	56.23	78.61	181	98	83	119	0	119	0
UltimateEliminator+MathSAT	0	176	6824.91	5749.27	176	59	117	124	0	42	0
iProver v3.9.3	0	89	4177.28	1138.83	90	0	90	210	0	201	0
SMTInterpol	0	34	30.17	22.12	34	3	31	266	0	60	0
Z3-alpha-base ⁿ	0	234	598.98	627.85	234	111	123	66	0	66	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
Z3-alpha	0	234 (base +0)	5473.23	1444.28	234	111	123	66	0	66	0
cvc5	0	223	62.53	89.98	223	100	123	77	0	77	0
Amaya	0	190	5109.81	5134.13	190	88	102	110	0	12	93
YicesQS	0	181	56.23	78.61	181	98	83	119	0	119	0
UltimateEliminator+MathSAT	0	176	6824.91	5749.27	176	59	117	124	0	42	0
iProver v3.9.3	0	90	5468.75	1466.60	90	0	90	210	0	201	0
SMTInterpol	0	34	30.17	22.12	34	3	31	266	0	60	0
Z3-alpha-base ⁿ	0	234	598.98	627.85	234	111	123	66	0	66	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
Z3-alpha	0	111 (base +0)	5433.46	1394.49	111	111	0	66	123	66	0
cvc5	0	100	38.88	51.14	100	100	0	77	123	77	0
YicesQS	0	98	42.60	54.73	98	98	0	79	123	79	0
Amaya	0	88	3276.58	3287.90	88	88	0	89	123	8	79
UltimateEliminator+MathSAT	0	59	5497.56	4880.93	59	59	0	118	123	38	0
SMTInterpol	0	3	1.26	1.31	3	3	0	174	123	50	0
iProver v3.9.3	0	0	0.00	0.00	0	0	0	177	123	174	0
Z3-alpha-base ⁿ	0	111	576.71	590.47	111	111	0	66	123	66	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
cvc5	0	123	23.65	38.85	123	0	123	0	177	0	0
Z3-alpha	0	123 (base +0)	39.76	49.79	123	0	123	0	177	0	0
UltimateEliminator+MathSAT	0	117	1327.36	868.34	117	0	117	6	177	4	0
Amaya	0	102	1833.24	1846.23	102	0	102	21	177	4	14
iProver v3.9.3	0	90	5468.75	1466.60	90	0	90	33	177	27	0
YicesQS	0	83	13.63	23.88	83	0	83	40	177	40	0
SMTInterpol	0	31	28.91	20.81	31	0	31	92	177	10	0
Z3-alpha-base ⁿ	0	123	22.27	37.39	123	0	123	0	177	0	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
Z3-alpha	0	230 (base +1)	139.93	109.32	230	107	123	0	70	0	0
cvc5	0	223	62.53	89.98	223	100	123	0	77	0	0
YicesQS	0	180	29.81	52.06	180	97	83	0	120	0	0
Amaya	0	170	361.76	382.99	170	72	98	0	130	0	0
UltimateEliminator+MathSAT	0	163	1423.37	610.02	163	48	115	82	55	0	0
iProver v3.9.3	0	82	849.95	280.68	82	0	82	4	214	0	0
SMTInterpol	0	34	30.17	22.12	34	3	31	174	92	0	0
Z3-alpha-base ⁿ	0	229	46.48	74.64	229	106	123	0	71	0	0

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