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

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

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.

153 of 212 proofs gain a second solver: 99 bitwuzla, 28 cvc5_arrays_exp, and 26 Z3 profiles alongside a bitwuzla or cvc5 default. The other 59 do not, mostly because bitwuzla timed out or cvc5 returned unknown under a local 300s per-proof cap.

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. 153 of 212 proofs gain a second solver: 99 bitwuzla, 28 cvc5_arrays_exp, and 26 Z3 profiles alongside a bitwuzla or cvc5 default. The other 59 do not, mostly because bitwuzla timed out or cvc5 returned unknown under a local 300s per-proof cap. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

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*	⚠️	33s	12s	+175%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	24s	3s	+700%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	25s	2s	+1150%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	147s	19s	+674%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	81s	1s	+8000%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	4s	+400%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	25s	3s	+733%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	40s	5s	+700%
`pack_sk_s1`	LP64	bitwuzla	⚠️	39s	3s	+1200%
`poly_caddq_native`	LP64	bitwuzla	⚠️	57s	3s	+1800%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	39s	4s	+875%
`poly_challenge`	LP64	bitwuzla	⚠️	23s	6s	+283%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	39s	3s	+1200%
`poly_ntt_c`	LP64	bitwuzla	⚠️	44s	21s	+110%
`poly_ntt_native`	LP64	bitwuzla	⚠️	34s	3s	+1033%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	3s	+933%
`polyveck_reduce`	LP64	cvc5_arrays_exp	⚠️	?	4s	inconclusive
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
`rej_eta_c`	LP64	z3	⚠️	20s	4s	+400%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	52s	2s	+2500%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	45s	5s	+800%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	169s	49s	+245%

