SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

Arith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

LIA : 300 benchmarks
LRA : 1013 benchmarks
NIA : 254 benchmarks
NRA : 99 benchmarks

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	1474 (base -23)	30071.79	8145.93	1515	588	927	151	0	139	10
YicesQS	0	1382	1184.28	1353.56	1382	575	807	284	0	284	0
cvc5	0	1382	49381.69	49558.83	1382	527	855	284	0	284	0
UltimateEliminator+MathSAT	0	1192	19554.35	14310.52	1192	447	745	474	0	268	0
iProver v3.9.3	0	355	34918.57	9232.99	431	0	431	1235	0	1226	0
SMTInterpol	0	253	2592.36	1894.39	253	20	233	1413	0	98	0
SMT-RAT	0	96	26.55	38.57	96	4	92	3	1567	3	0
Amaya	2	396	5695.49	5745.77	398	139	259	156	1112	18	93
Z3-alpha-base ⁿ	0	1497	42872.96	43062.49	1497	583	914	169	0	162	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	1515 (base +18)	143774.86	36599.76	1515	588	927	151	0	139	10
YicesQS	0	1382	1184.28	1353.56	1382	575	807	284	0	284	0
cvc5	0	1382	49381.69	49558.83	1382	527	855	284	0	284	0
UltimateEliminator+MathSAT	0	1192	19554.35	14310.52	1192	447	745	474	0	268	0
iProver v3.9.3	0	431	262315.08	66595.76	431	0	431	1235	0	1226	0
SMTInterpol	0	253	2592.36	1894.39	253	20	233	1413	0	98	0
SMT-RAT	0	96	26.55	38.57	96	4	92	3	1567	3	0
Amaya	2	396	5695.49	5745.77	398	139	259	156	1112	18	93
Z3-alpha-base ⁿ	0	1497	42872.96	43062.49	1497	583	914	169	0	162	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	588 (base +5)	25036.63	6506.31	588	588	0	88	990	83	5
YicesQS	0	575	198.82	269.27	575	575	0	101	990	101	0
cvc5	0	527	6406.07	6471.97	527	527	0	149	990	149	0
UltimateEliminator+MathSAT	0	447	10352.61	8055.00	447	447	0	229	990	117	0
SMTInterpol	0	20	26.72	15.79	20	20	0	656	990	73	0
SMT-RAT	0	4	10.07	10.57	4	4	0	1	1661	1	0
iProver v3.9.3	0	0	0.00	0.00	0	0	0	676	990	673	0
Amaya	2	139	3579.02	3596.95	141	139	2	118	1407	10	79
Z3-alpha-base ⁿ	0	583	7630.51	7703.20	583	583	0	93	990	89	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	927 (base +13)	118738.23	30093.45	927	0	927	57	682	50	5
cvc5	0	855	42975.63	43086.86	855	0	855	129	682	129	0
YicesQS	0	807	985.46	1084.29	807	0	807	177	682	177	0
UltimateEliminator+MathSAT	0	745	9201.74	6255.53	745	0	745	239	682	149	0
iProver v3.9.3	0	431	262315.08	66595.76	431	0	431	553	682	547	0
Amaya	0	257	2116.47	2148.82	257	0	257	33	1376	8	14
SMTInterpol	0	233	2565.64	1878.60	233	0	233	751	682	25	0
SMT-RAT	0	92	16.48	28.00	92	0	92	1	1573	1	0
Z3-alpha-base ⁿ	0	914	35242.45	35359.28	914	0	914	70	682	68	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	1415 (base +35)	5324.14	1893.63	1415	568	847	0	251	0	0
YicesQS	0	1378	420.94	589.63	1378	574	804	0	288	0	0
cvc5	0	1168	482.28	626.83	1168	471	697	0	498	0	0
UltimateEliminator+MathSAT	0	1137	7868.55	3405.53	1137	423	714	205	324	0	0
iProver v3.9.3	0	277	4224.07	1310.64	277	0	277	4	1385	0	0
SMTInterpol	0	250	1091.49	473.64	250	20	230	1255	161	0	0
SMT-RAT	0	96	26.55	38.57	96	4	92	0	1570	0	0
Amaya	2	375	814.30	861.36	377	122	255	36	1253	0	0
Z3-alpha-base ⁿ	0	1380	1871.20	2041.61	1380	555	825	2	284	0	0

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