CBMC: Add more cvc5 proofs by mkannwischer · Pull Request #1491 · pq-code-package/mldsa-native

mkannwischer · 2026-10-24T16:04:28Z

Depends on CBMC: Use a second solver for 149/215 proofs #1423

A soundness bug in a single SMT solver would silently invalidate every proof discharged by it. To mitigate this risk, we aim to have each proof discharged by at least two solvers. 149 of 215 proofs gain a second solver: 98 bitwuzla, 25 cvc5_arrays_exp, and 26 Z3 profiles alongside a bitwuzla or cvc5 default. The other 66 do not, mostly because bitwuzla timed out or cvc5 returned unknown, either under a local 300s per-proof cap or in CI. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

oqs-bot · 2026-10-24T16:31:59Z

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	91s	50s	+82%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	21s	9s	+133%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	342s	58s	+490%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	76s	3s	+2433%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	20s	5s	+300%
`poly_caddq_native`	LP64	bitwuzla	⚠️	101s	5s	+1920%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	34s	4s	+750%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	114s	4s	+2750%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	3s	+633%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	42s	4s	+950%
`poly_ntt_c`	LP64	bitwuzla	⚠️	47s	19s	+147%
`poly_ntt_native`	LP64	bitwuzla	⚠️	25s	5s	+400%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	56s	2s	+2700%
`poly_power2round`	LP64	bitwuzla	⚠️	235s	4s	+5775%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	22s	4s	+450%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	91s	4s	+2175%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	32s	2s	+1500%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	27s	2s	+1250%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	⚠️	38s	3s	+1167%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	⚠️	39s	2s	+1850%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	31s	2s	+1450%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	28s	2s	+1300%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	2s	+1200%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	49s	2s	+2350%
	LP64	z3*	⚠️	24s	2s	+1100%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	28s	5s	+460%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	205s	26s	+688%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	339s	114s	+197%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	28s	3s	+833%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	28s	2s	+1300%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	28s	2s	+1300%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	⚠️	237s	1s	+23600%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	⚠️	239s	4s	+5875%
`yvec_get_poly`	LP64	bitwuzla	⚠️	29s	3s	+867%
`yvec_init`	LP64	bitwuzla	⚠️	37s	3s	+1133%