Full Results (370 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1311s	1364s	-3.9%
`caddq`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	4s	6s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	33s	12s	+175%
`decompose`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`fqmul`	LP64	bitwuzla*	✅	26s	39s	-33%
	LP64	z3_smt_only	✅	22s	39s	-44%
`fqscale`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	24s	3s	+700%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	25s	2s	+1150%
	LP64	z3*	✅	4s	2s	+100%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	8s	-25%
	LP64	cvc5_arrays_exp	✅	7s	8s	-12%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	6s	-83%
	LP64	z3_smt_only	✅	1s	6s	-83%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	3s	4s	-25%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	22s	-41%
	LP64	z3*	✅	11s	22s	-50%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3_no_bv_extract	✅	2s	5s	-60%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	147s	19s	+674%
`mld_check_pct`	LP64	bitwuzla	✅	4s	15s	-73%
	LP64	z3*	✅	6s	15s	-60%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	4s	6s	-33%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	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	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	⚠️	81s	1s	+8000%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	67s	105s	-36%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	7s	-29%
	LP64	z3*	✅	6s	7s	-14%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%
`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*	✅	26s	41s	-37%
	LP64	z3_no_bv_extract	✅	3s	41s	-93%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_sample_s1_s2`	LP64	z3*	✅	4s	1s	+300%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	4s	-25%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	20s	4s	+400%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	25s	3s	+733%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	z3*	✅	3s	4s	-25%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	5s	-80%
	LP64	z3*	✅	3s	5s	-40%
`pack_sig_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	40s	5s	+700%
	LP64	z3*	✅	2s	5s	-60%
`pack_sk_s1`	LP64	bitwuzla	⚠️	39s	3s	+1200%
	LP64	z3*	✅	3s	3s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	4s	+25%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	12s	2s	+500%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	1s	4s	-75%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	57s	3s	+1800%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	39s	4s	+875%
	LP64	z3*	✅	1s	4s	-75%
`poly_challenge`	LP64	bitwuzla	⚠️	23s	6s	+283%
	LP64	z3*	✅	2s	6s	-67%
`poly_chknorm`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	11s	-36%
	LP64	z3*	✅	6s	11s	-45%
`poly_chknorm_native`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	5s	2s	+150%
`poly_decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_c`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	11s	-45%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	39s	3s	+1200%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	44s	21s	+110%
	LP64	z3_smt_only*	✅	10s	21s	-52%
`poly_ntt_native`	LP64	bitwuzla	⚠️	34s	3s	+1033%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	5s	-80%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	4s	3s	+33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	78s	112s	-30%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	3s	2s	+50%
`poly_power2round`	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	11s	4s	+175%
	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_eta`	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_eta_4x`	LP64	z3*	✅	10s	12s	-17%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint`	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_c`	LP64	z3*	✅	5s	5s	+0%
`poly_use_hint_native`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	3s	+933%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	33s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	1s	3s	-67%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	14s	-86%
	LP64	z3*	✅	6s	14s	-57%
`polyt0_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	12s	-75%
	LP64	z3*	✅	9s	12s	-25%
`polyt1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	4s	4s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	5s	6s	-17%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	108s	149s	-28%
`polyveck_caddq`	LP64	z3*	✅	3s	3s	+0%
`polyveck_chknorm`	LP64	z3*	✅	4s	67s	-94%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	3s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	2s	5s	-60%
`polyveck_ntt`	LP64	z3*	✅	3s	2s	+50%
`polyveck_pack_eta`	LP64	z3*	✅	5s	4s	+25%
`polyveck_reduce`	LP64	cvc5_arrays_exp	⚠️	?	4s	inconclusive
	LP64	z3*	✅	2s	4s	-50%
`polyveck_unpack_eta`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_chknorm`	LP64	z3*	✅	4s	11s	-64%
`polyvecl_ntt`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pack_eta`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	3s	4s	-25%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	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	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	8s	-75%
	LP64	z3*	✅	5s	8s	-38%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	26s	3s	+767%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	2s	5s	-60%
`rej_eta_c`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	⚠️	20s	4s	+400%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	11s	3s	+267%
`rej_uniform`	LP64	bitwuzla	✅	2s	8s	-75%
	LP64	z3*	✅	4s	8s	-50%
`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	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	z3_smt_only	✅	18s	5s	+260%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	6s	-	new
	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`shake256`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake256_absorb`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`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*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3	✅	3s	1s	+200%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	52s	2s	+2500%
	LP64	z3*	✅	13s	2s	+550%
`sign_keypair`	LP64	z3*	✅	6s	5s	+20%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	19s	4s	+375%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	45s	5s	+800%
`sign_signature`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	3s	6s	-50%
`sign_signature_extmu`	LP64	z3*	✅	4s	4s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	16s	4s	+300%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	5s	4s	+25%
`sign_verify`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	4s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	5s	-60%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	169s	49s	+245%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	5s	5s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	6s	5s	+20%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	1s	5s	-80%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`unpack_pk_t1`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	2s	+0%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`yvec_get_poly`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`yvec_init`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%

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

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	1943s	1514s	+28.3%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	124s	50s	+148%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	26s	9s	+189%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	27s	4s	+575%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	175s	58s	+202%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	91s	3s	+2933%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	27s	3s	+800%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	46s	3s	+1433%
`pack_sk_s1`	LP64	bitwuzla	⚠️	43s	2s	+2050%
`poly_caddq_c`	LP64	bitwuzla	⚠️	22s	2s	+1000%
`poly_caddq_native`	LP64	bitwuzla	⚠️	66s	5s	+1220%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	44s	4s	+1000%
`poly_challenge`	LP64	bitwuzla	⚠️	30s	3s	+900%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	4s	+1050%
`poly_ntt_c`	LP64	bitwuzla	⚠️	54s	19s	+184%
`poly_ntt_native`	LP64	bitwuzla	⚠️	41s	5s	+720%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	37s	2s	+1750%
`polyveck_chknorm`	LP64	z3*	⚠️	75s	5s	+1400%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	⚠️	201s	131s	+53%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	2s	+1250%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	60s	2s	+2900%
	LP64	z3*	⚠️	27s	2s	+1250%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	45s	5s	+800%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	134s	26s	+415%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	334s	114s	+193%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	30s	2s	+1400%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	34s	2s	+1600%
`yvec_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
`yvec_init`	LP64	bitwuzla	⚠️	42s	3s	+1300%

Full Results (370 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	1943s	1514s	+28.3%
`caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	124s	50s	+148%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`fqmul`	LP64	bitwuzla*	✅	25s	39s	-36%
	LP64	z3_smt_only	✅	21s	39s	-46%
`fqscale`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	1s	3s	-67%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	26s	9s	+189%
	LP64	z3*	✅	4s	9s	-56%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	27s	4s	+575%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	9s	-22%
	LP64	cvc5_arrays_exp	✅	9s	9s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	4s	2s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`keccak_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	4s	4s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	22s	-41%
	LP64	z3*	✅	15s	22s	-32%
`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	✅	1s	3s	-67%
`make_hint`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	175s	58s	+202%
`mld_check_pct`	LP64	bitwuzla	✅	4s	14s	-71%
	LP64	z3*	✅	4s	14s	-71%
`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	✅	3s	2s	+50%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	⚠️	91s	3s	+2933%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`mld_invntt_layer`	LP64	bitwuzla*	✅	77s	107s	-28%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	8s	-62%
	LP64	z3*	✅	6s	8s	-25%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	17s	23s	-26%
`mld_ntt_layer`	LP64	bitwuzla*	✅	29s	42s	-31%
	LP64	z3_no_bv_extract	✅	3s	42s	-93%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_s1_s2`	LP64	z3*	✅	3s	4s	-25%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	3s	+0%
`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	✅	2s	-	new
	LP64	z3*	✅	4s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`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*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	3s	3s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	27s	3s	+800%
	LP64	z3*	✅	4s	3s	+33%
`nttunpack_native_x86_64`	LP64	z3*	✅	3s	1s	+200%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	46s	3s	+1433%
	LP64	z3*	✅	1s	3s	-67%
`pack_sk_s1`	LP64	bitwuzla	⚠️	43s	2s	+2050%
	LP64	z3*	✅	1s	2s	-50%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	7s	-57%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	9s	5s	+80%
	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	10s	4s	+150%
	LP64	z3*	✅	4s	4s	+0%
`poly_add`	LP64	z3*	✅	6s	7s	-14%
`poly_caddq`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	bitwuzla	⚠️	22s	2s	+1000%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native`	LP64	bitwuzla	⚠️	66s	5s	+1220%
	LP64	z3*	✅	4s	5s	-20%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	44s	4s	+1000%
	LP64	z3*	✅	2s	4s	-50%
`poly_challenge`	LP64	bitwuzla	⚠️	30s	3s	+900%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_c`	LP64	bitwuzla	✅	11s	17s	-35%
	LP64	z3*	✅	8s	17s	-53%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_c`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_native`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	3s	4s	-25%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	11s	-45%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	4s	+1050%
	LP64	z3*	✅	3s	4s	-25%
`poly_ntt`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	54s	19s	+184%
	LP64	z3_smt_only*	✅	10s	19s	-47%
`poly_ntt_native`	LP64	bitwuzla	⚠️	41s	5s	+720%
	LP64	z3*	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	54s	114s	-53%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	4s	2s	+100%
`poly_power2round`	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	bitwuzla	✅	17s	3s	+467%
	LP64	z3*	✅	4s	3s	+33%
`poly_uniform`	LP64	z3*	✅	1s	6s	-83%
`poly_uniform_4x`	LP64	z3*	✅	9s	14s	-36%
`poly_uniform_eta`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	11s	-18%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint_native`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	37s	2s	+1750%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	37s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	5s	14s	-64%
	LP64	z3*	✅	5s	14s	-64%
`polyt0_pack`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	1s	2s	-50%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	7s	15s	-53%
`polyt1_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	19s	28s	-32%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	8s	-62%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	5s	2s	+150%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	15s	15s	+0%
`polyveck_caddq`	LP64	z3*	✅	1s	3s	-67%
`polyveck_chknorm`	LP64	z3*	⚠️	75s	5s	+1400%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	4s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	1s	5s	-80%
`polyveck_ntt`	LP64	z3*	✅	3s	5s	-40%
`polyveck_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyveck_reduce`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	1s	5s	-80%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_chknorm`	LP64	z3*	✅	4s	10s	-60%
`polyvecl_ntt`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_pack_eta`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	1s	4s	-75%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	⚠️	201s	131s	+53%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	2s	+0%
`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*	✅	2s	2s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	5s	1s	+400%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	5s	-20%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	11s	-82%
	LP64	z3*	✅	6s	11s	-45%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	2s	+1250%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	19s	4s	+375%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	13s	6s	+117%
`rej_uniform`	LP64	bitwuzla	✅	4s	18s	-78%
	LP64	z3*	✅	14s	18s	-22%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	11s	15s	-27%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`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	✅	19s	4s	+375%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3_smt_only*	✅	11s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`shake128_release`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3	✅	1s	1s	+0%
`shake256`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`shake256_absorb`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`shake256_release`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	3s	4s	-25%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	60s	2s	+2900%
	LP64	z3*	⚠️	27s	2s	+1250%
`sign_keypair`	LP64	z3*	✅	6s	4s	+50%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	17s	4s	+325%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	45s	5s	+800%
`sign_signature`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_extmu`	LP64	z3*	✅	5s	4s	+25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	134s	26s	+415%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	3s	6s	-50%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	5s	3s	+67%
`sign_verify`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	334s	114s	+193%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	30s	2s	+1400%
	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	34s	2s	+1600%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	5s	+140%
	LP64	z3*	✅	1s	5s	-80%
`unpack_sk`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s1hat`	LP64	z3*	✅	3s	1s	+200%
`unpack_sk_s2hat`	LP64	z3*	✅	3s	4s	-25%
`unpack_sk_t0hat`	LP64	z3*	✅	1s	3s	-67%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	⚠️	42s	3s	+1300%
	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*	⚠️	145s	13s	+1015%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	25s	3s	+733%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	23s	3s	+667%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	211s	63s	+235%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	80s	2s	+3900%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	23s	2s	+1050%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	23s	2s	+1050%
`poly_caddq_native`	LP64	bitwuzla	⚠️	58s	2s	+2800%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	37s	3s	+1133%
`poly_challenge`	LP64	bitwuzla	⚠️	23s	6s	+283%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	38s	2s	+1800%
`poly_ntt_c`	LP64	bitwuzla	⚠️	44s	19s	+132%
`poly_ntt_native`	LP64	bitwuzla	⚠️	36s	4s	+800%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	30s	3s	+900%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	25s	4s	+525%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1245s	2s	+62150%
	LP64	z3*	⚠️	28s	2s	+1300%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	29s	5s	+480%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	53s	6s	+783%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	199s	55s	+262%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	343s	3s	+11333%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	411s	177s	+132%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	38s	6s	+533%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
`yvec_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%

Full Results (370 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2112s	1784s	+18.4%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	145s	13s	+1015%
`decompose`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`fqmul`	LP64	bitwuzla*	✅	25s	40s	-38%
	LP64	z3_smt_only	✅	20s	40s	-50%
`fqscale`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	25s	3s	+733%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	23s	3s	+667%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	8s	-12%
	LP64	cvc5_arrays_exp	✅	7s	8s	-12%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	3s	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	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccak_init`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3	✅	2s	5s	-60%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	23s	-43%
	LP64	z3*	✅	11s	23s	-52%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	211s	63s	+235%
`mld_check_pct`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	5s	14s	-64%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	5s	7s	-29%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	1s	2s	-50%
	ILP32	z3	✅	4s	2s	+100%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	⚠️	80s	2s	+3900%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	64s	109s	-41%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	6s	6s	+0%
	LP64	z3*	✅	4s	6s	-33%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	24s	-54%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	41s	-44%
	LP64	z3_no_bv_extract	✅	1s	41s	-98%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_s1_s2`	LP64	z3*	✅	3s	6s	-50%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	4s	-25%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3*	✅	1s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	2s	+850%
	LP64	z3*	✅	3s	2s	+50%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	23s	2s	+1050%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	4s	5s	-20%
	LP64	z3*	✅	2s	5s	-60%
`pack_sig_h`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3_no_bv_extract*	✅	1s	5s	-80%
`pack_sig_z`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	23s	2s	+1050%
	LP64	z3*	✅	3s	2s	+50%
`pack_sk_s1`	LP64	bitwuzla	✅	8s	5s	+60%
	LP64	z3*	✅	4s	5s	-20%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	8s	-50%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	10s	5s	+100%
	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	3s	3s	+0%
`poly_add`	LP64	z3*	✅	5s	9s	-44%
`poly_caddq`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	2s	+800%
	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_native`	LP64	bitwuzla	⚠️	58s	2s	+2800%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	37s	3s	+1133%
	LP64	z3*	✅	2s	3s	-33%
`poly_challenge`	LP64	bitwuzla	⚠️	23s	6s	+283%
	LP64	z3*	✅	5s	6s	-17%
`poly_chknorm`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	15s	-53%
	LP64	z3*	✅	5s	15s	-67%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	1s	2s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`poly_decompose_c`	LP64	z3*	✅	1s	5s	-80%
`poly_decompose_native`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	8s	11s	-27%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	38s	2s	+1800%
	LP64	z3*	✅	3s	2s	+50%
`poly_ntt`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_ntt_c`	LP64	bitwuzla	⚠️	44s	19s	+132%
	LP64	z3_smt_only*	✅	11s	19s	-42%
`poly_ntt_native`	LP64	bitwuzla	⚠️	36s	4s	+800%
	LP64	z3*	✅	4s	4s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	49s	125s	-61%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	4s	3s	+33%
`poly_power2round`	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	3s	3s	+0%
`poly_sub`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform`	LP64	z3*	✅	5s	4s	+25%
`poly_uniform_4x`	LP64	z3*	✅	7s	13s	-46%
`poly_uniform_eta`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	14s	-43%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
	LP64	z3*	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	z3*	✅	4s	5s	-20%
`poly_use_hint_native`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	30s	3s	+900%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	6s	3s	+100%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	8s	-88%
	LP64	z3*	✅	3s	8s	-62%
`polyt0_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	16s	-81%
	LP64	z3*	✅	10s	16s	-38%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	5s	-80%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	69s	110s	-37%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	14s	27s	-48%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	14s	18s	-22%
`polyveck_caddq`	LP64	z3*	✅	5s	6s	-17%
`polyveck_chknorm`	LP64	z3*	✅	4s	6s	-33%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	5s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	8s	-38%
`polyveck_ntt`	LP64	z3*	✅	4s	7s	-43%
`polyveck_pack_eta`	LP64	z3*	✅	1s	4s	-75%
`polyveck_reduce`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	6s	-67%
`polyvecl_chknorm`	LP64	z3*	✅	3s	7s	-57%
`polyvecl_ntt`	LP64	z3*	✅	5s	4s	+25%
`polyvecl_pack_eta`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	180s	210s	-14%
`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*	✅	2s	3s	-33%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	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	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	13s	-85%
	LP64	z3*	✅	4s	13s	-69%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	25s	4s	+525%
	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	1s	3s	-67%
`power2round`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`reduce32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	10s	5s	+100%
`rej_eta_native`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	8s	3s	+167%
`rej_uniform`	LP64	bitwuzla	✅	1s	18s	-94%
	LP64	z3*	✅	12s	18s	-33%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	14s	-86%
	LP64	z3*	✅	9s	14s	-36%
`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	✅	1s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	6s	4s	+50%
	LP64	z3_smt_only	✅	16s	4s	+300%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3_smt_only*	✅	11s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`shake128_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake128_squeeze`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`shake256`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	4s	1s	+300%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1245s	2s	+62150%
	LP64	z3*	⚠️	28s	2s	+1300%
`sign_keypair`	LP64	z3*	✅	6s	3s	+100%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	29s	5s	+480%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	53s	6s	+783%
`sign_signature`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	5s	6s	-17%
`sign_signature_extmu`	LP64	z3*	✅	3s	2s	+50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	199s	55s	+262%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	343s	3s	+11333%
	LP64	z3*	✅	5s	3s	+67%
`sign_verify`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	411s	177s	+132%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	38s	6s	+533%
	LP64	z3*	✅	3s	6s	-50%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
	LP64	z3*	✅	4s	2s	+100%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	29s	2s	+1350%
	LP64	z3*	✅	3s	2s	+50%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	5s	+140%
	LP64	z3*	✅	3s	5s	-40%
`unpack_sk`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s1hat`	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	4s	5s	-20%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	3s	3s	+0%

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

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2765s	2151s	+28.5%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	205s	19s	+979%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	25s	3s	+733%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	23s	3s	+667%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	371s	55s	+575%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	81s	3s	+2600%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	24s	2s	+1100%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	55s	3s	+1733%
`poly_caddq_native`	LP64	bitwuzla	⚠️	55s	4s	+1275%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	37s	2s	+1750%
`poly_challenge`	LP64	bitwuzla	⚠️	32s	5s	+540%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	5s	inconclusive
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	39s	5s	+680%
`poly_ntt_c`	LP64	bitwuzla	⚠️	48s	21s	+129%
`poly_ntt_native`	LP64	bitwuzla	⚠️	35s	3s	+1067%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	27s	2s	+1250%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	24s	4s	+500%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	25s	3s	+733%
	LP64	z3*	⚠️	30s	3s	+900%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	47s	6s	+683%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	56s	6s	+833%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	362s	42s	+762%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1396s	6s	+23167%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	611s	97s	+530%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	32s	4s	+700%
`yvec_get_poly`	LP64	bitwuzla	⚠️	37s	4s	+825%

Full Results (370 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2765s	2151s	+28.5%
`caddq`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	205s	19s	+979%
`decompose`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`fqmul`	LP64	bitwuzla*	✅	24s	43s	-44%
	LP64	z3_smt_only	✅	20s	43s	-53%
`fqscale`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	25s	3s	+733%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	23s	3s	+667%
	LP64	z3*	✅	1s	3s	-67%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	9s	-33%
	LP64	cvc5_arrays_exp	✅	7s	9s	-22%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	4s	-75%
`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*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	2s	4s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccak_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	11s	23s	-52%
	LP64	z3*	✅	12s	23s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`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*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	371s	55s	+575%
`mld_check_pct`	LP64	bitwuzla	✅	5s	16s	-69%
	LP64	z3*	✅	5s	16s	-69%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	5s	8s	-38%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	4s	3s	+33%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_no_bv_extract	⚠️	81s	3s	+2600%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`mld_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	61s	115s	-47%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	6s	7s	-14%
	LP64	z3*	✅	4s	7s	-43%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	24s	-54%
`mld_ntt_layer`	LP64	bitwuzla*	✅	21s	45s	-53%
	LP64	z3_no_bv_extract	✅	3s	45s	-93%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	2s	8s	-75%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	-	new
	LP64	z3*	✅	4s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	✅	17s	6s	+183%
	LP64	z3*	✅	2s	6s	-67%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	24s	2s	+1100%
	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	4s	4s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	5s	-80%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	55s	3s	+1733%
	LP64	z3*	✅	2s	3s	-33%
`pack_sk_s1`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	1s	1s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	5s	6s	-17%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	6s	6s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	8s	5s	+60%
	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	10s	2s	+400%
	LP64	z3*	✅	1s	2s	-50%
`poly_add`	LP64	z3*	✅	3s	6s	-50%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	bitwuzla	✅	17s	3s	+467%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	55s	4s	+1275%
	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	37s	2s	+1750%
	LP64	z3*	✅	3s	2s	+50%
`poly_challenge`	LP64	bitwuzla	⚠️	32s	5s	+540%
	LP64	z3*	✅	4s	5s	-20%
`poly_chknorm`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	15s	-40%
	LP64	z3*	✅	6s	15s	-60%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	5s	inconclusive
	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_c`	LP64	z3*	✅	1s	5s	-80%
`poly_decompose_native`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	12s	-42%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	39s	5s	+680%
	LP64	z3*	✅	2s	5s	-60%
`poly_ntt`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	bitwuzla	⚠️	48s	21s	+129%
	LP64	z3_smt_only*	✅	10s	21s	-52%
`poly_ntt_native`	LP64	bitwuzla	⚠️	35s	3s	+1067%
	LP64	z3*	✅	5s	3s	+67%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	47s	144s	-67%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	4s	5s	-20%
`poly_power2round`	LP64	z3*	✅	3s	3s	+0%
`poly_reduce`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	2s	2s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	10s	4s	+150%
	LP64	z3*	✅	1s	4s	-75%
`poly_sub`	LP64	bitwuzla	✅	13s	3s	+333%
	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*	✅	3s	4s	-25%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	11s	-18%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint`	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_c`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	27s	2s	+1250%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	29s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	17s	-88%
	LP64	z3*	✅	6s	17s	-65%
`polyt0_pack`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	14s	-86%
	LP64	z3*	✅	6s	14s	-57%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	114s	324s	-65%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	18s	38s	-53%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	10s	18s	-44%
`polyveck_caddq`	LP64	z3*	✅	9s	8s	+12%
`polyveck_chknorm`	LP64	z3*	✅	1s	3s	-67%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	8s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	9s	-44%
`polyveck_ntt`	LP64	z3*	✅	5s	11s	-55%
`polyveck_pack_eta`	LP64	z3*	✅	3s	6s	-50%
`polyveck_reduce`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`polyveck_unpack_eta`	LP64	z3*	✅	4s	4s	+0%
`polyvecl_chknorm`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_ntt`	LP64	z3*	✅	5s	7s	-29%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	3s	5s	-40%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	211s	353s	-40%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	3s	4s	-25%
`polyvecl_unpack_eta`	LP64	z3*	✅	1s	5s	-80%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	5s	4s	+25%
`polyw1_pack_88`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	4s	5s	-20%
`polyz_unpack`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	24s	4s	+500%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`reduce32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`rej_eta`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	5s	4s	+25%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	16s	5s	+220%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	10s	6s	+67%
`rej_uniform`	LP64	bitwuzla	✅	3s	15s	-80%
	LP64	z3*	✅	11s	15s	-27%
`rej_uniform_c`	LP64	bitwuzla	✅	5s	19s	-74%
	LP64	z3*	✅	9s	19s	-53%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	1s	5s	-80%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	8s	-62%
	LP64	z3_smt_only	✅	15s	8s	+88%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3_smt_only*	✅	10s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`shake128_release`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	2s	5s	-60%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	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*	⚠️	30s	3s	+900%
`sign_keypair`	LP64	z3*	✅	4s	4s	+0%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	47s	6s	+683%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	56s	6s	+833%
`sign_signature`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	5s	-40%
`sign_signature_extmu`	LP64	z3*	✅	4s	4s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	362s	42s	+762%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	5s	-60%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1396s	6s	+23167%
	LP64	z3*	✅	8s	6s	+33%
`sign_verify`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	5s	-40%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	611s	97s	+530%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	3s	+33%
`sk_s1hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	⚠️	32s	4s	+700%
	LP64	z3*	✅	2s	4s	-50%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	1s	+900%
	LP64	z3*	✅	3s	1s	+200%
`unpack_sk`	LP64	z3*	✅	2s	5s	-60%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_t0hat`	LP64	z3*	✅	5s	7s	-29%
`use_hint`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`yvec_get_poly`	LP64	bitwuzla	⚠️	37s	4s	+825%
	LP64	z3*	✅	2s	4s	-50%
`yvec_init`	LP64	bitwuzla	✅	15s	4s	+275%
	LP64	z3*	✅	2s	4s	-50%

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*	⚠️	38s	7s	+443%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	28s	2s	+1300%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	24s	4s	+500%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	144s	31s	+365%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	91s	4s	+2175%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	27s	5s	+440%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	24s	2s	+1100%
`poly_caddq_c`	LP64	bitwuzla	⚠️	21s	5s	+320%
`poly_caddq_native`	LP64	bitwuzla	⚠️	63s	4s	+1475%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	40s	1s	+3900%
`poly_challenge`	LP64	bitwuzla	⚠️	25s	5s	+400%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	4s	inconclusive
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	5s	+820%
`poly_ntt_c`	LP64	bitwuzla	⚠️	53s	22s	+141%
`poly_ntt_native`	LP64	bitwuzla	⚠️	40s	2s	+1900%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	31s	4s	+675%
`polyveck_reduce`	LP64	cvc5_arrays_exp	⚠️	?	6s	inconclusive
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	3s	+800%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	21s	4s	+425%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1430s	1s	+142900%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	28s	3s	+833%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	68s	5s	+1260%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	377s	7s	+5286%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	231s	71s	+225%

Full Results (370 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1520s	1482s	+2.6%
`caddq`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	38s	7s	+443%
`decompose`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`fqmul`	LP64	bitwuzla*	✅	26s	40s	-35%
	LP64	z3_smt_only	✅	22s	40s	-45%
`fqscale`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	28s	2s	+1300%
	LP64	z3*	✅	2s	2s	+0%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	24s	4s	+500%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	10s	-50%
	LP64	cvc5_arrays_exp	✅	9s	10s	-10%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	11s	22s	-50%
	LP64	z3*	✅	14s	22s	-36%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	144s	31s	+365%
`mld_check_pct`	LP64	bitwuzla	✅	6s	12s	-50%
	LP64	z3*	✅	6s	12s	-50%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	4s	6s	-33%
	ILP32	cvc5_arrays_exp	✅	1s	6s	-83%
	ILP32	z3	✅	1s	6s	-83%
	LP64	bitwuzla	✅	1s	6s	-83%
	LP64	cvc5_arrays_exp	✅	2s	6s	-67%
	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	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	3s	4s	-25%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_no_bv_extract	⚠️	91s	4s	+2175%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_invntt_layer`	LP64	bitwuzla*	✅	71s	108s	-34%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	7s	-57%
	LP64	z3*	✅	4s	7s	-43%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	25s	-48%
`mld_ntt_layer`	LP64	bitwuzla*	✅	27s	43s	-37%
	LP64	z3_no_bv_extract	✅	1s	43s	-98%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	4s	3s	+33%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	3s	+500%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	27s	5s	+440%
	LP64	z3*	✅	3s	5s	-40%
`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	✅	4s	2s	+100%
	LP64	z3_no_bv_extract*	✅	4s	2s	+100%
`pack_sig_z`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	24s	2s	+1100%
	LP64	z3*	✅	4s	2s	+100%
`pack_sk_s1`	LP64	bitwuzla	✅	9s	3s	+200%
	LP64	z3*	✅	2s	3s	-33%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	5s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	1s	3s	-67%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	10s	2s	+400%
	LP64	z3*	✅	4s	2s	+100%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_c`	LP64	bitwuzla	⚠️	21s	5s	+320%
	LP64	z3*	✅	4s	5s	-20%
`poly_caddq_native`	LP64	bitwuzla	⚠️	63s	4s	+1475%
	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	40s	1s	+3900%
	LP64	z3*	✅	2s	1s	+100%
`poly_challenge`	LP64	bitwuzla	⚠️	25s	5s	+400%
	LP64	z3*	✅	4s	5s	-20%
`poly_chknorm`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	6s	13s	-54%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	4s	inconclusive
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	3s	8s	-62%
`poly_decompose_native`	LP64	z3*	✅	1s	5s	-80%
`poly_decompose_native_x86_64`	LP64	z3*	✅	4s	2s	+100%
`poly_invntt_tomont`	LP64	bitwuzla	✅	8s	5s	+60%
	LP64	z3*	✅	2s	5s	-60%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	10s	-30%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	5s	+820%
	LP64	z3*	✅	1s	5s	-80%
`poly_ntt`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	4s	2s	+100%
`poly_ntt_c`	LP64	bitwuzla	⚠️	53s	22s	+141%
	LP64	z3_smt_only*	✅	10s	22s	-55%
`poly_ntt_native`	LP64	bitwuzla	⚠️	40s	2s	+1900%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	6s	3s	+100%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	13s	2s	+550%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	78s	116s	-33%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	4s	-50%
`poly_power2round`	LP64	z3*	✅	3s	7s	-57%
`poly_reduce`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	bitwuzla	✅	16s	4s	+300%
	LP64	z3*	✅	2s	4s	-50%
`poly_uniform`	LP64	z3*	✅	4s	2s	+100%
`poly_uniform_4x`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta`	LP64	z3*	✅	3s	5s	-40%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	13s	-38%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
	LP64	z3*	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	5s	3s	+67%
`poly_use_hint`	LP64	z3*	✅	1s	3s	-67%
`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	⚠️	31s	4s	+675%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	-	new
	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	1s	+300%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	4s	5s	-20%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	13s	-77%
	LP64	z3*	✅	8s	13s	-38%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	4s	6s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	8s	-62%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	196s	201s	-2%
`polyveck_caddq`	LP64	z3*	✅	3s	7s	-57%
`polyveck_chknorm`	LP64	z3*	✅	7s	36s	-81%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	8s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	3s	7s	-57%
`polyveck_ntt`	LP64	z3*	✅	1s	4s	-75%
`polyveck_pack_eta`	LP64	z3*	✅	3s	3s	+0%
`polyveck_reduce`	LP64	cvc5_arrays_exp	⚠️	?	6s	inconclusive
	LP64	z3*	✅	5s	6s	-17%
`polyveck_unpack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_chknorm`	LP64	z3*	✅	6s	43s	-86%
`polyvecl_ntt`	LP64	z3*	✅	5s	7s	-29%
`polyvecl_pack_eta`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	3s	4s	-25%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	1s	1s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	9s	-78%
	LP64	z3*	✅	6s	9s	-33%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	27s	3s	+800%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`reduce32`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	2s	+50%
`rej_eta`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3_smt_only	✅	4s	5s	-20%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	18s	4s	+350%
`rej_eta_native`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	10s	3s	+233%
`rej_uniform`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	6s	7s	-14%
`rej_uniform_c`	LP64	bitwuzla	✅	1s	16s	-94%
	LP64	z3*	✅	10s	16s	-38%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	4s	5s	-20%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	⚠️	21s	4s	+425%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3_smt_only	✅	3s	5s	-40%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3_smt_only*	✅	10s	-	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	✅	1s	6s	-83%
	LP64	z3*	✅	3s	6s	-50%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	1s	2s	-50%
`shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%
`shake256_release`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	1s	4s	-75%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	1430s	1s	+142900%
	LP64	z3*	✅	12s	1s	+1100%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	28s	3s	+833%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	68s	5s	+1260%
`sign_signature`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	5s	-60%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	13s	6s	+117%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	377s	7s	+5286%
	LP64	z3*	✅	5s	7s	-29%
`sign_verify`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	3s	6s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	231s	71s	+225%
`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*	✅	5s	6s	-17%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`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*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	z3*	✅	3s	4s	-25%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	3s	3s	+0%
`yvec_init`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%

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*	⚠️	36s	12s	+200%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	30s	4s	+650%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	27s	4s	+575%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	173s	34s	+409%
`mld_ct_memcmp`	LP64	z3_no_bv_extract	⚠️	99s	1s	+9800%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	22s	4s	+450%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	29s	2s	+1350%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	63s	2s	+3050%
`poly_caddq_c`	LP64	bitwuzla	⚠️	22s	3s	+633%
`poly_caddq_native`	LP64	bitwuzla	⚠️	67s	3s	+2133%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	46s	3s	+1433%
`poly_challenge`	LP64	bitwuzla	⚠️	40s	4s	+900%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	2s	+2200%
`poly_ntt_c`	LP64	bitwuzla	⚠️	58s	19s	+205%
`poly_ntt_native`	LP64	bitwuzla	⚠️	41s	4s	+925%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	33s	3s	+1000%
`polyveck_reduce`	LP64	cvc5_arrays_exp	⚠️	?	6s	inconclusive
`polyz_unpack_native`	LP64	bitwuzla	⚠️	29s	1s	+2800%
`rej_eta_c`	LP64	z3	⚠️	28s	4s	+600%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	30s	4s	+650%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	41s	6s	+583%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	101s	6s	+1583%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1657s	3s	+55133%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	245s	47s	+421%

Full Results (370 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1591s	1436s	+10.8%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	36s	12s	+200%
`decompose`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`fqmul`	LP64	bitwuzla*	✅	27s	39s	-31%
	LP64	z3_smt_only	✅	22s	39s	-44%
`fqscale`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`intt_native_aarch64`	LP64	bitwuzla	⚠️	30s	4s	+650%
	LP64	z3*	✅	2s	4s	-50%
`intt_native_x86_64`	LP64	bitwuzla	⚠️	27s	4s	+575%
	LP64	z3*	✅	4s	4s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	5s	4s	+25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	8s	-25%
	LP64	cvc5_arrays_exp	✅	10s	8s	+25%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	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*	✅	1s	1s	+0%
	LP64	z3	✅	3s	1s	+200%
`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	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	4s	1s	+300%
`keccak_init`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3	✅	1s	5s	-80%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	11s	25s	-56%
	LP64	z3*	✅	13s	25s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`make_hint`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	173s	34s	+409%
`mld_check_pct`	LP64	bitwuzla	✅	7s	15s	-53%
	LP64	z3*	✅	6s	15s	-60%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	2s	1s	+100%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	5s	2s	+150%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`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	⚠️	99s	1s	+9800%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	74s	111s	-33%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	8s	-62%
	LP64	z3*	✅	6s	8s	-25%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	16s	23s	-30%
`mld_ntt_layer`	LP64	bitwuzla*	✅	28s	44s	-36%
	LP64	z3_no_bv_extract	✅	4s	44s	-91%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`mld_sample_s1_s2`	LP64	z3*	✅	5s	8s	-38%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	5s	6s	-17%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`mld_sign_finish`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	2s	-	new
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	22s	4s	+450%
	LP64	z3*	✅	1s	4s	-75%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	29s	2s	+1350%
	LP64	z3*	✅	1s	2s	-50%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	LP64	bitwuzla	⚠️	63s	2s	+3050%
	LP64	z3*	✅	3s	2s	+50%
`pack_sk_s1`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	5s	5s	+0%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	8s	-50%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	12s	4s	+200%
	LP64	z3*	✅	2s	4s	-50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	13s	5s	+160%
	LP64	z3*	✅	2s	5s	-60%
`poly_add`	LP64	z3*	✅	4s	8s	-50%
`poly_caddq`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_c`	LP64	bitwuzla	⚠️	22s	3s	+633%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	⚠️	67s	3s	+2133%
	LP64	z3*	✅	5s	3s	+67%
`poly_caddq_native_aarch64`	LP64	z3*	✅	5s	3s	+67%
`poly_caddq_native_x86_64`	LP64	bitwuzla	⚠️	46s	3s	+1433%
	LP64	z3*	✅	3s	3s	+0%
`poly_challenge`	LP64	bitwuzla	⚠️	40s	4s	+900%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	4s	-75%
`poly_chknorm_c`	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	7s	13s	-46%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	1s	+600%
	LP64	z3*	✅	4s	1s	+300%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	5s	-40%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	cvc5_arrays_exp	⚠️	?	3s	inconclusive
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	4s	6s	-33%
`poly_decompose_native`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	9s	-22%
`poly_invntt_tomont_native`	LP64	bitwuzla	⚠️	46s	2s	+2200%
	LP64	z3*	✅	3s	2s	+50%
`poly_ntt`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	4s	2s	+100%
`poly_ntt_c`	LP64	bitwuzla	⚠️	58s	19s	+205%
	LP64	z3_smt_only*	✅	12s	19s	-37%
`poly_ntt_native`	LP64	bitwuzla	⚠️	41s	4s	+925%
	LP64	z3*	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	75s	125s	-40%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	4s	3s	+33%
`poly_power2round`	LP64	z3*	✅	4s	7s	-43%
`poly_reduce`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	1s	4s	-75%
`poly_shiftl`	LP64	bitwuzla	✅	15s	4s	+275%
	LP64	z3*	✅	4s	4s	+0%
`poly_sub`	LP64	bitwuzla	✅	16s	5s	+220%
	LP64	z3*	✅	1s	5s	-80%
`poly_uniform`	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_4x`	LP64	z3*	✅	4s	3s	+33%
`poly_uniform_eta`	LP64	z3*	✅	1s	5s	-80%
`poly_uniform_eta_4x`	LP64	z3*	✅	7s	12s	-42%
`poly_uniform_gamma1`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native`	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	⚠️	33s	3s	+1000%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	34s	-	new
	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	13s	-77%
	LP64	z3*	✅	6s	13s	-54%
`polyt0_pack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	14s	-79%
	LP64	z3*	✅	8s	14s	-43%
`polyt1_pack`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	5s	-80%
`polyt1_unpack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	8s	13s	-38%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	139s	196s	-29%
`polyveck_caddq`	LP64	z3*	✅	7s	8s	-12%
`polyveck_chknorm`	LP64	z3*	✅	4s	9s	-56%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	6s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	4s	+0%
`polyveck_ntt`	LP64	z3*	✅	4s	3s	+33%
`polyveck_pack_eta`	LP64	z3*	✅	2s	5s	-60%
`polyveck_reduce`	LP64	cvc5_arrays_exp	⚠️	?	6s	inconclusive
	LP64	z3*	✅	5s	6s	-17%
`polyveck_unpack_eta`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_chknorm`	LP64	z3*	✅	4s	38s	-89%
`polyvecl_ntt`	LP64	z3*	✅	7s	8s	-12%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	1s	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*	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	z3*	✅	1s	3s	-67%
`polyw1_pack`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	-	new
	LP64	z3*	✅	6s	-	new
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	-	new
	LP64	z3*	✅	1s	-	new
`polyz_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	5s	7s	-29%
`polyz_unpack_native`	LP64	bitwuzla	⚠️	29s	1s	+2800%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	3s	+467%
	LP64	z3*	✅	1s	3s	-67%
`power2round`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`reduce32`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	3s	+33%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	5s	2s	+150%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	⚠️	28s	4s	+600%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	16s	4s	+300%
`rej_uniform`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	5s	7s	-29%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	18s	-83%
	LP64	z3*	✅	13s	18s	-28%
`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	✅	5s	-	new
	LP64	z3_smt_only*	✅	4s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	19s	5s	+280%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	-	new
	LP64	z3_smt_only*	✅	11s	-	new
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`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*	✅	3s	3s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`shake256_release`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	5s	-80%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	3s	5s	-40%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	bitwuzla	⚠️	30s	4s	+650%
	LP64	z3*	✅	18s	4s	+350%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	41s	6s	+583%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	101s	6s	+1583%
`sign_signature`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	8s	4s	+100%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	17s	3s	+467%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	4s	2s	+100%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	⚠️	1657s	3s	+55133%
	LP64	z3*	✅	5s	3s	+67%
`sign_verify`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_extmu`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	245s	47s	+421%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	2s	7s	-71%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	6s	3s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	2s	+500%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk`	LP64	z3*	✅	1s	4s	-75%
`unpack_sk_s1hat`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s2hat`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	4s	-50%
`use_hint`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`yvec_get_poly`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%

Navigation Menu

CBMC: Use a second solver for 154/212 proofs - #1423

CBMC: Use a second solver for 154/212 proofs#1423
mkannwischer wants to merge 1 commit into
mainfrom
mjk/cbmc-lp64-two-solvers

mkannwischer commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mkannwischer commented Sep 9, 2026

Uh oh!

oqs-bot commented Sep 9, 2026

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

Uh oh!

oqs-bot commented Sep 9, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Sep 9, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Sep 9, 2026

CBMC Results (ML-DSA-87)

Uh oh!

oqs-bot commented Sep 9, 2026

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

Uh oh!

oqs-bot commented Sep 9, 2026

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

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants