Equality_MachineArith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

ABV : 892 benchmarks
ABVFP : 60 benchmarks
ABVFPLRA : 77 benchmarks
AUFBV : 552 benchmarks
AUFBVDTLIA : 556 benchmarks
AUFBVDTNIA : 300 benchmarks
AUFBVDTNIRA : 904 benchmarks
AUFBVFP : 57 benchmarks
AUFBVFPDTNIRA : 117 benchmarks
AUFFPDTNIRA : 159 benchmarks
UFBV : 144 benchmarks
UFBVDT : 1 benchmarks
UFBVDTLIA : 24 benchmarks
UFBVDTNIA : 157 benchmarks
UFBVDTNIRA : 525 benchmarks
UFBVFP : 2 benchmarks
UFBVFPDTNIRA : 89 benchmarks
UFBVLIA : 208 benchmarks
UFFPDTNIRA : 355 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	Bitwuzla	cvc5	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	3162 (base +16)	147396.43	147800.20	3162	632	2530	2017	0	1631
cvc5	3158	135722.64	136124.66	3158	629	2529	2021	0	1435
SMTInterpol	1449	31351.25	24731.31	1449	18	1431	2814	916	1712
Bitwuzla-fixed ⁿ	1214	27095.27	27250.43	1214	799	415	570	3395	565
Bitwuzla	1213	26497.87	26654.29	1213	799	414	571	3395	566
z3-BooledASS ^ne	819 (base -1946)	20867.68	20970.20	819	279	540	4360	0	2012
bitwuzla-dandelion ⁿ	591 (base -93)	20380.52	20457.45	591	254	337	1193	3395	252
UltimateEliminator+MathSAT	154	863.08	449.01	154	117	37	1838	3187	389
cvc5-cvc5-xyz-base ⁿ	3146	130086.54	130487.15	3146	628	2518	2033	0	1436
z3-BooledASS-base ⁿ	2765	37434.38	37778.07	2765	532	2233	2414	0	1638
bitwuzla-dandelion-base ⁿ	684	24129.59	24219.01	684	313	371	1100	3395	274

(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
cvc5-cvc5-xyz ^ne	3162 (base +16)	147396.43	147800.20	3162	632	2530	2017	0	1631
cvc5	3158	135722.64	136124.66	3158	629	2529	2021	0	1435
SMTInterpol	1449	31351.25	24731.31	1449	18	1431	2814	916	1712
Bitwuzla-fixed ⁿ	1214	27095.27	27250.43	1214	799	415	570	3395	565
Bitwuzla	1213	26497.87	26654.29	1213	799	414	571	3395	566
z3-BooledASS ^ne	819 (base -1946)	20867.68	20970.20	819	279	540	4360	0	2012
bitwuzla-dandelion ⁿ	591 (base -93)	20380.52	20457.45	591	254	337	1193	3395	252
UltimateEliminator+MathSAT	154	863.08	449.01	154	117	37	1838	3187	389
cvc5-cvc5-xyz-base ⁿ	3146	130086.54	130487.15	3146	628	2518	2033	0	1436
z3-BooledASS-base ⁿ	2765	37434.38	37778.07	2765	532	2233	2414	0	1638
bitwuzla-dandelion-base ⁿ	684	24129.59	24219.01	684	313	371	1100	3395	274

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	799	7393.06	7494.10	799	799	124	4256	124
Bitwuzla-fixed ⁿ	799	7865.39	7965.41	799	799	124	4256	124
cvc5-cvc5-xyz ^ne	632 (base +4)	61176.40	61259.86	632	632	480	4067	221
cvc5	629	59484.24	59567.05	629	629	483	4067	227
z3-BooledASS ^ne	279 (base -253)	4688.60	4723.19	279	279	833	4067	179
bitwuzla-dandelion ⁿ	254 (base -59)	3426.86	3459.06	254	254	669	4256	39
UltimateEliminator+MathSAT	117	622.02	333.25	117	117	826	4236	122
SMTInterpol	18	18.40	12.51	18	18	937	4224	242
cvc5-cvc5-xyz-base ⁿ	628	60042.19	60124.92	628	628	484	4067	227
z3-BooledASS-base ⁿ	532	7923.74	7989.85	532	532	580	4067	200
bitwuzla-dandelion-base ⁿ	313	3567.25	3606.94	313	313	610	4256	42

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	2530 (base +12)	86220.03	86540.34	2530	2530	559	2090	524
cvc5	2529	76238.40	76557.61	2529	2529	560	2090	531
SMTInterpol	1431	31332.85	24718.80	1431	1431	1055	2693	833
z3-BooledASS ^ne	540 (base -1693)	16179.08	16247.01	540	540	2549	2090	1038
Bitwuzla-fixed ⁿ	415	19229.88	19285.03	415	415	191	4573	191
Bitwuzla	414	19104.81	19160.20	414	414	192	4573	192
bitwuzla-dandelion ⁿ	337 (base -34)	16953.66	16998.40	337	337	269	4573	33
UltimateEliminator+MathSAT	37	241.06	115.76	37	37	578	4564	108
cvc5-cvc5-xyz-base ⁿ	2518	70044.35	70362.23	2518	2518	571	2090	532
z3-BooledASS-base ⁿ	2233	29510.64	29788.21	2233	2233	856	2090	583
bitwuzla-dandelion-base ⁿ	371	20562.34	20612.07	371	371	235	4573	34

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	2561	1798.68	2114.98	2561	297	2264	220	2398	0
cvc5-cvc5-xyz	2542 (base -12)	1830.09	2144.06	2542	299	2243	87	2550	73
SMTInterpol	1338	5464.25	2277.56	1338	18	1320	815	3026	0
Bitwuzla-fixed ⁿ	1095	1688.98	1824.12	1095	765	330	5	4079	0
Bitwuzla	1095	1695.17	1831.43	1095	765	330	5	4079	0
z3-BooledASS ^ne	733 (base -1883)	815.28	905.08	733	258	475	2258	2188	0
bitwuzla-dandelion ⁿ	506 (base -89)	1108.79	1172.14	506	243	263	940	3733	0
UltimateEliminator+MathSAT	152	788.01	390.70	152	116	36	1339	3688	0
z3-BooledASS-base ⁿ	2616	1706.36	2027.97	2616	501	2115	685	1878	0
cvc5-cvc5-xyz-base ⁿ	2554	1763.06	2078.83	2554	297	2257	225	2400	0
bitwuzla-dandelion-base ⁿ	595	1251.05	1325.42	595	302	293	826	3758	0

SMT-COMP 2026