SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

NIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 254
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	Z3-alpha	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	238 (base +17)	2042.11	730.14	238	79	159	16	0	13	1
cvc5	0	225	25317.53	25348.31	225	78	147	29	0	29	0
UltimateEliminator+MathSAT	0	138	664.54	298.42	138	42	96	116	0	30	0
YicesQS	0	107	583.24	596.44	107	65	42	147	0	147	0
iProver v3.9.3	0	35	1450.49	402.10	47	0	47	207	0	207	0
SMTInterpol	0	20	29.01	16.51	20	14	6	234	0	1	0
Amaya	2	206	585.67	611.64	208	51	157	46	0	6	0
Z3-alpha-base ⁿ	0	221	1653.49	1681.16	221	72	149	33	0	26	1

(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	238 (base +17)	2042.11	730.14	238	79	159	16	0	13	1
cvc5	0	225	25317.53	25348.31	225	78	147	29	0	29	0
UltimateEliminator+MathSAT	0	138	664.54	298.42	138	42	96	116	0	30	0
YicesQS	0	107	583.24	596.44	107	65	42	147	0	147	0
iProver v3.9.3	0	47	43167.83	10889.39	47	0	47	207	0	207	0
SMTInterpol	0	20	29.01	16.51	20	14	6	234	0	1	0
Amaya	2	206	585.67	611.64	208	51	157	46	0	6	0
Z3-alpha-base ⁿ	0	221	1653.49	1681.16	221	72	149	33	0	26	1

(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	79 (base +7)	138.89	112.87	79	79	0	3	172	2	1
cvc5	0	78	314.35	324.02	78	78	0	4	172	4	0
YicesQS	0	65	31.81	39.79	65	65	0	17	172	17	0
UltimateEliminator+MathSAT	0	42	200.97	90.11	42	42	0	40	172	12	0
SMTInterpol	0	14	24.05	13.09	14	14	0	68	172	0	0
iProver v3.9.3	0	0	0.00	0.00	0	0	0	82	172	82	0
Amaya	2	51	302.44	309.04	53	51	2	29	172	2	0
Z3-alpha-base ⁿ	0	72	1107.06	1116.17	72	72	0	10	172	6	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
Z3-alpha	0	159 (base +10)	1903.21	617.26	159	0	159	8	87	6	0
Amaya	0	155	283.23	302.60	155	0	155	12	87	4	0
cvc5	0	147	25003.18	25024.30	147	0	147	20	87	20	0
UltimateEliminator+MathSAT	0	96	463.57	208.31	96	0	96	71	87	16	0
iProver v3.9.3	0	47	43167.83	10889.39	47	0	47	120	87	120	0
YicesQS	0	42	551.42	556.66	42	0	42	125	87	125	0
SMTInterpol	0	6	4.96	3.42	6	0	6	161	87	1	0
Z3-alpha-base ⁿ	0	149	546.43	564.99	149	0	149	18	87	16	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	235 (base +20)	540.21	311.38	235	78	157	0	19	0	0
cvc5	0	142	101.52	119.06	142	77	65	0	112	0	0
UltimateEliminator+MathSAT	0	138	664.54	298.42	138	42	96	85	31	0	0
YicesQS	0	105	78.20	91.11	105	65	40	0	149	0	0
iProver v3.9.3	0	29	541.58	164.92	29	0	29	0	225	0	0
SMTInterpol	0	20	29.01	16.51	20	14	6	229	5	0	0
Amaya	2	205	452.54	478.37	207	50	157	36	11	0	0
Z3-alpha-base ⁿ	0	215	298.03	324.66	215	70	145	2	37	0	0

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