Rebuttal TACAS 2025

Tables

MQ1[R1,R2,R3] Selection of Benchmarks and time limits

Table 1. Number of selected benchmarks by logic.

	# Benchmarks	# Non-supported	# Final
QF_FP	40 407	23 454	16 953
QF_LIA	13 306	24	13 282
QF_BV	46 191	41 985	4 206
QF_S	18 940	6 320	12 620
QF_SLIA	84 395	51 857	31 538
Total	203 239	123 640	78 599

Table 2. Timeout percentage by logic using a 30 seconds timeout and a 10GB memory limit.

	QF_FP	QF_BV	QF_LIA	QF_S	QF_SLIA	Total
Z3	0.000	0.000	28.151	0.829	3.218	6.181
cvc5	0.000	0.000	30.748	0.850	1.570	5.962
Colibri2	0.000	0.000	42.004	–	–	7.098
Bitwuzla	0.000	0.000	–	–	–	0.000

MQ2[R1,R2,R3] Effect of Simplifications

Table 3. Speedup achieved with simplifications across the selected SMT-LIB benchmarks.

	QF_FP	QF_BV	QF_LIA	QF_S	QF_SLIA	Total
Z3	1.004	1.014	1.033	1.160	1.146	1.071
cvc5	1.008	0.991	1.046	1.025	0.993	1.013
Colibri2	0.980	0.974	0.999	–	–	0.953
Bitwuzla	1.004	1.016	–	–	–	1.010

Table 4. Speedup achieved with simplifications across the case-study benchmarks.

	array-examples	array-industry	eca-rers	Total
Z3	2.50	1.49	1.70	2.14

MQ3[R1,R2] Effect of caching

Table 5. Speedup achieved with caching across the case-study benchmarks.

	array-examples	array-industry	eca-rers	Total
Z3	1.52	1.36	2.89	1.92

MQ4[R1] Effect of hash-consing (memory & time)

Table 6. Effect of hash-consing on memory usage across the case-study benchmarks.

	array-examples	array-industry	eca-rers	Total
Memory (Z3)	0.942	0.963	0.960	0.949