CBMC: Use a second solver for 149/215 proofs by mkannwischer · Pull Request #1423 · pq-code-package/mldsa-native

mkannwischer · 2026-09-09T15:05:18Z

No description provided.

oqs-bot · 2026-09-09T15:29:06Z

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*	⚠️	28s	12s	+133%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	125s	19s	+558%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	79s	1s	+7800%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	20s	4s	+400%
`poly_caddq_native`	LP64	bitwuzla	⚠️	99s	3s	+3200%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	109s	4s	+2625%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	6s	+267%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	45s	3s	+1400%
`poly_ntt_c`	LP64	bitwuzla	⚠️	43s	21s	+105%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	3s	+933%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	23s	3s	+667%
`rej_eta_c`	LP64	z3	⚠️	22s	4s	+450%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	52s	2s	+2500%
	LP64	z3*	⚠️	33s	2s	+1550%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	29s	5s	+480%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	239s	49s	+388%

Full Results (375 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1332s	1364s	-2.3%
`caddq`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	1s	6s	-83%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	28s	12s	+133%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	24s	39s	-38%
	LP64	z3_smt_only	✅	20s	39s	-49%
`fqscale`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`intt_native_aarch64`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	15s	2s	+650%
	LP64	z3*	✅	2s	2s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	8s	-25%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_no_bv_extract	✅	3s	3s	+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*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`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*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	2s	6s	-67%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	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*	✅	14s	22s	-36%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_no_bv_extract	✅	2s	5s	-60%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	125s	19s	+558%
`mld_check_pct`	LP64	bitwuzla	✅	5s	15s	-67%
	LP64	z3*	✅	6s	15s	-60%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	3s	6s	-50%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	3s	3s	+0%
	ILP32	z3	✅	2s	3s	-33%
	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`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	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	⚠️	79s	1s	+7800%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	63s	105s	-40%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	7s	-57%
	LP64	z3*	✅	3s	7s	-57%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	23s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	22s	41s	-46%
	LP64	z3_no_bv_extract	✅	4s	41s	-90%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	2s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	z3*	✅	3s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	4s	+350%
	LP64	z3*	✅	6s	4s	+50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	17s	3s	+467%
	LP64	z3*	✅	5s	3s	+67%
`nttunpack_native_x86_64`	LP64	z3*	✅	3s	4s	-25%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`pack_sig_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_no_bv_extract*	✅	3s	4s	-25%
`pack_sig_z`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`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	4s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	18s	2s	+800%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	5s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	20s	4s	+400%
	LP64	z3*	✅	3s	4s	-25%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	99s	3s	+3200%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	109s	4s	+2625%
	LP64	z3*	✅	1s	4s	-75%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	6s	+267%
	LP64	z3*	✅	2s	6s	-67%
`poly_chknorm`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	11s	-36%
	LP64	z3*	✅	6s	11s	-45%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_c`	LP64	z3*	✅	4s	5s	-20%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	11s	-36%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	45s	3s	+1400%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`poly_ntt_c`	LP64	bitwuzla	⚠️	43s	21s	+105%
	LP64	z3_smt_only*	✅	10s	21s	-52%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	5s	-20%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	74s	112s	-34%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	2s	+0%
`poly_power2round`	LP64	z3*	✅	2s	4s	-50%
`poly_reduce`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	11s	4s	+175%
	LP64	z3*	✅	3s	4s	-25%
`poly_sub`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_eta`	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	12s	-33%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	1s	5s	-80%
`poly_use_hint`	LP64	z3*	✅	4s	2s	+100%
`poly_use_hint_c`	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint_native`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	3s	+933%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	28s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	14s	-86%
	LP64	z3*	✅	7s	14s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	4s	-75%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	12s	-75%
	LP64	z3*	✅	7s	12s	-42%
`polyt1_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	3s	+67%
`polyt1_unpack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	4s	2s	+100%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	2s	4s	-50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	6s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	119s	149s	-20%
`polyveck_caddq`	LP64	z3*	✅	4s	3s	+33%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	7s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	2s	5s	-60%
`polyveck_ntt`	LP64	z3*	✅	2s	2s	+0%
`polyveck_reduce`	LP64	z3*	✅	1s	4s	-75%
`polyveck_unpack_eta`	LP64	z3*	✅	1s	2s	-50%
`polyveck_unpack_eta_chknorm`	LP64	z3*	✅	1s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	3s	11s	-73%
`polyvecl_ntt`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	1s	4s	-75%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	8s	-75%
	LP64	z3*	✅	8s	8s	+0%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	23s	3s	+667%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	5s	5s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	⚠️	22s	4s	+450%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	10s	3s	+233%
`rej_uniform`	LP64	bitwuzla	✅	2s	8s	-75%
	LP64	z3*	✅	5s	8s	-38%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	16s	-81%
	LP64	z3*	✅	8s	16s	-50%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	15s	5s	+200%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	8s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake128_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake256_absorb`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`shake256_release`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	3s	1s	+200%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	52s	2s	+2500%
	LP64	z3*	⚠️	33s	2s	+1550%
`sign_keypair`	LP64	z3*	✅	3s	5s	-40%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	11s	4s	+175%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	29s	5s	+480%
`sign_signature`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	4s	6s	-33%
`sign_signature_extmu`	LP64	z3*	✅	2s	4s	-50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	13s	4s	+225%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	4s	+25%
`sign_verify`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	6s	4s	+50%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	239s	49s	+388%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	5s	-60%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	2s	+0%
`use_hint`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%

oqs-bot · 2026-09-09T15:31:50Z

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2087s	1514s	+37.8%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	104s	50s	+108%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	23s	9s	+156%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	385s	58s	+564%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	92s	3s	+2967%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	3s	+667%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	20s	3s	+567%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	5s	+360%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	4s	+450%
`poly_caddq_c`	LP64	bitwuzla	⚠️	20s	2s	+900%
`poly_caddq_native`	LP64	bitwuzla	⚠️	121s	5s	+2320%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	130s	4s	+3150%
`poly_challenge`	LP64	bitwuzla	⚠️	26s	3s	+767%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	47s	4s	+1075%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	19s	+168%
`poly_ntt_native`	LP64	bitwuzla	⚠️	30s	5s	+500%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	35s	2s	+1650%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	2s	+1200%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	21s	4s	+425%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	53s	2s	+2550%
	LP64	z3*	⚠️	26s	2s	+1200%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	29s	5s	+480%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	243s	26s	+835%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	346s	114s	+204%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	31s	3s	+933%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	33s	2s	+1550%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	30s	2s	+1400%
`yvec_get_poly`	LP64	bitwuzla	⚠️	34s	3s	+1033%
`yvec_init`	LP64	bitwuzla	⚠️	39s	3s	+1200%

Full Results (375 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2087s	1514s	+37.8%
`caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	104s	50s	+108%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	29s	39s	-26%
	LP64	z3_smt_only	✅	20s	39s	-49%
`fqscale`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	3s	-67%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	23s	9s	+156%
	LP64	z3*	✅	2s	9s	-78%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	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	✅	4s	5s	-20%
	LP64	z3*	✅	4s	5s	-20%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	9s	-44%
	LP64	cvc5_arrays_exp	✅	7s	9s	-22%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
`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*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`keccak_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	3s	4s	-25%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	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	✅	13s	22s	-41%
	LP64	z3*	✅	11s	22s	-50%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	385s	58s	+564%
`mld_check_pct`	LP64	bitwuzla	✅	5s	14s	-64%
	LP64	z3*	✅	6s	14s	-57%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	4s	7s	-43%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	4s	2s	+100%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	5s	2s	+150%
	LP64	z3*	✅	3s	2s	+50%
`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	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_no_bv_extract	⚠️	92s	3s	+2967%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	70s	107s	-35%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	4s	8s	-50%
	LP64	z3*	✅	2s	8s	-75%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	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*	✅	16s	23s	-30%
`mld_ntt_layer`	LP64	bitwuzla*	✅	27s	42s	-36%
	LP64	z3_no_bv_extract	✅	2s	42s	-95%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	2s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	z3*	✅	4s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	-	new
	LP64	z3*	✅	4s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	5s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	3s	+667%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	20s	3s	+567%
	LP64	z3*	✅	4s	3s	+33%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	1s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_h`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	4s	+0%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	2s	7s	-71%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	5s	+360%
	LP64	z3*	✅	1s	5s	-80%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	4s	+450%
	LP64	z3*	✅	5s	4s	+25%
`poly_add`	LP64	z3*	✅	4s	7s	-43%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_c`	LP64	bitwuzla	⚠️	20s	2s	+900%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	bitwuzla	⚠️	121s	5s	+2320%
	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_native_aarch64`	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	130s	4s	+3150%
	LP64	z3*	✅	2s	4s	-50%
`poly_challenge`	LP64	bitwuzla	⚠️	26s	3s	+767%
	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	17s	-41%
	LP64	z3*	✅	7s	17s	-59%
`poly_chknorm_native`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	1s	4s	-75%
`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*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	4s	2s	+100%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_c`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_native`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	11s	-36%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	47s	4s	+1075%
	LP64	z3*	✅	5s	4s	+25%
`poly_ntt`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	19s	+168%
	LP64	z3_smt_only*	✅	10s	19s	-47%
`poly_ntt_native`	LP64	bitwuzla	⚠️	30s	5s	+500%
	LP64	z3*	✅	5s	5s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	55s	114s	-52%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	2s	+0%
`poly_power2round`	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	1s	3s	-67%
`poly_sub`	LP64	bitwuzla	✅	15s	3s	+400%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform`	LP64	z3*	✅	2s	6s	-67%
`poly_uniform_4x`	LP64	z3*	✅	8s	14s	-43%
`poly_uniform_eta`	LP64	z3*	✅	3s	5s	-40%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	11s	-27%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	35s	2s	+1650%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	37s	-	new
	LP64	z3*	✅	1s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	7s	14s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	8s	15s	-47%
`polyt1_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	4s	5s	-20%
`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*	✅	13s	15s	-13%
`polyveck_caddq`	LP64	z3*	✅	2s	3s	-33%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	4s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	3s	5s	-40%
`polyveck_ntt`	LP64	z3*	✅	2s	5s	-60%
`polyveck_reduce`	LP64	z3*	✅	1s	5s	-80%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta_chknorm`	LP64	z3*	✅	1s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	2s	10s	-80%
`polyvecl_ntt`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	169s	131s	+29%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	1s	2s	-50%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	11s	-73%
	LP64	z3*	✅	6s	11s	-45%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	2s	+1200%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`rej_eta`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	4s	3s	+33%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	19s	4s	+375%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	12s	6s	+100%
`rej_uniform`	LP64	bitwuzla	✅	3s	18s	-83%
	LP64	z3*	✅	14s	18s	-22%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	12s	15s	-20%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`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	⚠️	21s	4s	+425%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	4s	5s	-20%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	11s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`shake128_release`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	1s	+0%
`shake256`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	53s	2s	+2550%
	LP64	z3*	⚠️	26s	2s	+1200%
`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*	⚠️	29s	5s	+480%
`sign_signature`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	z3*	✅	4s	4s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	243s	26s	+835%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	2s	6s	-67%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	346s	114s	+204%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	31s	3s	+933%
	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	33s	2s	+1550%
	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	30s	2s	+1400%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	5s	+140%
	LP64	z3*	✅	2s	5s	-60%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	z3*	✅	4s	4s	+0%
`unpack_sk_t0hat`	LP64	z3*	✅	4s	3s	+33%
`use_hint`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	⚠️	34s	3s	+1033%
	LP64	z3*	✅	3s	3s	+0%
`yvec_init`	LP64	bitwuzla	⚠️	39s	3s	+1200%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-09-09T15:46:07Z

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	134s	13s	+931%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	200s	63s	+217%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	84s	2s	+4100%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	2s	+900%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	5s	+360%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	20s	3s	+567%
`poly_caddq_c`	LP64	bitwuzla	⚠️	20s	2s	+900%
`poly_caddq_native`	LP64	bitwuzla	⚠️	109s	2s	+5350%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	123s	3s	+4000%
`poly_challenge`	LP64	bitwuzla	⚠️	23s	6s	+283%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	42s	2s	+2000%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	19s	+168%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	4s	+550%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	30s	3s	+900%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	25s	4s	+525%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	20s	4s	+400%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1293s	2s	+64550%
	LP64	z3*	⚠️	21s	2s	+950%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	38s	6s	+533%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	181s	55s	+229%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	333s	3s	+11000%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	427s	177s	+141%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	36s	6s	+500%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	28s	2s	+1300%
`yvec_get_poly`	LP64	bitwuzla	⚠️	32s	3s	+967%

Full Results (375 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1975s	1784s	+10.7%
`caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	134s	13s	+931%
`decompose`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`fqmul`	LP64	bitwuzla*	✅	23s	40s	-43%
	LP64	z3_smt_only	✅	21s	40s	-48%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	5s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	5s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	1s	3s	-67%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	8s	-38%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`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	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccak_init`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	4s	-75%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	1s	5s	-80%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	23s	-48%
	LP64	z3*	✅	13s	23s	-43%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_no_bv_extract	✅	1s	3s	-67%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	200s	63s	+217%
`mld_check_pct`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	4s	14s	-71%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	7s	-71%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	1s	2s	-50%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	5s	3s	+67%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	⚠️	84s	2s	+4100%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	65s	109s	-40%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`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	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	24s	-54%
`mld_ntt_layer`	LP64	bitwuzla*	✅	26s	41s	-37%
	LP64	z3_no_bv_extract	✅	4s	41s	-90%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	4s	4s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	5s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	z3*	✅	3s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	-	new
	LP64	z3*	✅	4s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	2s	+900%
	LP64	z3*	✅	5s	2s	+150%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	2s	+850%
	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`pack_sig_h`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3_no_bv_extract*	✅	1s	5s	-80%
`pack_sig_z`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	1s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	8s	-38%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	5s	+360%
	LP64	z3*	✅	5s	5s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	20s	3s	+567%
	LP64	z3*	✅	1s	3s	-67%
`poly_add`	LP64	z3*	✅	3s	9s	-67%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	bitwuzla	⚠️	20s	2s	+900%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	bitwuzla	⚠️	109s	2s	+5350%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	123s	3s	+4000%
	LP64	z3*	✅	3s	3s	+0%
`poly_challenge`	LP64	bitwuzla	⚠️	23s	6s	+283%
	LP64	z3*	✅	2s	6s	-67%
`poly_chknorm`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	15s	-33%
	LP64	z3*	✅	7s	15s	-53%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	4s	3s	+33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_c`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	9s	11s	-18%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	42s	2s	+2000%
	LP64	z3*	✅	3s	2s	+50%
`poly_ntt`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	51s	19s	+168%
	LP64	z3_smt_only*	✅	9s	19s	-53%
`poly_ntt_native`	LP64	bitwuzla	⚠️	26s	4s	+550%
	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	50s	125s	-60%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	z3*	✅	2s	4s	-50%
`poly_reduce`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	1s	3s	-67%
`poly_shiftl`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	1s	3s	-67%
`poly_sub`	LP64	bitwuzla	✅	15s	3s	+400%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_4x`	LP64	z3*	✅	6s	13s	-54%
`poly_uniform_eta`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta_4x`	LP64	z3*	✅	6s	14s	-57%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_c`	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint_native`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	30s	3s	+900%
	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	8s	-88%
	LP64	z3*	✅	4s	8s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	16s	-75%
	LP64	z3*	✅	7s	16s	-56%
`polyt1_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	5s	-40%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	81s	110s	-26%
`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*	✅	19s	18s	+6%
`polyveck_caddq`	LP64	z3*	✅	5s	6s	-17%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	8s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	8s	-50%
`polyveck_ntt`	LP64	z3*	✅	5s	7s	-29%
`polyveck_reduce`	LP64	z3*	✅	1s	4s	-75%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	6s	-67%
`polyveck_unpack_eta_chknorm`	LP64	z3*	✅	2s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	4s	7s	-43%
`polyvecl_ntt`	LP64	z3*	✅	4s	4s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	122s	210s	-42%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	z3*	✅	1s	3s	-67%
`polyw1_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	13s	-85%
	LP64	z3*	✅	4s	13s	-69%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	25s	4s	+525%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`reduce32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	9s	5s	+80%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	10s	3s	+233%
`rej_uniform`	LP64	bitwuzla	✅	2s	18s	-89%
	LP64	z3*	✅	12s	18s	-33%
`rej_uniform_c`	LP64	bitwuzla	✅	1s	14s	-93%
	LP64	z3*	✅	8s	14s	-43%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	2s	4s	-50%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	⚠️	20s	4s	+400%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`shake256`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	3s	1s	+200%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_release`	LP64	bitwuzla	✅	1s	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	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1293s	2s	+64550%
	LP64	z3*	⚠️	21s	2s	+950%
`sign_keypair`	LP64	z3*	✅	4s	3s	+33%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	19s	5s	+280%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	38s	6s	+533%
`sign_signature`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	3s	6s	-50%
`sign_signature_extmu`	LP64	z3*	✅	2s	2s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	181s	55s	+229%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	333s	3s	+11000%
	LP64	z3*	✅	6s	3s	+100%
`sign_verify`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	427s	177s	+141%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	5s	-80%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	36s	6s	+500%
	LP64	z3*	✅	2s	6s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	28s	2s	+1300%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	5s	+100%
	LP64	z3*	✅	2s	5s	-60%
`unpack_sk`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	4s	5s	-20%
`use_hint`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	⚠️	32s	3s	+967%
	LP64	z3*	✅	3s	3s	+0%
`yvec_init`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	1s	3s	-67%

oqs-bot · 2026-09-09T15:49:19Z

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	3373s	2151s	+56.8%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	245s	19s	+1189%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	23s	3s	+667%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	312s	55s	+467%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	87s	3s	+2800%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	6s	+233%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	24s	5s	+380%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
`poly_caddq_native`	LP64	bitwuzla	⚠️	113s	4s	+2725%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	117s	2s	+5750%
`poly_challenge`	LP64	bitwuzla	⚠️	34s	5s	+580%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	5s	+820%
`poly_ntt_c`	LP64	bitwuzla	⚠️	48s	21s	+129%
`poly_ntt_native`	LP64	bitwuzla	⚠️	29s	3s	+867%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	2s	+1450%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	4s	+575%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	25s	3s	+733%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	21s	6s	+250%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	34s	6s	+467%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	409s	42s	+874%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1632s	6s	+27100%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	1233s	97s	+1171%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	34s	3s	+1033%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	34s	4s	+750%
`yvec_get_poly`	LP64	bitwuzla	⚠️	37s	4s	+825%

Full Results (375 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	3373s	2151s	+56.8%
`caddq`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	245s	19s	+1189%
`decompose`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`fqmul`	LP64	bitwuzla*	✅	26s	43s	-40%
	LP64	z3_smt_only	✅	20s	43s	-53%
`fqscale`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	23s	3s	+667%
	LP64	z3*	✅	1s	3s	-67%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	5s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	2s	3s	-33%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	9s	-44%
	LP64	cvc5_arrays_exp	✅	9s	9s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_no_bv_extract	✅	4s	1s	+300%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	2s	4s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccak_init`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	23s	-48%
	LP64	z3*	✅	14s	23s	-39%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	312s	55s	+467%
`mld_check_pct`	LP64	bitwuzla	✅	5s	16s	-69%
	LP64	z3*	✅	5s	16s	-69%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	3s	8s	-62%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	1s	3s	-67%
	ILP32	z3	✅	2s	3s	-33%
	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	⚠️	87s	3s	+2800%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	6s	3s	+100%
`mld_invntt_layer`	LP64	bitwuzla*	✅	69s	115s	-40%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	4s	7s	-43%
	LP64	z3*	✅	4s	7s	-43%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	24s	-46%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	45s	-44%
	LP64	z3_no_bv_extract	✅	2s	45s	-96%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	6s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	z3*	✅	5s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	6s	+233%
	LP64	z3*	✅	4s	6s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	4s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	2s	+850%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3_no_bv_extract*	✅	6s	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*	✅	5s	6s	-17%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	24s	5s	+380%
	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
	LP64	z3*	✅	3s	2s	+50%
`poly_add`	LP64	z3*	✅	3s	6s	-50%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native`	LP64	bitwuzla	⚠️	113s	4s	+2725%
	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	117s	2s	+5750%
	LP64	z3*	✅	3s	2s	+50%
`poly_challenge`	LP64	bitwuzla	⚠️	34s	5s	+580%
	LP64	z3*	✅	2s	5s	-60%
`poly_chknorm`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	15s	-33%
	LP64	z3*	✅	7s	15s	-53%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	4s	+75%
	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	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_decompose_c`	LP64	z3*	✅	4s	5s	-20%
`poly_decompose_native`	LP64	z3*	✅	5s	2s	+150%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	6s	1s	+500%
	LP64	z3*	✅	2s	1s	+100%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	12s	-50%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	5s	+820%
	LP64	z3*	✅	4s	5s	-20%
`poly_ntt`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt_c`	LP64	bitwuzla	⚠️	48s	21s	+129%
	LP64	z3_smt_only*	✅	10s	21s	-52%
`poly_ntt_native`	LP64	bitwuzla	⚠️	29s	3s	+867%
	LP64	z3*	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	4s	+125%
	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	50s	144s	-65%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	5s	-60%
`poly_power2round`	LP64	z3*	✅	4s	3s	+33%
`poly_reduce`	LP64	bitwuzla	✅	8s	2s	+300%
	LP64	z3*	✅	2s	2s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	10s	4s	+150%
	LP64	z3*	✅	1s	4s	-75%
`poly_sub`	LP64	bitwuzla	✅	15s	3s	+400%
	LP64	z3*	✅	4s	3s	+33%
`poly_uniform`	LP64	z3*	✅	5s	4s	+25%
`poly_uniform_4x`	LP64	z3*	✅	7s	13s	-46%
`poly_uniform_eta`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta_4x`	LP64	z3*	✅	11s	11s	+0%
`poly_uniform_gamma1`	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint`	LP64	z3*	✅	4s	1s	+300%
`poly_use_hint_c`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	2s	+1450%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	28s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	17s	-82%
	LP64	z3*	✅	4s	17s	-76%
`polyt0_pack`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	8s	14s	-43%
`polyt1_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	4s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	115s	324s	-65%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	24s	38s	-37%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	16s	18s	-11%
`polyveck_caddq`	LP64	z3*	✅	5s	8s	-38%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	6s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	9s	-44%
`polyveck_ntt`	LP64	z3*	✅	5s	11s	-55%
`polyveck_reduce`	LP64	z3*	✅	3s	3s	+0%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	4s	-50%
`polyveck_unpack_eta_chknorm`	LP64	z3*	✅	2s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_ntt`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	3s	5s	-40%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	154s	353s	-56%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_eta`	LP64	z3*	✅	3s	5s	-40%
`polyvecl_unpack_z`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	4s	+575%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	3s	+467%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`reduce32`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	1s	4s	-75%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	18s	5s	+260%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	11s	6s	+83%
`rej_uniform`	LP64	bitwuzla	✅	2s	15s	-87%
	LP64	z3*	✅	12s	15s	-20%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	19s	-89%
	LP64	z3*	✅	11s	19s	-42%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	8s	-75%
	LP64	z3_smt_only	✅	19s	8s	+138%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	z3_smt_only	✅	4s	2s	+100%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	10s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake128_release`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	3s	5s	-40%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`shake256`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake256_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	5s	3s	+67%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	25s	3s	+733%
	LP64	z3*	✅	17s	3s	+467%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	21s	6s	+250%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	34s	6s	+467%
`sign_signature`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`sign_signature_extmu`	LP64	z3*	✅	7s	4s	+75%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	409s	42s	+874%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	5s	-60%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1632s	6s	+27100%
	LP64	z3*	✅	5s	6s	-17%
`sign_verify`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	5s	5s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	1233s	97s	+1171%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	34s	3s	+1033%
	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	4s	3s	+33%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	34s	4s	+750%
	LP64	z3*	✅	1s	4s	-75%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	1s	+1100%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk`	LP64	z3*	✅	2s	5s	-60%
`unpack_sk_s1hat`	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_s2hat`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	z3*	✅	4s	7s	-43%
`use_hint`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	bitwuzla	⚠️	37s	4s	+825%
	LP64	z3*	✅	2s	4s	-50%
`yvec_init`	LP64	bitwuzla	✅	15s	4s	+275%
	LP64	z3*	✅	4s	4s	+0%

oqs-bot · 2026-09-09T15:50:09Z

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*	⚠️	36s	7s	+414%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	22s	2s	+1000%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	183s	31s	+490%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	80s	4s	+1900%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	3s	+567%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	21s	3s	+600%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
`poly_caddq_native`	LP64	bitwuzla	⚠️	106s	4s	+2550%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	101s	1s	+10000%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	5s	+340%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	43s	5s	+760%
`poly_ntt_c`	LP64	bitwuzla	⚠️	49s	22s	+123%
`poly_ntt_native`	LP64	bitwuzla	⚠️	25s	2s	+1150%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	26s	4s	+550%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1299s	1s	+129800%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	34s	5s	+580%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	334s	7s	+4671%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	195s	71s	+175%

Full Results (375 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1350s	1482s	-8.9%
`caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	36s	7s	+414%
`decompose`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`fqmul`	LP64	bitwuzla*	✅	25s	40s	-38%
	LP64	z3_smt_only	✅	20s	40s	-50%
`fqscale`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	22s	2s	+1000%
	LP64	z3*	✅	4s	2s	+100%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	4s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	15s	4s	+275%
	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	10s	-60%
	LP64	cvc5_arrays_exp	✅	8s	10s	-20%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	4s	2s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`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	✅	1s	2s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
`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	✅	1s	4s	-75%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	22s	-41%
	LP64	z3*	✅	12s	22s	-45%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	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	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	183s	31s	+490%
`mld_check_pct`	LP64	bitwuzla	✅	3s	12s	-75%
	LP64	z3*	✅	3s	12s	-75%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	4s	5s	-20%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	6s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	6s	-67%
	ILP32	z3	✅	2s	6s	-67%
	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	cvc5_arrays_exp	✅	1s	6s	-83%
	LP64	z3*	✅	2s	6s	-67%
`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	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	2s	4s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_no_bv_extract	⚠️	80s	4s	+1900%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	63s	108s	-42%
`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*	✅	3s	7s	-57%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	25s	-48%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	43s	-42%
	LP64	z3_no_bv_extract	✅	3s	43s	-93%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	5s	4s	+25%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	4s	-	new
`mld_sample_pack_s1_s2_serial`	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	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	3s	+567%
	LP64	z3*	✅	3s	3s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	4s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	5s	+260%
	LP64	z3*	✅	4s	5s	-20%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`pack_sig_h`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	5s	1s	+400%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	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	⚠️	21s	3s	+600%
	LP64	z3*	✅	3s	3s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
	LP64	z3*	✅	2s	2s	+0%
`poly_add`	LP64	z3*	✅	2s	7s	-71%
`poly_caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	5s	+280%
	LP64	z3*	✅	4s	5s	-20%
`poly_caddq_native`	LP64	bitwuzla	⚠️	106s	4s	+2550%
	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	101s	1s	+10000%
	LP64	z3*	✅	1s	1s	+0%
`poly_challenge`	LP64	bitwuzla	⚠️	22s	5s	+340%
	LP64	z3*	✅	4s	5s	-20%
`poly_chknorm`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	13s	-46%
	LP64	z3*	✅	8s	13s	-38%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	4s	2s	+100%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_c`	LP64	z3*	✅	4s	8s	-50%
`poly_decompose_native`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	5s	-40%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	10s	10s	+0%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	43s	5s	+760%
	LP64	z3*	✅	3s	5s	-40%
`poly_ntt`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	49s	22s	+123%
	LP64	z3_smt_only*	✅	9s	22s	-59%
`poly_ntt_native`	LP64	bitwuzla	⚠️	25s	2s	+1150%
	LP64	z3*	✅	4s	2s	+100%
`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*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	2s	+350%
	LP64	z3*	✅	1s	2s	-50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	76s	116s	-34%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	4s	-50%
`poly_power2round`	LP64	z3*	✅	2s	7s	-71%
`poly_reduce`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	1s	4s	-75%
`poly_shiftl`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	bitwuzla	✅	14s	4s	+250%
	LP64	z3*	✅	5s	4s	+25%
`poly_uniform`	LP64	z3*	✅	4s	2s	+100%
`poly_uniform_4x`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_eta`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	13s	-38%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	z3*	✅	3s	7s	-57%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	26s	4s	+550%
	LP64	z3*	✅	4s	4s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	27s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`polyt0_pack`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	3s	5s	-40%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	13s	-69%
	LP64	z3*	✅	8s	13s	-38%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	5s	8s	-38%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	118s	201s	-41%
`polyveck_caddq`	LP64	z3*	✅	3s	7s	-57%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	8s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	3s	7s	-57%
`polyveck_ntt`	LP64	z3*	✅	1s	4s	-75%
`polyveck_reduce`	LP64	z3*	✅	4s	6s	-33%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta_chknorm`	LP64	z3*	✅	2s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	3s	43s	-93%
`polyvecl_ntt`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	1s	4s	-75%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	1s	+100%
`polyvecl_unpack_eta`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_unpack_z`	LP64	z3*	✅	1s	1s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	4s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack_c`	LP64	bitwuzla	✅	4s	9s	-56%
	LP64	z3*	✅	4s	9s	-56%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	1s	3s	-67%
`power2round`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	15s	4s	+275%
`rej_eta_native`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	9s	3s	+200%
`rej_uniform`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	3s	7s	-57%
`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	✅	3s	5s	-40%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	18s	4s	+350%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	10s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	2s	6s	-67%
`shake128_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`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	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`shake256_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	2s	4s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1299s	1s	+129800%
	LP64	z3*	✅	17s	1s	+1600%
`sign_keypair`	LP64	z3*	✅	6s	4s	+50%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	18s	3s	+500%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	34s	5s	+580%
`sign_signature`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`sign_signature_extmu`	LP64	z3*	✅	4s	4s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	14s	6s	+133%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	334s	7s	+4671%
	LP64	z3*	✅	3s	7s	-57%
`sign_verify`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	1s	6s	-83%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	195s	71s	+175%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	5s	5s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	1s	6s	-83%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	1s	+200%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	1s	1s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	2s	+500%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	1s	+0%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	4s	-50%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	5s	-80%

oqs-bot · 2026-09-09T15:54:55Z

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*	⚠️	28s	12s	+133%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	20s	4s	+400%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	187s	34s	+450%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	78s	1s	+7700%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	4s	+475%
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	5s	+340%
`poly_caddq_native`	LP64	bitwuzla	⚠️	87s	3s	+2800%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	114s	3s	+3700%
`poly_challenge`	LP64	bitwuzla	⚠️	33s	4s	+725%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	43s	2s	+2050%
`poly_ntt_c`	LP64	bitwuzla	⚠️	45s	19s	+137%
`poly_ntt_native`	LP64	bitwuzla	⚠️	25s	4s	+525%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	28s	3s	+833%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	22s	1s	+2100%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	26s	4s	+550%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	26s	6s	+333%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	32s	6s	+433%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1371s	3s	+45600%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	237s	47s	+404%

Full Results (375 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1342s	1436s	-6.5%
`caddq`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	28s	12s	+133%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	24s	39s	-38%
	LP64	z3_smt_only	✅	19s	39s	-51%
`fqscale`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	20s	4s	+400%
	LP64	z3*	✅	3s	4s	-25%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_x86_64`	LP64	bitwuzla	✅	16s	4s	+300%
	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	4s	4s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	8s	-25%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
`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	2s	-50%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`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*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccak_init`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	3s	5s	-40%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	25s	-48%
	LP64	z3*	✅	13s	25s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	187s	34s	+450%
`mld_check_pct`	LP64	bitwuzla	✅	5s	15s	-67%
	LP64	z3*	✅	4s	15s	-73%
`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	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`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	✅	1s	5s	-80%
	LP64	z3*	✅	2s	5s	-60%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	⚠️	78s	1s	+7700%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	61s	111s	-45%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	8s	-62%
	LP64	z3*	✅	5s	8s	-38%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	23s	-48%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	44s	-48%
	LP64	z3_no_bv_extract	✅	2s	44s	-95%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_sample_pack_s1_s2`	LP64	z3*	✅	7s	-	new
`mld_sample_pack_s1_s2_serial`	LP64	z3*	✅	3s	-	new
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	-	new
	LP64	z3*	✅	1s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	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*	✅	1s	3s	-67%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	4s	+375%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	2s	+800%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	2s	5s	-60%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	8s	-38%
`pointwise_native_aarch64`	LP64	bitwuzla	⚠️	23s	4s	+475%
	LP64	z3*	✅	2s	4s	-50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_x86_64`	LP64	bitwuzla	⚠️	22s	5s	+340%
	LP64	z3*	✅	3s	5s	-40%
`poly_add`	LP64	z3*	✅	3s	8s	-62%
`poly_caddq`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	5s	-80%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	87s	3s	+2800%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	114s	3s	+3700%
	LP64	z3*	✅	2s	3s	-33%
`poly_challenge`	LP64	bitwuzla	⚠️	33s	4s	+725%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	13s	-46%
	LP64	z3*	✅	7s	13s	-46%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	1s	+500%
	LP64	z3*	✅	1s	1s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	1s	5s	-80%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	6s	6s	+0%
`poly_decompose_native`	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	5s	9s	-44%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	43s	2s	+2050%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	45s	19s	+137%
	LP64	z3_smt_only*	✅	11s	19s	-42%
`poly_ntt_native`	LP64	bitwuzla	⚠️	25s	4s	+525%
	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	70s	125s	-44%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	3s	3s	+0%
`poly_power2round`	LP64	z3*	✅	3s	7s	-57%
`poly_reduce`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	1s	4s	-75%
`poly_shiftl`	LP64	bitwuzla	✅	11s	4s	+175%
	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	bitwuzla	✅	13s	5s	+160%
	LP64	z3*	✅	1s	5s	-80%
`poly_uniform`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_eta`	LP64	z3*	✅	1s	5s	-80%
`poly_uniform_eta_4x`	LP64	z3*	✅	7s	12s	-42%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_c`	LP64	z3*	✅	1s	4s	-75%
`poly_use_hint_native`	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	28s	3s	+833%
	LP64	z3*	✅	5s	3s	+67%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	27s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	13s	-92%
	LP64	z3*	✅	6s	13s	-54%
`polyt0_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	8s	14s	-43%
`polyt1_pack`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	5s	-40%
`polyt1_unpack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	1s	3s	-67%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	6s	13s	-54%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	86s	196s	-56%
`polyveck_caddq`	LP64	z3*	✅	4s	8s	-50%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	12s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	6s	4s	+50%
`polyveck_ntt`	LP64	z3*	✅	1s	3s	-67%
`polyveck_reduce`	LP64	z3*	✅	4s	6s	-33%
`polyveck_unpack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyveck_unpack_eta_chknorm`	LP64	z3*	✅	2s	-	new
`polyvecl_chknorm`	LP64	z3*	✅	2s	38s	-95%
`polyvecl_ntt`	LP64	z3*	✅	3s	8s	-62%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	3s	2s	+50%
`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	z3*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	6s	7s	-14%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	22s	1s	+2100%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	3s	2s	+50%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	17s	4s	+325%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	9s	4s	+125%
`rej_uniform`	LP64	bitwuzla	✅	1s	7s	-86%
	LP64	z3*	✅	5s	7s	-29%
`rej_uniform_c`	LP64	bitwuzla	✅	1s	18s	-94%
	LP64	z3*	✅	8s	18s	-56%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	17s	5s	+240%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	7s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	3s	4s	-25%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
`shake256`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_absorb`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`shake256_release`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	5s	-60%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	2s	5s	-60%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	2s	4s	-50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	26s	4s	+550%
	LP64	z3*	✅	16s	4s	+300%
`sign_keypair`	LP64	z3*	✅	3s	4s	-25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	26s	6s	+333%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	32s	6s	+433%
`sign_signature`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	14s	3s	+367%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1371s	3s	+45600%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	237s	47s	+404%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	2s	7s	-71%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	11s	2s	+450%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_s1hat`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s2hat`	LP64	z3*	✅	3s	3s	+0%
`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	✅	8s	2s	+300%
	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%

hanno-becker

@mkannwischer Thanks a lot. It's great to make progress towards the desired proof redundancy.

Can you rebase and get it ready for review?

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>

hanno-becker

Thanks a lot @mkannwischer, it's great to make progress towards the proof-redundancy goal!

hanno-becker reviewed Oct 17, 2026

View reviewed changes

mkannwischer force-pushed the mjk/cbmc-lp64-two-solvers branch from 70b5ce9 to 191da3c Compare October 24, 2026 13:04

mkannwischer changed the title ~~CBMC: Use a second solver for 154/212 proofs~~ CBMC: Use a second solver for 150/215 proofs Oct 24, 2026

mkannwischer force-pushed the mjk/cbmc-lp64-two-solvers branch from 191da3c to 15fe7d6 Compare October 24, 2026 14:11

mkannwischer changed the title ~~CBMC: Use a second solver for 150/215 proofs~~ CBMC: Use a second solver for 149/215 proofs Oct 24, 2026

mkannwischer marked this pull request as ready for review October 24, 2026 15:01

mkannwischer requested a review from a team as a code owner October 24, 2026 15:01

mkannwischer mentioned this pull request Oct 24, 2026

CBMC: Add more cvc5 proofs #1491

Merged

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 8bd08a0 Oct 25, 2026
402 checks passed

hanno-becker deleted the mjk/cbmc-lp64-two-solvers branch October 25, 2026 07:14

Navigation Menu

Repository navigation

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

CBMC: Use a second solver for 149/215 proofs#1423
hanno-becker merged 1 commit into
mainfrom
mjk/cbmc-lp64-two-solvers

mkannwischer commented Sep 9, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 9, 2026 •

edited

Loading

Uh oh!

hanno-becker left a comment

Uh oh!

hanno-becker left a comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mkannwischer commented Sep 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Sep 9, 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 Sep 9, 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 Sep 9, 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 Sep 9, 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 Sep 9, 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 Sep 9, 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!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mkannwischer commented Sep 9, 2026 •

edited

Loading

oqs-bot commented Sep 9, 2026 •

edited

Loading

oqs-bot commented Sep 9, 2026 •

edited

Loading

oqs-bot commented Sep 9, 2026 •

edited

Loading

oqs-bot commented Sep 9, 2026 •

edited

Loading

oqs-bot commented Sep 9, 2026 •

edited

Loading

oqs-bot commented Sep 9, 2026 •

edited

Loading