Full Results (397 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1887s	1514s	+24.6%
`caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	91s	50s	+82%
`decompose`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`fqmul`	LP64	bitwuzla*	✅	23s	39s	-41%
	LP64	z3_smt_only	✅	18s	39s	-54%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	21s	9s	+133%
	LP64	z3*	✅	4s	9s	-56%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	7s	-	new
	LP64	z3	✅	4s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	16s	4s	+300%
	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	4s	5s	-20%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	9s	-56%
	LP64	cvc5_arrays_exp	✅	7s	9s	-22%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	1s	+200%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_init`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	22s	-45%
	LP64	z3*	✅	11s	22s	-50%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	342s	58s	+490%
`mld_check_pct`	LP64	bitwuzla	✅	4s	14s	-71%
	LP64	z3*	✅	5s	14s	-64%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	3s	7s	-57%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	1s	2s	-50%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	⚠️	76s	3s	+2433%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`mld_invntt_layer`	LP64	bitwuzla*	✅	60s	107s	-44%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	8s	-62%
	LP64	z3*	✅	3s	8s	-62%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	23s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	42s	-45%
	LP64	z3_no_bv_extract	✅	2s	42s	-95%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	5s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	89s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	4s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	5s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	5s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	17s	3s	+467%
	LP64	z3*	✅	3s	3s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	1s	+100%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	2s	4s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	7s	-29%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	20s	5s	+300%
	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	7s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	7s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	✅	19s	4s	+375%
	LP64	z3*	✅	2s	4s	-50%
`poly_add`	LP64	z3*	✅	2s	7s	-71%
`poly_caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	2s	+850%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native`	LP64	bitwuzla	⚠️	101s	5s	+1920%
	LP64	z3*	✅	2s	5s	-60%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	34s	4s	+750%
	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	114s	4s	+2750%
	LP64	z3*	✅	2s	4s	-50%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	17s	-59%
	LP64	z3*	✅	6s	17s	-65%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_c`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_native`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	4s	-25%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	11s	-36%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	42s	4s	+950%
	LP64	z3*	✅	1s	4s	-75%
`poly_ntt`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt_c`	LP64	bitwuzla	⚠️	47s	19s	+147%
	LP64	z3_smt_only*	✅	10s	19s	-47%
`poly_ntt_native`	LP64	bitwuzla	⚠️	25s	5s	+400%
	LP64	z3*	✅	1s	5s	-80%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	43s	114s	-62%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	56s	2s	+2700%
	LP64	z3*	✅	1s	2s	-50%
`poly_power2round`	LP64	bitwuzla	⚠️	235s	4s	+5775%
	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	1s	3s	-67%
`poly_shiftl`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	4s	3s	+33%
`poly_sub`	LP64	bitwuzla	✅	12s	3s	+300%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	3s	6s	-50%
`poly_uniform_4x`	LP64	z3*	✅	5s	14s	-64%
`poly_uniform_eta`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	11s	-18%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	1s	5s	-80%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	22s	4s	+450%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	10s	3s	+233%
	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	91s	4s	+2175%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	32s	2s	+1500%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	33s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	14s	-93%
	LP64	z3*	✅	6s	14s	-57%
`polyt0_pack`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	3s	2s	+50%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	15s	-87%
	LP64	z3*	✅	7s	15s	-53%
`polyt1_pack`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`polyt1_unpack`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	5s	-80%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	15s	28s	-46%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	4s	8s	-50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	12s	15s	-20%
`polyveck_caddq`	LP64	z3*	✅	1s	3s	-67%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	2s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	5s	-20%
`polyveck_ntt`	LP64	z3*	✅	3s	5s	-40%
`polyveck_reduce`	LP64	z3*	✅	2s	5s	-60%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	27s	2s	+1250%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	15s	-	new
	LP64	z3*	✅	3s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	5s	10s	-50%
`polyvecl_ntt`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	6s	4s	+50%
	LP64	z3_smt_only*	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	122s	131s	-7%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	⚠️	38s	3s	+1167%
	LP64	z3*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	⚠️	39s	2s	+1850%
	LP64	z3*	✅	5s	2s	+150%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	31s	2s	+1450%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	28s	2s	+1300%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	4s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	11s	-91%
	LP64	z3*	✅	7s	11s	-36%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	2s	+1200%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`reduce32`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	1s	2s	-50%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	15s	4s	+275%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	12s	6s	+100%
`rej_uniform`	LP64	bitwuzla	✅	1s	18s	-94%
	LP64	z3*	✅	12s	18s	-33%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	10s	15s	-33%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	15s	4s	+275%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	z3_smt_only	✅	2s	5s	-60%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3_smt_only*	✅	8s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_release`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`shake256`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake256_absorb`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`shake256_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	2s	4s	-50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	49s	2s	+2350%
	LP64	z3*	⚠️	24s	2s	+1100%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	15s	4s	+275%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	28s	5s	+460%
`sign_signature`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	z3*	✅	6s	4s	+50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	205s	26s	+688%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	3s	6s	-50%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	339s	114s	+197%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	28s	3s	+833%
	LP64	z3*	✅	3s	3s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	28s	2s	+1300%
	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	28s	2s	+1300%
	LP64	z3*	✅	1s	2s	-50%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	5s	+100%
	LP64	z3*	✅	2s	5s	-60%
`unpack_sk`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	⚠️	237s	1s	+23600%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	⚠️	239s	4s	+5875%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	3s	-33%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	bitwuzla	⚠️	29s	3s	+867%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	⚠️	37s	3s	+1133%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-10-24T16:52:38Z

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	138s	13s	+962%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	21s	3s	+600%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	197s	63s	+213%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	79s	2s	+3850%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	20s	5s	+300%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	3s	+633%
`poly_caddq_native`	LP64	bitwuzla	⚠️	105s	2s	+5150%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	34s	2s	+1600%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	113s	3s	+3667%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	6s	+267%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	43s	2s	+2050%
`poly_ntt_c`	LP64	bitwuzla	⚠️	45s	19s	+137%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	4s	+550%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	57s	3s	+1800%
`poly_power2round`	LP64	bitwuzla	⚠️	264s	4s	+6500%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	25s	3s	+733%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	92s	2s	+4500%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	26s	3s	+767%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	41s	6s	+583%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	⚠️	33s	2s	+1550%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	⚠️	34s	3s	+1033%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	33s	3s	+1000%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	32s	3s	+967%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	24s	4s	+500%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1325s	2s	+66150%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	34s	6s	+467%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	198s	55s	+260%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	332s	3s	+10967%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	437s	177s	+147%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	37s	6s	+517%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	⚠️	85s	2s	+4150%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	⚠️	154s	4s	+3750%
`yvec_get_poly`	LP64	bitwuzla	⚠️	32s	3s	+967%

Full Results (397 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1976s	1784s	+10.8%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	138s	13s	+962%
`decompose`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`fqmul`	LP64	bitwuzla*	✅	24s	40s	-40%
	LP64	z3_smt_only	✅	22s	40s	-45%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	4s	3s	+33%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	21s	3s	+600%
	LP64	z3*	✅	1s	3s	-67%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	15s	3s	+400%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	8s	-50%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	1s	4s	-75%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3	✅	2s	5s	-60%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	3s	4s	-25%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	23s	-43%
	LP64	z3*	✅	14s	23s	-39%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	5s	3s	+67%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	197s	63s	+213%
`mld_check_pct`	LP64	bitwuzla	✅	4s	14s	-71%
	LP64	z3*	✅	5s	14s	-64%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	7s	-71%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	2s	+50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	⚠️	79s	2s	+3850%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	60s	109s	-45%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	4s	6s	-33%
	LP64	z3*	✅	3s	6s	-50%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	24s	-50%
`mld_ntt_layer`	LP64	bitwuzla*	✅	24s	41s	-41%
	LP64	z3_no_bv_extract	✅	4s	41s	-90%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	5s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	223s	-	new
	LP64	z3*	✅	4s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	2s	+850%
	LP64	z3*	✅	3s	2s	+50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	4s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	15s	2s	+650%
	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	1s	5s	-80%
`pack_sig_h`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3_no_bv_extract*	✅	2s	5s	-60%
`pack_sig_z`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	1s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	2s	6s	-67%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	8s	-62%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	20s	5s	+300%
	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	2s	3s	-33%
`poly_add`	LP64	z3*	✅	3s	9s	-67%
`poly_caddq`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	2s	+800%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	bitwuzla	⚠️	105s	2s	+5150%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	34s	2s	+1600%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	113s	3s	+3667%
	LP64	z3*	✅	3s	3s	+0%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	6s	+267%
	LP64	z3*	✅	3s	6s	-50%
`poly_chknorm`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	15s	-33%
	LP64	z3*	✅	5s	15s	-67%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	4s	3s	+33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_c`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_native_x86_64`	LP64	z3*	✅	4s	3s	+33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	11s	-36%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	43s	2s	+2050%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	3s	2s	+50%
`poly_ntt_c`	LP64	bitwuzla	⚠️	45s	19s	+137%
	LP64	z3_smt_only*	✅	10s	19s	-47%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	4s	+550%
	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	47s	125s	-62%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	57s	3s	+1800%
	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	bitwuzla	⚠️	264s	4s	+6500%
	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	4s	3s	+33%
`poly_sub`	LP64	bitwuzla	✅	12s	3s	+300%
	LP64	z3*	✅	4s	3s	+33%
`poly_uniform`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_4x`	LP64	z3*	✅	7s	13s	-46%
`poly_uniform_eta`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_eta_4x`	LP64	z3*	✅	6s	14s	-57%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	6s	4s	+50%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	25s	3s	+733%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	5s	+140%
	LP64	z3*	✅	1s	5s	-80%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	92s	2s	+4500%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	26s	3s	+767%
	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	28s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	8s	-88%
	LP64	z3*	✅	4s	8s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	16s	-75%
	LP64	z3*	✅	8s	16s	-50%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	5s	-20%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	69s	110s	-37%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	14s	27s	-48%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	2s	1s	+100%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	18s	18s	+0%
`polyveck_caddq`	LP64	z3*	✅	6s	6s	+0%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	7s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	8s	-38%
`polyveck_ntt`	LP64	z3*	✅	5s	7s	-29%
`polyveck_reduce`	LP64	z3*	✅	3s	4s	-25%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	41s	6s	+583%
	LP64	z3*	✅	2s	6s	-67%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	17s	-	new
	LP64	z3*	✅	2s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	1s	7s	-86%
`polyvecl_ntt`	LP64	z3*	✅	5s	4s	+25%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	9s	3s	+200%
	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	120s	210s	-43%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	⚠️	33s	2s	+1550%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	⚠️	34s	3s	+1033%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	33s	3s	+1000%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	32s	3s	+967%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	5s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	1s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	13s	-85%
	LP64	z3*	✅	3s	13s	-77%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	24s	4s	+500%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	1s	3s	-67%
`power2round`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`reduce32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	10s	5s	+100%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	9s	3s	+200%
`rej_uniform`	LP64	bitwuzla	✅	1s	18s	-94%
	LP64	z3*	✅	11s	18s	-39%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	14s	-86%
	LP64	z3*	✅	11s	14s	-21%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	✅	18s	4s	+350%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3_smt_only*	✅	8s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`shake128_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	3s	3s	+0%
`shake256`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	4s	3s	+33%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	3s	2s	+50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1325s	2s	+66150%
	LP64	z3*	✅	19s	2s	+850%
`sign_keypair`	LP64	z3*	✅	4s	3s	+33%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	17s	5s	+240%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	34s	6s	+467%
`sign_signature`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	3s	6s	-50%
`sign_signature_extmu`	LP64	z3*	✅	3s	2s	+50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	198s	55s	+260%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	332s	3s	+10967%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	437s	177s	+147%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	37s	6s	+517%
	LP64	z3*	✅	1s	6s	-83%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
	LP64	z3*	✅	4s	2s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	4s	4s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	5s	+140%
	LP64	z3*	✅	3s	5s	-40%
`unpack_sk`	LP64	z3*	✅	4s	3s	+33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	⚠️	85s	2s	+4150%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	⚠️	154s	4s	+3750%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	6s	5s	+20%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	⚠️	32s	3s	+967%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	3s	3s	+0%

oqs-bot · 2026-10-24T16:54:20Z

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	3516s	2151s	+63.5%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	263s	19s	+1284%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	351s	55s	+538%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	83s	3s	+2667%
`mld_sample_pack_s1_s2`	LP64	bitwuzla	❌	-	-	-
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	6s	+283%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	25s	5s	+400%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
`poly_caddq_native`	LP64	bitwuzla	⚠️	116s	4s	+2800%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	35s	3s	+1067%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	131s	2s	+6450%
`poly_challenge`	LP64	bitwuzla	⚠️	36s	5s	+620%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	47s	5s	+840%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	21s	+143%
`poly_ntt_native`	LP64	bitwuzla	⚠️	28s	3s	+833%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	52s	5s	+940%
`poly_power2round`	LP64	bitwuzla	⚠️	324s	3s	+10700%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	22s	1s	+2100%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	92s	3s	+2967%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	33s	2s	+1550%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	56s	4s	+1300%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	⚠️	80s	2s	+3900%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	⚠️	45s	4s	+1025%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	47s	5s	+840%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	43s	4s	+975%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	4s	+575%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	27s	3s	+800%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	22s	6s	+267%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	37s	6s	+517%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	406s	42s	+867%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1695s	6s	+28150%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	1304s	97s	+1244%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	32s	3s	+967%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	34s	3s	+1033%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	35s	4s	+775%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	⚠️	88s	2s	+4300%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	⚠️	310s	3s	+10233%
`yvec_get_poly`	LP64	bitwuzla	⚠️	37s	4s	+825%

Full Results (398 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	3516s	2151s	+63.5%
`caddq`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	263s	19s	+1284%
`decompose`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	25s	43s	-42%
	LP64	z3_smt_only	✅	22s	43s	-49%
`fqscale`	LP64	bitwuzla*	✅	5s	3s	+67%
	LP64	z3	✅	4s	3s	+33%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	1s	3s	-67%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	10s	-	new
	LP64	z3	✅	4s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	9s	-44%
	LP64	cvc5_arrays_exp	✅	8s	9s	-11%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	3s	4s	-25%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccak_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	4s	2s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	15s	23s	-35%
	LP64	z3*	✅	12s	23s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	351s	55s	+538%
`mld_check_pct`	LP64	bitwuzla	✅	5s	16s	-69%
	LP64	z3*	✅	5s	16s	-69%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	5s	8s	-38%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	1s	3s	-67%
	ILP32	z3	✅	2s	3s	-33%
	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	5s	4s	+25%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_no_bv_extract	⚠️	83s	3s	+2667%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	66s	115s	-43%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	7s	-57%
	LP64	z3*	✅	4s	7s	-43%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	24s	-42%
`mld_ntt_layer`	LP64	bitwuzla*	✅	26s	45s	-42%
	LP64	z3_no_bv_extract	✅	4s	45s	-91%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_pack_s1_s2`	LP64	bitwuzla	❌	-	-	-
	LP64	z3*	✅	8s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	554s	-	new
	LP64	z3*	✅	4s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	5s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	6s	+283%
	LP64	z3*	✅	4s	6s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	6s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	5s	-	new
	LP64	z3	✅	4s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	2s	+800%
	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	z3*	✅	4s	3s	+33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`pack_sig_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	25s	5s	+400%
	LP64	z3*	✅	1s	5s	-80%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	4s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
	LP64	z3*	✅	5s	2s	+150%
`poly_add`	LP64	z3*	✅	6s	6s	+0%
`poly_caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native`	LP64	bitwuzla	⚠️	116s	4s	+2800%
	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	35s	3s	+1067%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	131s	2s	+6450%
	LP64	z3*	✅	2s	2s	+0%
`poly_challenge`	LP64	bitwuzla	⚠️	36s	5s	+620%
	LP64	z3*	✅	3s	5s	-40%
`poly_chknorm`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	15s	-33%
	LP64	z3*	✅	7s	15s	-53%
`poly_chknorm_native`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_c`	LP64	z3*	✅	5s	5s	+0%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	9s	12s	-25%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	47s	5s	+840%
	LP64	z3*	✅	2s	5s	-60%
`poly_ntt`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	21s	+143%
	LP64	z3_smt_only*	✅	11s	21s	-48%
`poly_ntt_native`	LP64	bitwuzla	⚠️	28s	3s	+833%
	LP64	z3*	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	5s	-40%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	4s	+150%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	48s	144s	-67%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	52s	5s	+940%
	LP64	z3*	✅	1s	5s	-80%
`poly_power2round`	LP64	bitwuzla	⚠️	324s	3s	+10700%
	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	2s	2s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	11s	4s	+175%
	LP64	z3*	✅	3s	4s	-25%
`poly_sub`	LP64	bitwuzla	✅	15s	3s	+400%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_4x`	LP64	z3*	✅	7s	13s	-46%
`poly_uniform_eta`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	11s	-18%
`poly_uniform_gamma1`	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	22s	1s	+2100%
	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	2s	+500%
	LP64	z3*	✅	4s	2s	+100%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	92s	3s	+2967%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	33s	2s	+1550%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	6s	4s	+50%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	17s	-94%
	LP64	z3*	✅	7s	17s	-59%
`polyt0_pack`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	14s	-86%
	LP64	z3*	✅	8s	14s	-43%
`polyt1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	114s	324s	-65%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	25s	38s	-34%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	16s	18s	-11%
`polyveck_caddq`	LP64	z3*	✅	6s	8s	-25%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	7s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	9s	-44%
`polyveck_ntt`	LP64	z3*	✅	6s	11s	-45%
`polyveck_reduce`	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	56s	4s	+1300%
	LP64	z3*	✅	6s	4s	+50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	-	new
	LP64	z3*	✅	3s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_ntt`	LP64	z3*	✅	7s	7s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	15s	5s	+200%
	LP64	z3_smt_only*	✅	2s	5s	-60%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	159s	353s	-55%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	⚠️	80s	2s	+3900%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	⚠️	45s	4s	+1025%
	LP64	z3*	✅	3s	4s	-25%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	47s	5s	+840%
	LP64	z3*	✅	1s	5s	-80%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	43s	4s	+975%
	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	6s	3s	+100%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	4s	+575%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	4s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	4s	4s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3	✅	17s	5s	+240%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	12s	6s	+100%
`rej_uniform`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	12s	15s	-20%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	19s	-89%
	LP64	z3*	✅	10s	19s	-47%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	1s	5s	-80%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	8s	-75%
	LP64	z3_smt_only	✅	19s	8s	+138%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake128_init`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake128_release`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	3s	5s	-40%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`shake256`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	27s	3s	+800%
	LP64	z3*	✅	15s	3s	+400%
`sign_keypair`	LP64	z3*	✅	4s	4s	+0%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	22s	6s	+267%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	37s	6s	+517%
`sign_signature`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	5s	5s	+0%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	406s	42s	+867%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	6s	5s	+20%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1695s	6s	+28150%
	LP64	z3*	✅	7s	6s	+17%
`sign_verify`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	1304s	97s	+1244%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	32s	3s	+967%
	LP64	z3*	✅	3s	3s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	34s	3s	+1033%
	LP64	z3*	✅	1s	3s	-67%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	35s	4s	+775%
	LP64	z3*	✅	2s	4s	-50%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	1s	+1100%
	LP64	z3*	✅	4s	1s	+300%
`unpack_sk`	LP64	z3*	✅	4s	5s	-20%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	⚠️	88s	2s	+4300%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	⚠️	310s	3s	+10233%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	z3*	✅	3s	7s	-57%
`use_hint`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	bitwuzla	⚠️	37s	4s	+825%
	LP64	z3*	✅	3s	4s	-25%
`yvec_init`	LP64	bitwuzla	✅	17s	4s	+325%
	LP64	z3*	✅	1s	4s	-75%

oqs-bot · 2026-10-24T16:55:16Z

CBMC Results (ML-DSA-44, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	30s	12s	+150%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	20s	3s	+567%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	143s	19s	+653%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	82s	1s	+8100%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	21s	4s	+425%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	20s	2s	+900%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	4s	+450%
`poly_caddq_native`	LP64	bitwuzla	⚠️	108s	3s	+3500%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	36s	3s	+1100%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	106s	4s	+2550%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	6s	+267%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	42s	3s	+1300%
`poly_ntt_c`	LP64	bitwuzla	⚠️	50s	21s	+138%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	52s	2s	+2500%
`poly_power2round`	LP64	bitwuzla	⚠️	249s	4s	+6125%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	25s	2s	+1150%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	89s	3s	+2867%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	3s	+933%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	32s	4s	+700%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	26s	3s	+767%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	25s	3s	+733%
`rej_eta_c`	LP64	z3	⚠️	21s	4s	+425%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	51s	2s	+2450%
	LP64	z3*	⚠️	36s	2s	+1700%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	31s	5s	+520%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	242s	49s	+394%

Full Results (397 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1368s	1364s	+0.3%
`caddq`	LP64	bitwuzla	✅	1s	6s	-83%
	LP64	z3*	✅	2s	6s	-67%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	30s	12s	+150%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	24s	39s	-38%
	LP64	z3_smt_only	✅	21s	39s	-46%
`fqscale`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	20s	3s	+567%
	LP64	z3*	✅	1s	3s	-67%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	7s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	17s	2s	+750%
	LP64	z3*	✅	2s	2s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	8s	-50%
	LP64	cvc5_arrays_exp	✅	9s	8s	+12%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccak_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	6s	-83%
	LP64	z3_smt_only	✅	1s	6s	-83%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	22s	-45%
	LP64	z3*	✅	13s	22s	-41%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_no_bv_extract	✅	1s	5s	-80%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	143s	19s	+653%
`mld_check_pct`	LP64	bitwuzla	✅	6s	15s	-60%
	LP64	z3*	✅	5s	15s	-67%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	1s	6s	-83%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	1s	3s	-67%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	5s	3s	+67%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	⚠️	82s	1s	+8100%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_invntt_layer`	LP64	bitwuzla*	✅	64s	105s	-39%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	7s	-57%
	LP64	z3*	✅	5s	7s	-29%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	23s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	24s	41s	-41%
	LP64	z3_no_bv_extract	✅	1s	41s	-98%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	2s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	89s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	21s	4s	+425%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	6s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	3s	3s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	4s	-75%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`pack_sig_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	3s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	2s	6s	-67%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	20s	2s	+900%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	7s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	4s	+450%
	LP64	z3*	✅	4s	4s	+0%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	108s	3s	+3500%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	36s	3s	+1100%
	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	106s	4s	+2550%
	LP64	z3*	✅	2s	4s	-50%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	6s	+267%
	LP64	z3*	✅	2s	6s	-67%
`poly_chknorm`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	8s	11s	-27%
	LP64	z3*	✅	6s	11s	-45%
`poly_chknorm_native`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	4s	4s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_c`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native`	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	11s	-45%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	42s	3s	+1300%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	3s	+33%
`poly_ntt_c`	LP64	bitwuzla	⚠️	50s	21s	+138%
	LP64	z3_smt_only*	✅	11s	21s	-48%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
	LP64	z3*	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	5s	3s	+67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	74s	112s	-34%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	52s	2s	+2500%
	LP64	z3*	✅	4s	2s	+100%
`poly_power2round`	LP64	bitwuzla	⚠️	249s	4s	+6125%
	LP64	z3*	✅	2s	4s	-50%
`poly_reduce`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	12s	4s	+200%
	LP64	z3*	✅	5s	4s	+25%
`poly_sub`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_eta`	LP64	z3*	✅	1s	2s	-50%
`poly_uniform_eta_4x`	LP64	z3*	✅	5s	12s	-58%
`poly_uniform_gamma1`	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	25s	2s	+1150%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	10s	5s	+100%
	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	89s	3s	+2867%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	3s	+933%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	32s	-	new
	LP64	z3*	✅	1s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	4s	14s	-71%
	LP64	z3*	✅	7s	14s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	12s	-83%
	LP64	z3*	✅	7s	12s	-42%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyt1_unpack`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	4s	4s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	6s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	131s	149s	-12%
`polyveck_caddq`	LP64	z3*	✅	5s	3s	+67%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	7s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	3s	5s	-40%
`polyveck_ntt`	LP64	z3*	✅	2s	2s	+0%
`polyveck_reduce`	LP64	z3*	✅	2s	4s	-50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	15s	-	new
	LP64	z3*	✅	2s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	3s	11s	-73%
`polyvecl_ntt`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	4s	3s	+33%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	32s	4s	+700%
	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	26s	3s	+767%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	8s	-75%
	LP64	z3*	✅	5s	8s	-38%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	25s	3s	+733%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	⚠️	21s	4s	+425%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	11s	3s	+267%
`rej_uniform`	LP64	bitwuzla	✅	4s	8s	-50%
	LP64	z3*	✅	5s	8s	-38%
`rej_uniform_c`	LP64	bitwuzla	✅	1s	16s	-94%
	LP64	z3*	✅	9s	16s	-44%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3_smt_only	✅	17s	5s	+240%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	10s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`shake128_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	1s	+300%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`shake256_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	51s	2s	+2450%
	LP64	z3*	⚠️	36s	2s	+1700%
`sign_keypair`	LP64	z3*	✅	4s	5s	-20%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	12s	4s	+200%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	31s	5s	+520%
`sign_signature`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	3s	6s	-50%
`sign_signature_extmu`	LP64	z3*	✅	5s	4s	+25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	12s	4s	+200%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	242s	49s	+394%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	1s	5s	-80%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	3s	+300%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`unpack_sk_t0hat`	LP64	z3*	✅	1s	2s	-50%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`yvec_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%

oqs-bot · 2026-10-24T16:55:19Z

CBMC Results (ML-DSA-65, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	39s	7s	+457%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	24s	2s	+1100%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	20s	4s	+400%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	221s	31s	+613%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	93s	4s	+2225%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	3s	+667%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	24s	2s	+1100%
`poly_caddq_c`	LP64	bitwuzla	⚠️	21s	5s	+320%
`poly_caddq_native`	LP64	bitwuzla	⚠️	124s	4s	+3000%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	40s	2s	+1900%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	128s	1s	+12700%
`poly_challenge`	LP64	bitwuzla	⚠️	26s	5s	+420%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	49s	5s	+880%
`poly_ntt_c`	LP64	bitwuzla	⚠️	53s	22s	+141%
`poly_ntt_native`	LP64	bitwuzla	⚠️	31s	2s	+1450%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	55s	4s	+1275%
`poly_power2round`	LP64	bitwuzla	⚠️	288s	7s	+4014%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	24s	3s	+700%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	79s	7s	+1029%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	4s	+675%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	35s	2s	+1650%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	37s	1s	+3600%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	29s	3s	+867%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	20s	4s	+400%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1532s	1s	+153100%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	21s	3s	+600%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	37s	5s	+640%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	399s	7s	+5600%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	219s	71s	+208%

Full Results (398 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1502s	1482s	+1.3%
`caddq`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	39s	7s	+457%
`decompose`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`fqmul`	LP64	bitwuzla*	✅	25s	40s	-38%
	LP64	z3_smt_only	✅	20s	40s	-50%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	24s	2s	+1100%
	LP64	z3*	✅	3s	2s	+50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	7s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	bitwuzla	⚠️	20s	4s	+400%
	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	10s	-50%
	LP64	cvc5_arrays_exp	✅	8s	10s	-20%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`keccak_squeeze`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	4s	4s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	22s	-45%
	LP64	z3*	✅	13s	22s	-41%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	5s	3s	+67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	221s	31s	+613%
`mld_check_pct`	LP64	bitwuzla	✅	4s	12s	-67%
	LP64	z3*	✅	5s	12s	-58%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	6s	-83%
	ILP32	cvc5_arrays_exp	✅	2s	6s	-67%
	ILP32	z3	✅	3s	6s	-50%
	LP64	bitwuzla	✅	1s	6s	-83%
	LP64	cvc5_arrays_exp	✅	3s	6s	-50%
	LP64	z3*	✅	3s	6s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	2s	4s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_no_bv_extract	⚠️	93s	4s	+2225%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	71s	108s	-34%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	7s	-57%
	LP64	z3*	✅	5s	7s	-29%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	25s	-44%
`mld_ntt_layer`	LP64	bitwuzla*	✅	26s	43s	-40%
	LP64	z3_no_bv_extract	✅	2s	43s	-95%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
`mld_sample_pack_s1_s2`	LP64	bitwuzla	✅	1284s	-	new
	LP64	z3*	✅	5s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	237s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	1s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	3s	3s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	6s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	5s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	5s	+260%
	LP64	z3*	✅	2s	5s	-60%
`nttunpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`pack_sig_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	5s	-20%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	3s	+667%
	LP64	z3*	✅	2s	3s	-33%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	10s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	6s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	24s	2s	+1100%
	LP64	z3*	✅	1s	2s	-50%
`poly_add`	LP64	z3*	✅	4s	7s	-43%
`poly_caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_c`	LP64	bitwuzla	⚠️	21s	5s	+320%
	LP64	z3*	✅	6s	5s	+20%
`poly_caddq_native`	LP64	bitwuzla	⚠️	124s	4s	+3000%
	LP64	z3*	✅	3s	4s	-25%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	40s	2s	+1900%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	128s	1s	+12700%
	LP64	z3*	✅	1s	1s	+0%
`poly_challenge`	LP64	bitwuzla	⚠️	26s	5s	+420%
	LP64	z3*	✅	2s	5s	-60%
`poly_chknorm`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	13s	-31%
	LP64	z3*	✅	6s	13s	-54%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	1s	4s	-75%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	5s	2s	+150%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_c`	LP64	z3*	✅	5s	8s	-38%
`poly_decompose_native`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	1s	5s	-80%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	10s	-30%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	49s	5s	+880%
	LP64	z3*	✅	2s	5s	-60%
`poly_ntt`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	53s	22s	+141%
	LP64	z3_smt_only*	✅	9s	22s	-59%
`poly_ntt_native`	LP64	bitwuzla	⚠️	31s	2s	+1450%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	2s	+400%
	LP64	z3*	✅	1s	2s	-50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	82s	116s	-29%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	55s	4s	+1275%
	LP64	z3*	✅	2s	4s	-50%
`poly_power2round`	LP64	bitwuzla	⚠️	288s	7s	+4014%
	LP64	z3*	✅	5s	7s	-29%
`poly_reduce`	LP64	bitwuzla	✅	11s	4s	+175%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	bitwuzla	✅	13s	4s	+225%
	LP64	z3*	✅	4s	4s	+0%
`poly_uniform`	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_4x`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_eta`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	13s	-31%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	24s	3s	+700%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	2s	+500%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	79s	7s	+1029%
	LP64	z3*	✅	4s	7s	-43%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	4s	+675%
	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	33s	-	new
	LP64	z3*	✅	1s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`polyeta_unpack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	5s	4s	+25%
`polyt0_pack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	5s	-60%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	13s	-69%
	LP64	z3*	✅	8s	13s	-38%
`polyt1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	3s	6s	-50%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	6s	8s	-25%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	138s	201s	-31%
`polyveck_caddq`	LP64	z3*	✅	4s	7s	-43%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	8s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	7s	-29%
`polyveck_ntt`	LP64	z3*	✅	2s	4s	-50%
`polyveck_reduce`	LP64	z3*	✅	3s	6s	-50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	20s	-	new
	LP64	z3*	✅	3s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	2s	43s	-95%
`polyvecl_ntt`	LP64	z3*	✅	3s	7s	-57%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	1s	4s	-75%
	LP64	z3*	✅	4s	4s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	35s	2s	+1650%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	37s	1s	+3600%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	4s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	9s	-89%
	LP64	z3*	✅	4s	9s	-56%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	29s	3s	+867%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	1s	3s	-67%
`power2round`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	17s	4s	+325%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	10s	3s	+233%
`rej_uniform`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	6s	7s	-14%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	16s	-88%
	LP64	z3*	✅	10s	16s	-38%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	⚠️	20s	4s	+400%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3_smt_only	✅	2s	5s	-60%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	11s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	2s	6s	-67%
`shake128_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
`shake256`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake256_absorb`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`shake256_release`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	4s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1532s	1s	+153100%
	LP64	z3*	✅	18s	1s	+1700%
`sign_keypair`	LP64	z3*	✅	7s	4s	+75%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	21s	3s	+600%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	37s	5s	+640%
`sign_signature`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	5s	-20%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	16s	6s	+167%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	399s	7s	+5600%
	LP64	z3*	✅	5s	7s	-29%
`sign_verify`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	3s	6s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	219s	71s	+208%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	4s	6s	-33%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`unpack_pk_t1`	LP64	bitwuzla	✅	13s	2s	+550%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	z3*	✅	3s	4s	-25%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	4s	3s	+33%
`yvec_init`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%

oqs-bot · 2026-10-24T16:56:25Z

CBMC Results (ML-DSA-87, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	31s	12s	+158%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	25s	4s	+525%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	224s	34s	+559%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	89s	1s	+8800%
`mld_sample_pack_s1_s2`	LP64	bitwuzla	❌	-	-	-
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	4s	+475%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	4s	+475%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	23s	5s	+360%
`poly_caddq_c`	LP64	bitwuzla	⚠️	20s	3s	+567%
`poly_caddq_native`	LP64	bitwuzla	⚠️	120s	3s	+3900%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	35s	3s	+1067%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	127s	3s	+4133%
`poly_challenge`	LP64	bitwuzla	⚠️	41s	4s	+925%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	49s	2s	+2350%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	19s	+168%
`poly_ntt_native`	LP64	bitwuzla	⚠️	32s	4s	+700%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	54s	3s	+1700%
`poly_power2round`	LP64	bitwuzla	⚠️	293s	7s	+4086%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	23s	4s	+475%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	84s	1s	+8300%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	28s	3s	+833%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	48s	3s	+1500%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	50s	3s	+1567%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	29s	1s	+2800%
`rej_eta_c`	LP64	z3	⚠️	26s	4s	+550%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	29s	4s	+625%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	26s	6s	+333%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	37s	6s	+517%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1741s	3s	+57933%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	277s	47s	+489%

Full Results (398 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1501s	1436s	+4.5%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	31s	12s	+158%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	27s	39s	-31%
	LP64	z3_smt_only	✅	21s	39s	-46%
`fqscale`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	25s	4s	+525%
	LP64	z3*	✅	2s	4s	-50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	4s	+350%
	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	8s	-38%
	LP64	cvc5_arrays_exp	✅	9s	8s	+12%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	2s	5s	-60%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	4s	4s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	25s	-52%
	LP64	z3*	✅	13s	25s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	224s	34s	+559%
`mld_check_pct`	LP64	bitwuzla	✅	5s	15s	-67%
	LP64	z3*	✅	5s	15s	-67%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	1s	+200%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	2s	1s	+100%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	⚠️	89s	1s	+8800%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	70s	111s	-37%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	8s	-38%
	LP64	z3*	✅	3s	8s	-62%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	23s	-39%
`mld_ntt_layer`	LP64	bitwuzla*	✅	28s	44s	-36%
	LP64	z3_no_bv_extract	✅	1s	44s	-98%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_sample_pack_s1_s2`	LP64	bitwuzla	❌	-	-	-
	LP64	z3*	✅	6s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	545s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	4s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	4s	+475%
	LP64	z3*	✅	3s	4s	-25%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	8s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	7s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	2s	+850%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	3s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	5s	-20%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	8s	-38%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	4s	+475%
	LP64	z3*	✅	3s	4s	-25%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	5s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	cvc5_mbqi_enum	✅	9s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	23s	5s	+360%
	LP64	z3*	✅	2s	5s	-60%
`poly_add`	LP64	z3*	✅	2s	8s	-75%
`poly_caddq`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_c`	LP64	bitwuzla	⚠️	20s	3s	+567%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	120s	3s	+3900%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	⚠️	35s	3s	+1067%
	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	127s	3s	+4133%
	LP64	z3*	✅	2s	3s	-33%
`poly_challenge`	LP64	bitwuzla	⚠️	41s	4s	+925%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	6s	13s	-54%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	1s	+500%
	LP64	z3*	✅	3s	1s	+200%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	5s	-80%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	z3*	✅	6s	6s	+0%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	9s	9s	+0%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	49s	2s	+2350%
	LP64	z3*	✅	1s	2s	-50%
`poly_ntt`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	1s	2s	-50%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	19s	+168%
	LP64	z3_smt_only*	✅	13s	19s	-32%
`poly_ntt_native`	LP64	bitwuzla	⚠️	32s	4s	+700%
	LP64	z3*	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	85s	125s	-32%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	⚠️	54s	3s	+1700%
	LP64	z3*	✅	3s	3s	+0%
`poly_power2round`	LP64	bitwuzla	⚠️	293s	7s	+4086%
	LP64	z3*	✅	4s	7s	-43%
`poly_reduce`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	13s	4s	+225%
	LP64	z3*	✅	4s	4s	+0%
`poly_sub`	LP64	bitwuzla	✅	15s	5s	+200%
	LP64	z3*	✅	1s	5s	-80%
`poly_uniform`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_4x`	LP64	z3*	✅	4s	3s	+33%
`poly_uniform_eta`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform_eta_4x`	LP64	z3*	✅	7s	12s	-42%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	⚠️	23s	4s	+475%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	13s	4s	+225%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	⚠️	84s	1s	+8300%
	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	28s	3s	+833%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	29s	-	new
	LP64	z3*	✅	1s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	13s	-85%
	LP64	z3*	✅	10s	13s	-23%
`polyt0_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	8s	14s	-43%
`polyt1_pack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	5s	-80%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	4s	13s	-69%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	94s	196s	-52%
`polyveck_caddq`	LP64	z3*	✅	5s	8s	-38%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	14s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	4s	+25%
`polyveck_ntt`	LP64	z3*	✅	2s	3s	-33%
`polyveck_reduce`	LP64	z3*	✅	3s	6s	-50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	-	new
	LP64	z3*	✅	1s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	1s	38s	-97%
`polyvecl_ntt`	LP64	z3*	✅	4s	8s	-50%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	⚠️	48s	3s	+1500%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	⚠️	50s	3s	+1567%
	LP64	z3*	✅	1s	3s	-67%
`polyw1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	4s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	4s	7s	-43%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	29s	1s	+2800%
	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	15s	3s	+400%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	4s	2s	+100%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	⚠️	26s	4s	+550%
`rej_eta_native`	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	z3_smt_only	✅	13s	4s	+225%
`rej_uniform`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	7s	7s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	18s	-89%
	LP64	z3*	✅	8s	18s	-56%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	1s	3s	-67%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	19s	5s	+280%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	3s	-67%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	2s	4s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`shake256_absorb`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`shake256_release`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3	✅	3s	5s	-40%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	29s	4s	+625%
	LP64	z3*	✅	18s	4s	+350%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	26s	6s	+333%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	37s	6s	+517%
`sign_signature`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	6s	4s	+50%
`sign_signature_extmu`	LP64	z3*	✅	2s	4s	-50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	16s	3s	+433%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1741s	3s	+57933%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	277s	47s	+489%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	7s	-57%
	LP64	z3*	✅	2s	7s	-71%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`unpack_pk_t1`	LP64	bitwuzla	✅	14s	2s	+600%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk`	LP64	z3*	✅	3s	4s	-25%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	z3*	✅	3s	4s	-25%
`use_hint`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`yvec_get_poly`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	1s	2s	-50%
`yvec_init`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%

cvc5_arrays_exp returns unknown on most proofs that lack a second solver, because cvc5 gives up on quantifier instantiation by default. Add two cvc5 profiles that instantiate more aggressively: - cvc5_mbqi_enum: --mbqi --mbqi-enum - cvc5_enum_inst: --enum-inst Use them as a second solver for 21 proofs that discharge in about 150s or less locally: 20 with cvc5_mbqi_enum, and poly_use_hint_c with cvc5_enum_inst. Also add bitwuzla as a second solver for poly_power2round. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer force-pushed the cbmc-more-cvc5-proofs branch from cf5b97b to bba1f42 Compare October 25, 2026 04:44

mkannwischer force-pushed the cbmc-more-cvc5-proofs branch from bba1f42 to 721f3e7 Compare October 25, 2026 04:45

mkannwischer marked this pull request as ready for review October 25, 2026 05:51

mkannwischer requested a review from a team as a code owner October 25, 2026 05:51

hanno-becker approved these changes Oct 25, 2026

View reviewed changes

hanno-becker added this pull request to the merge queue Oct 25, 2026

Merged via the queue into main with commit 4ec47ce Oct 25, 2026
402 checks passed

hanno-becker deleted the cbmc-more-cvc5-proofs branch October 25, 2026 08:09

Navigation Menu

Repository navigation

CBMC: Add more cvc5 proofs - #1491

CBMC: Add more cvc5 proofs#1491
hanno-becker merged 2 commits into
mainfrom
cbmc-more-cvc5-proofs

mkannwischer commented Oct 24, 2026

Uh oh!

oqs-bot commented Oct 24, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 24, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 24, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 24, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 24, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 24, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mkannwischer commented Oct 24, 2026

Uh oh!

oqs-bot commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

oqs-bot commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-44, REDUCE-RAM)

Uh oh!

oqs-bot commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-65, REDUCE-RAM)

Uh oh!

oqs-bot commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87, REDUCE-RAM)

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Oct 24, 2026 •

edited

Loading

oqs-bot commented Oct 24, 2026 •

edited

Loading

oqs-bot commented Oct 24, 2026 •

edited

Loading

oqs-bot commented Oct 24, 2026 •

edited

Loading

oqs-bot commented Oct 24, 2026 •

edited

Loading

oqs-bot commented Oct 24, 2026 •

edited

Loading