Arith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Z3-alpha2	Z3-alpha2	Z3-alpha2	Z3-GEX	Z3-GEX

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	1111 (base +27)	29502.05	29149.70	1111	431	680	144	0	144
Z3-alpha2-debug ⁿ	1111	32274.49	30850.42	1111	431	680	144	0	144
z3-BooledASS ^ne	1088 (base +0)	30236.01	30371.84	1088	417	671	167	0	166
Z3-GEX	1067 (base -19)	15235.97	4141.71	1104	421	683	151	0	151
YicesQS	1015	4713.27	4837.48	1015	427	588	240	0	213
cvc5-cvc5-xyz ^ne	1001 (base +0)	35596.35	35723.15	1001	373	628	254	0	254
cvc5	999	34410.56	34537.60	999	373	626	256	0	256
UltimateEliminator+MathSAT	810	15813.65	12387.73	810	299	511	445	0	204
Amaya	408	4183.51	4243.27	408	170	238	146	701	92
SMTInterpol	226	3416.27	2883.90	226	20	206	1029	0	70
SMT-RAT	96	20.07	32.02	96	4	92	3	1156	3
z3-BooledASS-base ⁿ	1088	30106.92	30242.99	1088	417	671	167	0	166
Z3-GEX-base ⁿ	1086	31862.17	31999.76	1086	413	673	169	0	165
Z3-alpha2-base ⁿ	1084	30423.03	30559.05	1084	412	672	171	0	168
cvc5-cvc5-xyz-base ⁿ	1001	35606.93	35734.14	1001	373	628	254	0	254

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	1111 (base +27)	29502.05	29149.70	1111	431	680	144	0	144
Z3-alpha2-debug ⁿ	1111	32274.49	30850.42	1111	431	680	144	0	144
Z3-GEX	1104 (base +18)	104821.35	26801.69	1104	421	683	151	0	151
z3-BooledASS ^ne	1088 (base +0)	30236.01	30371.84	1088	417	671	167	0	166
YicesQS	1015	4713.27	4837.48	1015	427	588	240	0	213
cvc5-cvc5-xyz ^ne	1001 (base +0)	35596.35	35723.15	1001	373	628	254	0	254
cvc5	999	34410.56	34537.60	999	373	626	256	0	256
UltimateEliminator+MathSAT	810	15813.65	12387.73	810	299	511	445	0	204
Amaya	408	4183.51	4243.27	408	170	238	146	701	92
SMTInterpol	226	3416.27	2883.90	226	20	206	1029	0	70
SMT-RAT	96	20.07	32.02	96	4	92	3	1156	3
z3-BooledASS-base ⁿ	1088	30106.92	30242.99	1088	417	671	167	0	166
Z3-GEX-base ⁿ	1086	31862.17	31999.76	1086	413	673	169	0	165
Z3-alpha2-base ⁿ	1084	30423.03	30559.05	1084	412	672	171	0	168
cvc5-cvc5-xyz-base ⁿ	1001	35606.93	35734.14	1001	373	628	254	0	254

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-alpha2	431 (base +19)	12739.77	12618.08	431	431	103	721	103
Z3-alpha2-debug ⁿ	431	13911.02	13374.35	431	431	103	721	103
YicesQS	427	3715.46	3767.77	427	427	107	721	80
Z3-GEX ^ne	421 (base +8)	25212.30	6689.46	421	421	113	721	113
z3-BooledASS ^ne	417 (base +0)	7476.42	7527.98	417	417	117	721	117
cvc5-cvc5-xyz ^ne	373 (base +0)	5087.95	5134.59	373	373	161	721	161
cvc5	373	5629.09	5676.11	373	373	161	721	161
UltimateEliminator+MathSAT	299	7184.19	5697.14	299	299	235	721	88
Amaya	170	3817.83	3843.12	170	170	113	972	73
SMTInterpol	20	26.14	15.62	20	20	514	721	60
SMT-RAT	4	4.28	4.77	4	4	1	1250	1
z3-BooledASS-base ⁿ	417	7409.38	7461.36	417	417	117	721	117
Z3-GEX-base ⁿ	413	6824.55	6876.54	413	413	121	721	120
Z3-alpha2-base ⁿ	412	6463.43	6514.88	412	412	122	721	122
cvc5-cvc5-xyz-base ⁿ	373	5085.65	5132.41	373	373	161	721	161

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-GEX	683 (base +10)	79609.04	20112.23	683	683	36	536	36
Z3-alpha2	680 (base +8)	16762.28	16531.61	680	680	39	536	39
Z3-alpha2-debug ⁿ	680	18363.47	17476.07	680	680	39	536	39
z3-BooledASS ^ne	671 (base +0)	22759.58	22843.85	671	671	48	536	47
cvc5-cvc5-xyz ^ne	628 (base +0)	30508.40	30588.56	628	628	91	536	91
cvc5	626	28781.47	28861.49	626	626	93	536	93
YicesQS	588	997.81	1069.71	588	588	131	536	131
UltimateEliminator+MathSAT	511	8629.46	6690.59	511	511	208	536	116
Amaya	238	365.68	400.15	238	238	32	985	19
SMTInterpol	206	3390.13	2868.28	206	206	513	536	10
SMT-RAT	92	15.79	27.25	92	92	1	1162	1
Z3-GEX-base ⁿ	673	25037.63	25123.21	673	673	46	536	43
Z3-alpha2-base ⁿ	672	23959.60	24044.17	672	672	47	536	44
z3-BooledASS-base ⁿ	671	22697.54	22781.62	671	671	48	536	47
cvc5-cvc5-xyz-base ⁿ	628	30521.28	30601.73	628	628	91	536	91

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-GEX	1028 (base +27)	3145.40	1084.99	1028	399	629	0	227
Z3-alpha2 ^ne	1025 (base +22)	3973.48	3648.92	1025	399	626	0	230
Z3-alpha2-debug ⁿ	1025	6492.40	5179.05	1025	399	626	0	230
z3-BooledASS ^ne	1008 (base -1)	1132.79	1256.97	1008	396	612	1	246
YicesQS	994	296.37	418.12	994	414	580	0	261
cvc5-cvc5-xyz ^ne	853 (base +0)	357.71	463.51	853	337	516	0	402
cvc5	852	333.67	439.60	852	336	516	0	403
UltimateEliminator+MathSAT	773	5185.11	2271.81	773	283	490	237	245
Amaya	388	869.70	926.12	388	150	238	36	831
SMTInterpol	222	677.45	305.87	222	20	202	920	113
SMT-RAT	96	20.07	32.02	96	4	92	0	1159
z3-BooledASS-base ⁿ	1009	1154.00	1278.24	1009	397	612	1	245
Z3-alpha2-base ⁿ	1003	1098.23	1222.40	1003	391	612	3	249
Z3-GEX-base ⁿ	1001	1095.79	1220.66	1001	390	611	1	253
cvc5-cvc5-xyz-base ⁿ	853	355.27	461.14	853	337	516	0	402

SMT-COMP 2026