[mkannwischer]

No description provided.

[oqs-bot]

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

* default.

Full Results (415 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1509s	1484s	+1.7%
caddq	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	1s	+200%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	37s	39s	-5%
decompose	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
fqmul	LP64	bitwuzla*	✅	27s	24s	+12%
	LP64	z3_smt_only	✅	20s	20s	+0%
fqscale	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	3s	3s	+0%
intt_native_aarch64	LP64	bitwuzla	✅	24s	21s	+14%
	LP64	z3*	✅	1s	3s	-67%
intt_native_rv32im_fastmul	ILP32	z3*	✅	5s	3s	+67%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	1s	2s	-50%
intt_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	2s	+50%
intt_native_x86_64	LP64	bitwuzla	✅	17s	19s	-11%
	LP64	z3*	✅	4s	3s	+33%
keccak_absorb	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	5s	-40%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	cvc5_arrays_exp	✅	7s	8s	-12%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	1s	4s	-75%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	3s	+0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
keccak_finalize	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
keccak_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
keccak_squeeze	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	2s	+0%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	4s	1s	+300%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
keccakf1600_permute	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
keccakf1600_permute_native	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	1s	+0%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	2s	-50%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	12s	12s	+0%
	LP64	z3*	✅	11s	12s	-8%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
make_hint	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	220s	210s	+5%
mld_check_pct	LP64	bitwuzla	✅	10s	6s	+67%
	LP64	z3*	✅	4s	5s	-20%
mld_compute_pack_z	LP64	cadical	✅	41s	43s	-5%
	LP64	z3_no_bv_extract*	✅	3s	4s	-25%
mld_ct_abs_i32	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	4s	3s	+33%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
mld_ct_memcmp	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	89s	83s	+7%
mld_ct_sel_int32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_h	LP64	bitwuzla	✅	1s	6s	-83%
	LP64	z3*	✅	3s	1s	+200%
mld_invntt_layer	LP64	bitwuzla*	✅	70s	67s	+4%
	LP64	z3_smt_only	✅	78s	75s	+4%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	5s	-40%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	1s	+0%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	14s	14s	+0%
	LP64	z3_no_bv_extract	✅	130s	121s	+7%
mld_ntt_layer	LP64	bitwuzla*	✅	25s	26s	-4%
	LP64	z3_no_bv_extract	✅	3s	4s	-25%
mld_polymat_expand_entry	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
mld_sample_pack_s1_s2	LP64	cadical	✅	57s	51s	+12%
	LP64	z3*	✅	3s	4s	-25%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	233s	234s	-0%
	LP64	z3*	✅	5s	3s	+67%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_sign_finish	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
mld_sign_resume	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
mld_value_barrier_u32	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
ntt_native_aarch64	LP64	bitwuzla	✅	23s	20s	+15%
	LP64	z3*	✅	2s	2s	+0%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	1s	4s	-75%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	3s	2s	+50%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	7s	5s	+40%
	LP64	z3	✅	2s	2s	+0%
ntt_native_x86_64	LP64	bitwuzla	✅	19s	18s	+6%
	LP64	z3*	✅	3s	2s	+50%
nttunpack_native_x86_64	LP64	bitwuzla	✅	168s	161s	+4%
	LP64	z3*	✅	4s	2s	+100%
pack_sig_c	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	4s	-25%
pack_sig_h	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
pack_sig_z	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
pointwise_acc_native_aarch64	LP64	z3_smt_only*	✅	3s	5s	-40%
pointwise_acc_native_x86_64	LP64	cadical	✅	96s	84s	+14%
	LP64	z3_smt_only*	✅	3s	4s	-25%
pointwise_native_aarch64	LP64	bitwuzla	✅	23s	22s	+5%
	LP64	z3*	✅	2s	2s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	1s	3s	-67%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	2s	4s	-50%
pointwise_native_x86_64	LP64	bitwuzla	✅	23s	20s	+15%
	LP64	z3*	✅	3s	3s	+0%
poly_add	LP64	z3*	✅	5s	4s	+25%
poly_caddq	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	4s	-50%
poly_caddq_c	LP64	bitwuzla	✅	21s	19s	+11%
	LP64	z3*	✅	3s	3s	+0%
poly_caddq_native	LP64	bitwuzla	✅	123s	115s	+7%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	35s	35s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	131s	127s	+3%
	LP64	z3*	✅	2s	3s	-33%
poly_challenge	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	2s	5s	-60%
poly_chknorm	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_c	LP64	bitwuzla	✅	9s	10s	-10%
	LP64	z3*	✅	6s	7s	-14%
poly_chknorm_native	LP64	bitwuzla	✅	7s	7s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	10s	11s	-9%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_c	LP64	z3*	✅	6s	7s	-14%
poly_decompose_native	LP64	cadical	✅	15s	16s	-6%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_native_x86_64	LP64	cadical	✅	11s	9s	+22%
	LP64	z3*	✅	2s	3s	-33%
poly_invntt_tomont	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	3s	4s	-25%
poly_invntt_tomont_c	LP64	bitwuzla	✅	170s	164s	+4%
	LP64	z3_smt_only*	✅	6s	8s	-25%
poly_invntt_tomont_native	LP64	bitwuzla	✅	47s	50s	-6%
	LP64	z3*	✅	2s	3s	-33%
poly_ntt	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	3s	-67%
poly_ntt_c	LP64	bitwuzla	✅	51s	51s	+0%
	LP64	z3_smt_only*	✅	10s	10s	+0%
poly_ntt_native	LP64	bitwuzla	✅	29s	28s	+4%
	LP64	z3*	✅	2s	3s	-33%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	4s	-75%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_pointwise_montgomery	LP64	bitwuzla	✅	10s	9s	+11%
	LP64	z3*	✅	2s	1s	+100%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	193s	182s	+6%
	LP64	z3*	✅	86s	78s	+10%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	54s	51s	+6%
	LP64	z3*	✅	2s	3s	-33%
poly_power2round	LP64	bitwuzla	✅	322s	324s	-1%
	LP64	z3*	✅	3s	4s	-25%
poly_reduce	LP64	bitwuzla	✅	8s	9s	-11%
	LP64	z3*	✅	2s	1s	+100%
poly_shiftl	LP64	bitwuzla	✅	11s	11s	+0%
	LP64	z3*	✅	4s	3s	+33%
poly_sub	LP64	bitwuzla	✅	13s	14s	-7%
	LP64	z3*	✅	3s	3s	+0%
poly_uniform	LP64	bitwuzla	✅	166s	155s	+7%
	LP64	z3*	✅	2s	4s	-50%
poly_uniform_4x	LP64	z3*	✅	3s	2s	+50%
poly_uniform_eta	LP64	bitwuzla	✅	140s	147s	-5%
	LP64	z3*	✅	3s	3s	+0%
poly_uniform_eta_4x	LP64	z3*	✅	11s	8s	+38%
poly_uniform_gamma1	LP64	cadical	✅	4s	4s	+0%
	LP64	z3*	✅	2s	1s	+100%
poly_uniform_gamma1_4x	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	24s	26s	-8%
	LP64	z3*	✅	5s	1s	+400%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	13s	13s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	98s	95s	+3%
	LP64	z3*	✅	3s	1s	+200%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	32s	30s	+7%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	2s	4s	-50%
polyeta_pack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
polyeta_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
polyt0_pack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
polyt0_unpack	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	8s	7s	+14%
polyt1_pack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
polyt1_unpack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	6s	3s	+100%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
polyvec_matrix_expand_serial	LP64	z3*	✅	2s	2s	+0%
polyvec_matrix_pointwise_montgomery_row	LP64	z3_no_bv_extract*	✅	6s	5s	+20%
polyvec_matrix_pointwise_montgomery_yvec	LP64	z3*	✅	131s	129s	+2%
polyveck_caddq	LP64	z3*	✅	2s	5s	-60%
polyveck_decompose_pack_w1	LP64	z3*	✅	7s	9s	-22%
polyveck_invntt_tomont	LP64	z3*	✅	5s	4s	+25%
polyveck_ntt	LP64	z3*	✅	2s	2s	+0%
polyveck_reduce	LP64	z3*	✅	4s	5s	-20%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	20s	17s	+18%
	LP64	z3*	✅	1s	1s	+0%
polyvecl_chknorm	LP64	z3*	✅	3s	2s	+50%
polyvecl_ntt	LP64	z3*	✅	5s	3s	+67%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery_c	LP64	z3*	✅	1s	2s	-50%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	4s	3s	+33%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	38s	35s	+9%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	34s	34s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
polyw1_pack_32	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack_88	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
polyw1_unpack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
polyw1_unpack_32	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
polyz_pack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
polyz_unpack	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_c	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
polyz_unpack_native	LP64	bitwuzla	✅	30s	29s	+3%
	LP64	z3*	✅	2s	1s	+100%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	16s	19s	-16%
	LP64	z3*	✅	3s	2s	+50%
power2round	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
reduce32	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
rej_eta	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	2s	+50%
rej_eta_c	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	18s	17s	+6%
rej_eta_native	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	✅	9s	9s	+0%
rej_uniform	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	8s	-62%
rej_uniform_c	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	8s	9s	-11%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	4s	2s	+100%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3_smt_only*	✅	1s	5s	-80%
rej_uniform_native	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	21s	17s	+24%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	4s	1s	+300%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3_smt_only*	✅	8s	9s	-11%
shake128_absorb	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake128_finalize	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
shake128_init	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
shake128_release	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
shake128_squeeze	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
shake128x4_absorb_once	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	3s	-33%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	1s	+100%
shake256	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
shake256_absorb	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake256_finalize	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
shake256_init	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
shake256_release	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
shake256_squeeze	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
shake256x4_absorb_once	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	2s	-50%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	4s	3s	+33%
sig_unpack_hints	LP64	bitwuzla	✅	1463s	1334s	+10%
	LP64	z3*	✅	17s	17s	+0%
sign_keypair	LP64	z3*	✅	6s	5s	+20%
sign_keypair_internal	LP64	z3_no_bv_extract*	✅	20s	19s	+5%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	39s	35s	+11%
sign_signature	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_extmu	LP64	cadical	✅	37s	32s	+16%
	LP64	z3*	✅	2s	2s	+0%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	16s	17s	-6%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	3s	4s	-25%
sign_signature_pre_hash_shake256	LP64	bitwuzla	✅	356s	396s	-10%
	LP64	z3*	✅	6s	3s	+100%
sign_verify	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
sign_verify_extmu	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	241s	234s	+3%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	4s	+0%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
sk_s1hat_get_poly	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	5s	2s	+150%
sk_s2hat_get_poly	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
sk_t0hat_get_poly	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
sys_check_capability	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
unpack_pk_t1	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
unpack_sk_t0hat	LP64	z3*	✅	3s	3s	+0%
use_hint	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
yvec_get_poly	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	3s	1s	+200%
yvec_init	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%

[oqs-bot]

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

* default.

Full Results (415 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1472s	1665s	-11.6%
caddq	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	31s	36s	-14%
decompose	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
fqmul	LP64	bitwuzla*	✅	26s	26s	+0%
	LP64	z3_smt_only	✅	20s	23s	-13%
fqscale	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	7s	2s	+250%
intt_native_aarch64	LP64	bitwuzla	✅	21s	25s	-16%
	LP64	z3*	✅	3s	2s	+50%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	10s	8s	+25%
	LP64	z3	✅	2s	2s	+0%
intt_native_rv32im_slowmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	2s	1s	+100%
intt_native_x86_64	LP64	bitwuzla	✅	18s	21s	-14%
	LP64	z3*	✅	2s	2s	+0%
keccak_absorb	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	5s	-40%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	cvc5_arrays_exp	✅	7s	8s	-12%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	1s	+0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	1s	1s	+0%
	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	✅	2s	2s	+0%
	LP64	z3*	✅	6s	2s	+200%
keccak_init	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	2s	+150%
keccak_squeeze	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	1s	2s	-50%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
keccakf1600_permute	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
keccakf1600_permute_native	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	2s	-50%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	12s	12s	+0%
	LP64	z3*	✅	12s	12s	+0%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
make_hint	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	205s	243s	-16%
mld_check_pct	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	5s	8s	-38%
mld_compute_pack_z	LP64	cadical	✅	42s	44s	-5%
	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
mld_ct_abs_i32	ILP32	bitwuzla	✅	2s	4s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	3s	-67%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	4s	-25%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	79s	100s	-21%
mld_ct_sel_int32	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	1s	+100%
mld_h	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
mld_invntt_layer	LP64	bitwuzla*	✅	65s	76s	-14%
	LP64	z3_smt_only	✅	75s	85s	-12%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	6s	4s	+50%
	LP64	z3*	✅	2s	4s	-50%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	14s	12s	+17%
	LP64	z3_no_bv_extract	✅	121s	144s	-16%
mld_ntt_layer	LP64	bitwuzla*	✅	25s	30s	-17%
	LP64	z3_no_bv_extract	✅	1s	4s	-75%
mld_polymat_expand_entry	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
mld_sample_pack_s1_s2	LP64	cadical	✅	83s	94s	-12%
	LP64	z3*	✅	6s	5s	+20%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	540s	562s	-4%
	LP64	z3*	✅	5s	4s	+25%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
mld_sign_finish	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
mld_sign_resume	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_value_barrier_u32	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	4s	-75%
ntt_native_aarch64	LP64	bitwuzla	✅	21s	22s	-5%
	LP64	z3*	✅	2s	3s	-33%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	3s	5s	-40%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	3s	2s	+50%
ntt_native_x86_64	LP64	bitwuzla	✅	18s	19s	-5%
	LP64	z3*	✅	2s	3s	-33%
nttunpack_native_x86_64	LP64	bitwuzla	✅	187s	212s	-12%
	LP64	z3*	✅	2s	3s	-33%
pack_sig_c	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
pack_sig_h	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
pack_sig_z	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	4s	-50%
pointwise_acc_native_aarch64	LP64	z3_smt_only*	✅	6s	5s	+20%
pointwise_acc_native_x86_64	LP64	cadical	✅	106s	115s	-8%
	LP64	z3_smt_only*	✅	5s	5s	+0%
pointwise_native_aarch64	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	2s	1s	+100%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	1s	+100%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	10s	-20%
	LP64	z3	✅	3s	2s	+50%
pointwise_native_x86_64	LP64	bitwuzla	✅	23s	25s	-8%
	LP64	z3*	✅	3s	3s	+0%
poly_add	LP64	z3*	✅	3s	3s	+0%
poly_caddq	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
poly_caddq_c	LP64	bitwuzla	✅	19s	23s	-17%
	LP64	z3*	✅	3s	5s	-40%
poly_caddq_native	LP64	bitwuzla	✅	112s	135s	-17%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	33s	37s	-11%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	124s	146s	-15%
	LP64	z3*	✅	2s	3s	-33%
poly_challenge	LP64	bitwuzla	✅	34s	40s	-15%
	LP64	z3*	✅	1s	3s	-67%
poly_chknorm	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
poly_chknorm_c	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	7s	8s	-12%
poly_chknorm_native	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	5s	3s	+67%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_32_native_aarch64	LP64	cadical	✅	10s	14s	-29%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_c	LP64	z3*	✅	4s	5s	-20%
poly_decompose_native	LP64	cadical	✅	13s	16s	-19%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_native_x86_64	LP64	cadical	✅	10s	11s	-9%
	LP64	z3*	✅	2s	1s	+100%
poly_invntt_tomont	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	4s	3s	+33%
poly_invntt_tomont_c	LP64	bitwuzla	✅	139s	179s	-22%
	LP64	z3_smt_only*	✅	6s	9s	-33%
poly_invntt_tomont_native	LP64	bitwuzla	✅	43s	53s	-19%
	LP64	z3*	✅	2s	2s	+0%
poly_ntt	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_ntt_c	LP64	bitwuzla	✅	52s	57s	-9%
	LP64	z3_smt_only*	✅	10s	12s	-17%
poly_ntt_native	LP64	bitwuzla	✅	27s	32s	-16%
	LP64	z3*	✅	3s	2s	+50%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	5s	3s	+67%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	3s	-33%
poly_pointwise_montgomery	LP64	bitwuzla	✅	9s	12s	-25%
	LP64	z3*	✅	2s	2s	+0%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	175s	218s	-20%
	LP64	z3*	✅	75s	92s	-18%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	55s	55s	+0%
	LP64	z3*	✅	3s	4s	-25%
poly_power2round	LP64	bitwuzla	✅	290s	340s	-15%
	LP64	z3*	✅	5s	4s	+25%
poly_reduce	LP64	bitwuzla	✅	10s	11s	-9%
	LP64	z3*	✅	3s	1s	+200%
poly_shiftl	LP64	bitwuzla	✅	11s	14s	-21%
	LP64	z3*	✅	4s	2s	+100%
poly_sub	LP64	bitwuzla	✅	15s	19s	-21%
	LP64	z3*	✅	2s	4s	-50%
poly_uniform	LP64	bitwuzla	✅	152s	168s	-10%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_4x	LP64	z3*	✅	4s	6s	-33%
poly_uniform_eta	LP64	bitwuzla	✅	85s	95s	-11%
	LP64	z3*	✅	3s	4s	-25%
poly_uniform_eta_4x	LP64	z3*	✅	8s	7s	+14%
poly_uniform_gamma1	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
poly_uniform_gamma1_4x	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	4s	2s	+100%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	23s	24s	-4%
	LP64	z3*	✅	4s	2s	+100%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	10s	13s	-23%
	LP64	z3*	✅	1s	1s	+0%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	88s	89s	-1%
	LP64	z3*	✅	6s	3s	+100%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	29s	33s	-12%
	LP64	z3*	✅	5s	3s	+67%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	28s	32s	-12%
	LP64	z3*	✅	3s	2s	+50%
polyeta_pack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	1s	+0%
polyeta_unpack	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	9s	8s	+12%
polyt0_pack	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	3s	-33%
polyt0_unpack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	8s	7s	+14%
polyt1_pack	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyt1_unpack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	4s	2s	+100%
polyvec_matrix_expand_serial	LP64	z3*	✅	1s	2s	-50%
polyvec_matrix_pointwise_montgomery_row	LP64	z3_no_bv_extract*	✅	7s	5s	+40%
polyvec_matrix_pointwise_montgomery_yvec	LP64	z3*	✅	90s	101s	-11%
polyveck_caddq	LP64	z3*	✅	4s	5s	-20%
polyveck_decompose_pack_w1	LP64	z3*	✅	11s	16s	-31%
polyveck_invntt_tomont	LP64	z3*	✅	4s	6s	-33%
polyveck_ntt	LP64	z3*	✅	2s	2s	+0%
polyveck_reduce	LP64	z3*	✅	4s	6s	-33%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	17s	18s	-6%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_chknorm	LP64	z3*	✅	1s	3s	-67%
polyvecl_ntt	LP64	z3*	✅	4s	4s	+0%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery_c	LP64	z3*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	3s	3s	+0%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	49s	51s	-4%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	45s	46s	-2%
	LP64	z3*	✅	2s	3s	-33%
polyw1_pack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack_32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
polyw1_pack_88	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	3s	-67%
polyw1_unpack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
polyw1_unpack_88	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	1s	+200%
polyz_pack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	2s	-50%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	5s	-20%
polyz_unpack_c	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	6s	-50%
polyz_unpack_native	LP64	bitwuzla	✅	24s	30s	-20%
	LP64	z3*	✅	2s	1s	+100%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	15s	17s	-12%
	LP64	z3*	✅	3s	2s	+50%
power2round	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
reduce32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
rej_eta	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
rej_eta_c	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	21s	26s	-19%
rej_eta_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	11s	14s	-21%
rej_uniform	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	6s	6s	+0%
rej_uniform_c	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	8s	12s	-33%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	2s	4s	-50%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3_smt_only*	✅	3s	2s	+50%
rej_uniform_native	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	16s	20s	-20%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	3s	3s	+0%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3_smt_only*	✅	9s	14s	-36%
shake128_absorb	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
shake128_finalize	LP64	cvc5_arrays_exp	✅	1s	5s	-80%
	LP64	z3*	✅	1s	1s	+0%
shake128_init	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
shake128_release	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
shake128_squeeze	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
shake128x4_absorb_once	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	3s	-67%
shake256	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	3s	-67%
shake256_absorb	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake256_finalize	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake256_init	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	3s	+0%
shake256_release	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
shake256_squeeze	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
shake256x4_absorb_once	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	2s	+50%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
sig_unpack_hints	LP64	bitwuzla	✅	27s	31s	-13%
	LP64	z3*	✅	18s	21s	-14%
sign_keypair	LP64	z3*	✅	3s	6s	-50%
sign_keypair_internal	LP64	z3_no_bv_extract*	✅	25s	28s	-11%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	34s	38s	-11%
sign_signature	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
sign_signature_extmu	LP64	cadical	✅	76s	85s	-11%
	LP64	z3*	✅	3s	4s	-25%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	15s	18s	-17%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	6s	2s	+200%
sign_signature_pre_hash_shake256	LP64	bitwuzla	✅	1511s	1753s	-14%
	LP64	z3*	✅	5s	3s	+67%
sign_verify	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	2s	+50%
sign_verify_extmu	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	3s	+0%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	279s	317s	-12%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	5s	1s	+400%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	4s	2s	+100%
sk_s1hat_get_poly	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
sk_s2hat_get_poly	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
sk_t0hat_get_poly	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
sys_check_capability	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
unpack_pk_t1	LP64	bitwuzla	✅	11s	11s	+0%
	LP64	z3*	✅	1s	2s	-50%
unpack_sk	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	4s	1s	+300%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
unpack_sk_t0hat	LP64	z3*	✅	2s	4s	-50%
use_hint	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
yvec_get_poly	LP64	bitwuzla	✅	5s	7s	-29%
	LP64	z3*	✅	2s	1s	+100%
yvec_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%

[oqs-bot]

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

* default.

Full Results (415 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1412s	1411s	+0.1%
caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	31s	31s	+0%
decompose	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
fqmul	LP64	bitwuzla*	✅	24s	24s	+0%
	LP64	z3_smt_only	✅	21s	20s	+5%
fqscale	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
intt_native_aarch64	LP64	bitwuzla	✅	21s	21s	+0%
	LP64	z3*	✅	2s	3s	-33%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	10s	8s	+25%
	LP64	z3	✅	4s	2s	+100%
intt_native_rv32im_slowmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	2s	1s	+100%
intt_native_x86_64	LP64	bitwuzla	✅	17s	17s	+0%
	LP64	z3*	✅	3s	4s	-25%
keccak_absorb	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	cvc5_arrays_exp	✅	8s	7s	+14%
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	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	3s	1s	+200%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	1s	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	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
keccak_finalize	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	1s	+200%
keccak_init	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
keccak_squeeze	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	4s	-25%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	1s	+200%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
keccakf1600_permute	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
keccakf1600_permute_native	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	4s	-50%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	13s	12s	+8%
	LP64	z3*	✅	13s	11s	+18%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
make_hint	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	154s	154s	+0%
mld_check_pct	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	7s	5s	+40%
mld_compute_pack_z	LP64	cadical	✅	44s	42s	+5%
	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
mld_ct_abs_i32	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	1s	2s	-50%
	ILP32	z3	✅	3s	4s	-25%
	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	4s	1s	+300%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	73s	83s	-12%
mld_ct_sel_int32	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_h	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
mld_invntt_layer	LP64	bitwuzla*	✅	65s	64s	+2%
	LP64	z3_smt_only	✅	74s	71s	+4%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	5s	4s	+25%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	12s	14s	-14%
	LP64	z3_no_bv_extract	✅	97s	113s	-14%
mld_ntt_layer	LP64	bitwuzla*	✅	24s	25s	-4%
	LP64	z3_no_bv_extract	✅	2s	4s	-50%
mld_polymat_expand_entry	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	4s	+0%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
mld_sample_pack_s1_s2	LP64	cadical	✅	33s	36s	-8%
	LP64	z3*	✅	1s	2s	-50%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	89s	89s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
mld_sign_finish	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	1s	+200%
mld_sign_resume	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_value_barrier_i64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
mld_value_barrier_u32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
ntt_native_aarch64	LP64	bitwuzla	✅	18s	20s	-10%
	LP64	z3*	✅	3s	2s	+50%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	6s	6s	+0%
	LP64	z3	✅	2s	1s	+100%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	3s	5s	-40%
	LP64	cvc5_mbqi_enum	✅	6s	5s	+20%
	LP64	z3	✅	2s	3s	-33%
ntt_native_x86_64	LP64	bitwuzla	✅	16s	18s	-11%
	LP64	z3*	✅	3s	1s	+200%
nttunpack_native_x86_64	LP64	bitwuzla	✅	149s	183s	-19%
	LP64	z3*	✅	2s	3s	-33%
pack_sig_c	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
pack_sig_h	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
pack_sig_z	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
pointwise_acc_native_aarch64	LP64	z3_smt_only*	✅	3s	3s	+0%
pointwise_acc_native_x86_64	LP64	cadical	✅	66s	66s	+0%
	LP64	z3_smt_only*	✅	4s	3s	+33%
pointwise_native_aarch64	LP64	bitwuzla	✅	21s	22s	-5%
	LP64	z3*	✅	4s	4s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	4s	2s	+100%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	1s	1s	+0%
pointwise_native_x86_64	LP64	bitwuzla	✅	21s	23s	-9%
	LP64	z3*	✅	2s	3s	-33%
poly_add	LP64	z3*	✅	3s	5s	-40%
poly_caddq	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
poly_caddq_c	LP64	bitwuzla	✅	20s	20s	+0%
	LP64	z3*	✅	4s	3s	+33%
poly_caddq_native	LP64	bitwuzla	✅	109s	111s	-2%
	LP64	z3*	✅	3s	3s	+0%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	33s	33s	+0%
	LP64	z3*	✅	2s	1s	+100%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	122s	121s	+1%
	LP64	z3*	✅	1s	1s	+0%
poly_challenge	LP64	bitwuzla	✅	23s	22s	+5%
	LP64	z3*	✅	3s	3s	+0%
poly_chknorm	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_c	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	5s	7s	-29%
poly_chknorm_native	LP64	bitwuzla	✅	5s	7s	-29%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
poly_decompose	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_32_native_aarch64	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	4s	4s	+0%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	1s	3s	-67%
poly_decompose_c	LP64	z3*	✅	5s	4s	+25%
poly_decompose_native	LP64	cadical	✅	16s	16s	+0%
	LP64	z3*	✅	4s	2s	+100%
poly_decompose_native_x86_64	LP64	cadical	✅	11s	14s	-21%
	LP64	z3*	✅	2s	1s	+100%
poly_invntt_tomont	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	4s	3s	+33%
poly_invntt_tomont_c	LP64	bitwuzla	✅	154s	158s	-3%
	LP64	z3_smt_only*	✅	6s	6s	+0%
poly_invntt_tomont_native	LP64	bitwuzla	✅	42s	42s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_ntt	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	4s	+0%
poly_ntt_c	LP64	bitwuzla	✅	50s	44s	+14%
	LP64	z3_smt_only*	✅	9s	10s	-10%
poly_ntt_native	LP64	bitwuzla	✅	28s	26s	+8%
	LP64	z3*	✅	2s	2s	+0%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
poly_pointwise_montgomery	LP64	bitwuzla	✅	10s	12s	-17%
	LP64	z3*	✅	3s	1s	+200%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	186s	188s	-1%
	LP64	z3*	✅	77s	73s	+5%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	56s	54s	+4%
	LP64	z3*	✅	3s	2s	+50%
poly_power2round	LP64	bitwuzla	✅	284s	298s	-5%
	LP64	z3*	✅	5s	4s	+25%
poly_reduce	LP64	bitwuzla	✅	11s	8s	+38%
	LP64	z3*	✅	2s	2s	+0%
poly_shiftl	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	3s	2s	+50%
poly_sub	LP64	bitwuzla	✅	14s	15s	-7%
	LP64	z3*	✅	1s	2s	-50%
poly_uniform	LP64	bitwuzla	✅	133s	148s	-10%
	LP64	z3*	✅	5s	5s	+0%
poly_uniform_4x	LP64	z3*	✅	2s	2s	+0%
poly_uniform_eta	LP64	bitwuzla	✅	81s	77s	+5%
	LP64	z3*	✅	3s	2s	+50%
poly_uniform_eta_4x	LP64	z3*	✅	8s	6s	+33%
poly_uniform_gamma1	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
poly_uniform_gamma1_4x	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	22s	25s	-12%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	11s	9s	+22%
	LP64	z3*	✅	3s	1s	+200%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	84s	83s	+1%
	LP64	z3*	✅	2s	4s	-50%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	33s	34s	-3%
	LP64	z3*	✅	2s	1s	+100%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	30s	32s	-6%
	LP64	z3*	✅	1s	4s	-75%
polyeta_pack	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	4s	-50%
polyeta_unpack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	7s	8s	-12%
polyt0_pack	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	2s	-50%
polyt0_unpack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	10s	7s	+43%
polyt1_pack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
polyt1_unpack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	2s	1s	+100%
polyvec_matrix_expand_serial	LP64	z3*	✅	1s	3s	-67%
polyvec_matrix_pointwise_montgomery_row	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
polyvec_matrix_pointwise_montgomery_yvec	LP64	z3*	✅	127s	126s	+1%
polyveck_caddq	LP64	z3*	✅	2s	3s	-33%
polyveck_decompose_pack_w1	LP64	z3*	✅	6s	7s	-14%
polyveck_invntt_tomont	LP64	z3*	✅	2s	2s	+0%
polyveck_ntt	LP64	z3*	✅	3s	1s	+200%
polyveck_reduce	LP64	z3*	✅	2s	3s	-33%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	17s	20s	-15%
	LP64	z3*	✅	3s	1s	+200%
polyvecl_chknorm	LP64	z3*	✅	5s	4s	+25%
polyvecl_ntt	LP64	z3*	✅	4s	4s	+0%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	4s	2s	+100%
	LP64	z3_smt_only*	✅	3s	2s	+50%
polyvecl_pointwise_acc_montgomery_c	LP64	z3*	✅	2s	1s	+100%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	1s	3s	-67%
	LP64	z3_smt_only*	✅	1s	3s	-67%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	33s	31s	+6%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	24s	27s	-11%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	1s	+0%
polyw1_pack_32	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	5s	4s	+25%
polyw1_pack_88	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	1s	+300%
polyw1_unpack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
polyw1_unpack_88	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	4s	-50%
polyz_pack	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	4s	-50%
polyz_unpack	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_c	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	7s	6s	+17%
polyz_unpack_native	LP64	bitwuzla	✅	25s	26s	-4%
	LP64	z3*	✅	1s	4s	-75%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	16s	15s	+7%
	LP64	z3*	✅	1s	2s	-50%
power2round	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
reduce32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
rej_eta	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	3s	4s	-25%
rej_eta_c	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	22s	20s	+10%
rej_eta_native	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	11s	12s	-8%
rej_uniform	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	6s	-50%
rej_uniform_c	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	9s	9s	+0%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	1s	3s	-67%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_smt_only*	✅	3s	2s	+50%
rej_uniform_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	19s	17s	+12%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_smt_only*	✅	7s	9s	-22%
shake128_absorb	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
shake128_finalize	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
shake128_init	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	3s	-33%
shake128_release	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
shake128_squeeze	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
shake128x4_absorb_once	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	5s	-60%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	4s	2s	+100%
shake256	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
shake256_absorb	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake256_finalize	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
shake256_init	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake256_release	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	1s	+100%
shake256_squeeze	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
shake256x4_absorb_once	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	3s	-33%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	3s	+0%
sig_unpack_hints	LP64	bitwuzla	✅	49s	51s	-4%
	LP64	z3*	✅	33s	36s	-8%
sign_keypair	LP64	z3*	✅	6s	6s	+0%
sign_keypair_internal	LP64	z3_no_bv_extract*	✅	10s	12s	-17%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	29s	28s	+4%
sign_signature	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
sign_signature_extmu	LP64	cadical	✅	23s	23s	+0%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	14s	14s	+0%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	6s	3s	+100%
sign_signature_pre_hash_shake256	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	4s	6s	-33%
sign_verify	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
sign_verify_extmu	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	3s	+33%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	269s	273s	-1%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	1s	+100%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	3s	+0%
sk_s1hat_get_poly	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
sk_s2hat_get_poly	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
sk_t0hat_get_poly	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
sys_check_capability	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
unpack_pk_t1	LP64	bitwuzla	✅	9s	10s	-10%
	LP64	z3*	✅	2s	3s	-33%
unpack_sk	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
unpack_sk_t0hat	LP64	z3*	✅	1s	2s	-50%
use_hint	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	5s	-60%
yvec_get_poly	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	4s	-25%
yvec_init	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%

[oqs-bot]

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
poly_caddq_c	LP64	bitwuzla	⚠️	24s	16s	+50%

Full Results (415 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	2360s	2136s	+10.5%
caddq	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	105s	97s	+8%
decompose	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
fqmul	LP64	bitwuzla*	✅	26s	24s	+8%
	LP64	z3_smt_only	✅	20s	20s	+0%
fqscale	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
intt_native_aarch64	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	5s	2s	+150%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	2s	2s	+0%
intt_native_rv32im_slowmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	9s	+0%
	LP64	z3	✅	3s	3s	+0%
intt_native_x86_64	LP64	bitwuzla	✅	20s	18s	+11%
	LP64	z3*	✅	2s	2s	+0%
keccak_absorb	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	5s	4s	+25%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	7s	6s	+17%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	4s	2s	+100%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
keccak_finalize	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
keccak_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
keccak_squeeze	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	4s	-25%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	2s	1s	+100%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	4s	-50%
keccakf1600_permute	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute_native	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	1s	+100%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	1s	1s	+0%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	13s	14s	-7%
	LP64	z3*	✅	12s	12s	+0%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
make_hint	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	5s	2s	+150%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	447s	359s	+25%
mld_check_pct	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	6s	-50%
mld_compute_pack_z	LP64	cadical	✅	80s	76s	+5%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
mld_ct_abs_i32	ILP32	bitwuzla	✅	1s	3s	-67%
	ILP32	cvc5_arrays_exp	✅	3s	1s	+200%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	3s	+33%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	2s	6s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	100s	89s	+12%
mld_ct_sel_int32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
mld_h	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
mld_invntt_layer	LP64	bitwuzla*	✅	76s	71s	+7%
	LP64	z3_smt_only	✅	106s	93s	+14%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	3s	-33%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	4s	6s	-33%
	LP64	z3*	✅	3s	4s	-25%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	15s	12s	+25%
	LP64	z3_no_bv_extract	✅	192s	161s	+19%
mld_ntt_layer	LP64	bitwuzla*	✅	28s	25s	+12%
	LP64	z3_no_bv_extract	✅	4s	2s	+100%
mld_polymat_expand_entry	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	3s	-67%
mld_sample_pack_s1_s2	LP64	cadical	✅	37s	35s	+6%
	LP64	z3*	✅	2s	2s	+0%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	97s	89s	+9%
	LP64	z3*	✅	2s	3s	-33%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_sign_finish	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	5s	-60%
mld_sign_resume	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	4s	+0%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	4s	-50%
mld_value_barrier_u32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	5s	-80%
ntt_native_aarch64	LP64	bitwuzla	✅	21s	21s	+0%
	LP64	z3*	✅	4s	5s	-20%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	2s	4s	-50%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	1s	2s	-50%
ntt_native_x86_64	LP64	bitwuzla	✅	21s	20s	+5%
	LP64	z3*	✅	2s	3s	-33%
nttunpack_native_x86_64	LP64	bitwuzla	✅	223s	194s	+15%
	LP64	z3*	✅	2s	1s	+100%
pack_sig_c	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
pack_sig_h	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
pack_sig_z	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	4s	2s	+100%
pointwise_acc_native_aarch64	LP64	z3_smt_only*	✅	4s	3s	+33%
pointwise_acc_native_x86_64	LP64	cadical	✅	74s	62s	+19%
	LP64	z3_smt_only*	✅	3s	6s	-50%
pointwise_native_aarch64	LP64	bitwuzla	✅	24s	23s	+4%
	LP64	z3*	✅	3s	2s	+50%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	5s	2s	+150%
	LP64	cvc5_mbqi_enum	✅	10s	10s	+0%
	LP64	z3	✅	4s	2s	+100%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	9s	+0%
	LP64	z3	✅	1s	2s	-50%
pointwise_native_x86_64	LP64	bitwuzla	✅	25s	25s	+0%
	LP64	z3*	✅	2s	3s	-33%
poly_add	LP64	z3*	✅	5s	4s	+25%
poly_caddq	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
poly_caddq_c	LP64	bitwuzla	⚠️	24s	16s	+50%
	LP64	z3*	✅	3s	3s	+0%
poly_caddq_native	LP64	bitwuzla	✅	124s	114s	+9%
	LP64	z3*	✅	3s	3s	+0%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	37s	38s	-3%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	155s	129s	+20%
	LP64	z3*	✅	2s	3s	-33%
poly_challenge	LP64	bitwuzla	✅	29s	27s	+7%
	LP64	z3*	✅	7s	4s	+75%
poly_chknorm	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	5s	-60%
poly_chknorm_c	LP64	bitwuzla	✅	11s	10s	+10%
	LP64	z3*	✅	7s	6s	+17%
poly_chknorm_native	LP64	bitwuzla	✅	8s	7s	+14%
	LP64	z3*	✅	1s	3s	-67%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
poly_decompose	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	2s	4s	-50%
poly_decompose_c	LP64	z3*	✅	3s	5s	-40%
poly_decompose_native	LP64	cadical	✅	20s	17s	+18%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_native_x86_64	LP64	cadical	✅	14s	12s	+17%
	LP64	z3*	✅	2s	2s	+0%
poly_invntt_tomont	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
poly_invntt_tomont_c	LP64	bitwuzla	✅	186s	170s	+9%
	LP64	z3_smt_only*	✅	8s	6s	+33%
poly_invntt_tomont_native	LP64	bitwuzla	✅	54s	48s	+12%
	LP64	z3*	✅	1s	2s	-50%
poly_ntt	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	3s	-67%
poly_ntt_c	LP64	bitwuzla	✅	62s	55s	+13%
	LP64	z3_smt_only*	✅	12s	10s	+20%
poly_ntt_native	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	3s	2s	+50%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	4s	-75%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	2s	+150%
poly_pointwise_montgomery	LP64	bitwuzla	✅	13s	10s	+30%
	LP64	z3*	✅	1s	2s	-50%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	216s	201s	+7%
	LP64	z3*	✅	61s	48s	+27%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	57s	54s	+6%
	LP64	z3*	✅	1s	3s	-67%
poly_power2round	LP64	bitwuzla	✅	397s	336s	+18%
	LP64	z3*	✅	2s	4s	-50%
poly_reduce	LP64	bitwuzla	✅	10s	11s	-9%
	LP64	z3*	✅	1s	2s	-50%
poly_shiftl	LP64	bitwuzla	✅	13s	12s	+8%
	LP64	z3*	✅	3s	2s	+50%
poly_sub	LP64	bitwuzla	✅	18s	13s	+38%
	LP64	z3*	✅	3s	4s	-25%
poly_uniform	LP64	bitwuzla	✅	178s	128s	+39%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_4x	LP64	z3*	✅	10s	7s	+43%
poly_uniform_eta	LP64	bitwuzla	✅	97s	84s	+15%
	LP64	z3*	✅	4s	2s	+100%
poly_uniform_eta_4x	LP64	z3*	✅	10s	10s	+0%
poly_uniform_gamma1	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	15s	14s	+7%
	LP64	z3*	✅	3s	5s	-40%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	24s	23s	+4%
	LP64	z3*	✅	4s	2s	+100%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	13s	11s	+18%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	78s	86s	-9%
	LP64	z3*	✅	3s	2s	+50%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	37s	38s	-3%
	LP64	z3*	✅	3s	2s	+50%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	38s	35s	+9%
	LP64	z3*	✅	2s	1s	+100%
polyeta_pack	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyeta_unpack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	7s	4s	+75%
polyt0_pack	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
polyt0_unpack	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	9s	7s	+29%
polyt1_pack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	2s	+150%
polyt1_unpack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	18s	15s	+20%
polyvec_matrix_expand_serial	LP64	z3*	✅	5s	4s	+25%
polyvec_matrix_pointwise_montgomery_row	LP64	z3_no_bv_extract*	✅	4s	3s	+33%
polyvec_matrix_pointwise_montgomery_yvec	LP64	z3*	✅	12s	11s	+9%
polyveck_caddq	LP64	z3*	✅	1s	2s	-50%
polyveck_decompose_pack_w1	LP64	z3*	✅	3s	3s	+0%
polyveck_invntt_tomont	LP64	z3*	✅	2s	2s	+0%
polyveck_ntt	LP64	z3*	✅	1s	2s	-50%
polyveck_reduce	LP64	z3*	✅	3s	3s	+0%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	28s	29s	-3%
	LP64	z3*	✅	2s	2s	+0%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	17s	17s	+0%
	LP64	z3*	✅	3s	1s	+200%
polyvecl_chknorm	LP64	z3*	✅	3s	4s	-25%
polyvecl_ntt	LP64	z3*	✅	5s	2s	+150%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	5s	6s	-17%
	LP64	z3_smt_only*	✅	3s	2s	+50%
polyvecl_pointwise_acc_montgomery_c	LP64	z3*	✅	203s	176s	+15%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	167s	158s	+6%
	LP64	z3_smt_only*	✅	2s	3s	-33%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	41s	37s	+11%
	LP64	z3*	✅	1s	3s	-67%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	42s	41s	+2%
	LP64	z3*	✅	2s	1s	+100%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	33s	32s	+3%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	28s	27s	+4%
	LP64	z3*	✅	4s	1s	+300%
polyw1_pack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
polyw1_pack_32	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
polyw1_pack_88	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
polyw1_unpack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	4s	-50%
polyz_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	2s	-50%
polyz_unpack	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	4s	2s	+100%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	5s	2s	+150%
polyz_unpack_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	7s	-43%
polyz_unpack_native	LP64	bitwuzla	✅	30s	27s	+11%
	LP64	z3*	✅	2s	4s	-50%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	19s	17s	+12%
	LP64	z3*	✅	2s	3s	-33%
power2round	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	4s	-75%
reduce32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
rej_eta	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	4s	3s	+33%
rej_eta_c	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	21s	19s	+11%
rej_eta_native	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	16s	11s	+45%
rej_uniform	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	14s	14s	+0%
rej_uniform_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	12s	10s	+20%
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	✅	1s	2s	-50%
	LP64	z3_smt_only*	✅	3s	3s	+0%
rej_uniform_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	19s	19s	+0%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	2s	+0%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_smt_only*	✅	10s	8s	+25%
shake128_absorb	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
shake128_finalize	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
shake128_init	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
shake128_release	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
shake128_squeeze	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
shake128x4_absorb_once	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	2s	-50%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	1s	+100%
shake256	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake256_absorb	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	3s	+0%
shake256_finalize	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
shake256_init	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
shake256_release	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
shake256_squeeze	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
shake256x4_absorb_once	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	1s	+100%
sig_unpack_hints	LP64	bitwuzla	✅	66s	57s	+16%
	LP64	z3*	✅	29s	25s	+16%
sign_keypair	LP64	z3*	✅	5s	3s	+67%
sign_keypair_internal	LP64	z3_no_bv_extract*	✅	17s	16s	+6%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	38s	32s	+19%
sign_signature	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	5s	-20%
sign_signature_extmu	LP64	cadical	✅	26s	25s	+4%
	LP64	z3*	✅	3s	2s	+50%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	284s	257s	+11%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_pre_hash_shake256	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	4s	+0%
sign_verify	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	2s	+100%
sign_verify_extmu	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	414s	378s	+10%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	2s	+100%
sk_s1hat_get_poly	LP64	bitwuzla	✅	32s	30s	+7%
	LP64	z3*	✅	1s	3s	-67%
sk_s2hat_get_poly	LP64	bitwuzla	✅	34s	30s	+13%
	LP64	z3*	✅	2s	3s	-33%
sk_t0hat_get_poly	LP64	bitwuzla	✅	32s	30s	+7%
	LP64	z3*	✅	2s	1s	+100%
sys_check_capability	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
unpack_pk_t1	LP64	bitwuzla	✅	13s	11s	+18%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk	LP64	cadical	✅	43s	42s	+2%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	269s	256s	+5%
	LP64	z3*	✅	3s	3s	+0%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	271s	258s	+5%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk_t0hat	LP64	z3*	✅	2s	2s	+0%
use_hint	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
yvec_get_poly	LP64	bitwuzla	✅	35s	31s	+13%
	LP64	z3*	✅	2s	3s	-33%
yvec_init	LP64	bitwuzla	✅	44s	40s	+10%
	LP64	z3*	✅	2s	2s	+0%

[oqs-bot]

CBMC Results (ML-DSA-65)

* default.

Full Results (415 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	2153s	2276s	-5.4%
caddq	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	146s	160s	-9%
decompose	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
fqmul	LP64	bitwuzla*	✅	25s	25s	+0%
	LP64	z3_smt_only	✅	21s	19s	+11%
fqscale	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	5s	1s	+400%
intt_native_aarch64	LP64	bitwuzla	✅	24s	25s	-4%
	LP64	z3*	✅	1s	2s	-50%
intt_native_rv32im_fastmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	4s	2s	+100%
intt_native_rv32im_slowmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	2s	2s	+0%
intt_native_x86_64	LP64	bitwuzla	✅	17s	18s	-6%
	LP64	z3*	✅	2s	3s	-33%
keccak_absorb	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	6s	4s	+50%
	LP64	cvc5_arrays_exp	✅	7s	10s	-30%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	✅	3s	2s	+50%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
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*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	2s	+0%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
keccak_finalize	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
keccak_init	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
keccak_squeeze	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	4s	-25%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
keccakf1600_permute_native	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	2s	+50%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	13s	12s	+8%
	LP64	z3*	✅	13s	11s	+18%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
make_hint	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	227s	241s	-6%
mld_check_pct	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	4s	5s	-20%
mld_compute_pack_z	LP64	cadical	✅	79s	87s	-9%
	LP64	z3_no_bv_extract*	✅	5s	5s	+0%
mld_ct_abs_i32	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	3s	2s	+50%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
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	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
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	✅	80s	98s	-18%
mld_ct_sel_int32	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
mld_h	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	4s	-50%
mld_invntt_layer	LP64	bitwuzla*	✅	63s	73s	-14%
	LP64	z3_smt_only	✅	93s	102s	-9%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	4s	3s	+33%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	11s	12s	-8%
	LP64	z3_no_bv_extract	✅	172s	181s	-5%
mld_ntt_layer	LP64	bitwuzla*	✅	25s	26s	-4%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
mld_polymat_expand_entry	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	3s	+33%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	6s	4s	+50%
mld_sample_pack_s1_s2	LP64	cadical	✅	54s	57s	-5%
	LP64	z3*	✅	4s	4s	+0%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	232s	240s	-3%
	LP64	z3*	✅	2s	3s	-33%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	3s	1s	+200%
mld_sign_finish	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
mld_sign_resume	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	5s	-60%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
mld_value_barrier_u32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	4s	-25%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	2s	2s	+0%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	4s	-25%
ntt_native_aarch64	LP64	bitwuzla	✅	19s	24s	-21%
	LP64	z3*	✅	3s	4s	-25%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	5s	5s	+0%
	LP64	z3	✅	3s	3s	+0%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	3s	-33%
ntt_native_x86_64	LP64	bitwuzla	✅	19s	20s	-5%
	LP64	z3*	✅	3s	2s	+50%
nttunpack_native_x86_64	LP64	bitwuzla	✅	194s	206s	-6%
	LP64	z3*	✅	2s	2s	+0%
pack_sig_c	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
pack_sig_h	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
pack_sig_z	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	5s	-40%
pointwise_acc_native_aarch64	LP64	z3_smt_only*	✅	4s	3s	+33%
pointwise_acc_native_x86_64	LP64	cadical	✅	89s	97s	-8%
	LP64	z3_smt_only*	✅	4s	5s	-20%
pointwise_native_aarch64	LP64	bitwuzla	✅	23s	26s	-12%
	LP64	z3*	✅	2s	2s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	2s	1s	+100%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	3s	2s	+50%
pointwise_native_x86_64	LP64	bitwuzla	✅	23s	23s	+0%
	LP64	z3*	✅	4s	5s	-20%
poly_add	LP64	z3*	✅	5s	5s	+0%
poly_caddq	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
poly_caddq_c	LP64	bitwuzla	✅	21s	20s	+5%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native	LP64	bitwuzla	✅	114s	127s	-10%
	LP64	z3*	✅	4s	2s	+100%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	35s	37s	-5%
	LP64	z3*	✅	4s	3s	+33%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	122s	138s	-12%
	LP64	z3*	✅	5s	2s	+150%
poly_challenge	LP64	bitwuzla	✅	23s	27s	-15%
	LP64	z3*	✅	5s	2s	+150%
poly_chknorm	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	3s	-33%
poly_chknorm_c	LP64	bitwuzla	✅	11s	10s	+10%
	LP64	z3*	✅	6s	7s	-14%
poly_chknorm_native	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	3s	2s	+50%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	8s	8s	+0%
	LP64	z3*	✅	4s	5s	-20%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_c	LP64	z3*	✅	4s	2s	+100%
poly_decompose_native	LP64	cadical	✅	14s	14s	+0%
	LP64	z3*	✅	1s	3s	-67%
poly_decompose_native_x86_64	LP64	cadical	✅	9s	11s	-18%
	LP64	z3*	✅	2s	2s	+0%
poly_invntt_tomont	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	4s	3s	+33%
poly_invntt_tomont_c	LP64	bitwuzla	✅	159s	179s	-11%
	LP64	z3_smt_only*	✅	6s	7s	-14%
poly_invntt_tomont_native	LP64	bitwuzla	✅	44s	52s	-15%
	LP64	z3*	✅	3s	3s	+0%
poly_ntt	LP64	bitwuzla	✅	5s	7s	-29%
	LP64	z3*	✅	1s	1s	+0%
poly_ntt_c	LP64	bitwuzla	✅	48s	55s	-13%
	LP64	z3_smt_only*	✅	10s	12s	-17%
poly_ntt_native	LP64	bitwuzla	✅	26s	28s	-7%
	LP64	z3*	✅	3s	3s	+0%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
poly_pointwise_montgomery	LP64	bitwuzla	✅	8s	12s	-33%
	LP64	z3*	✅	1s	2s	-50%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	193s	210s	-8%
	LP64	z3*	✅	51s	57s	-11%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	57s	57s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_power2round	LP64	bitwuzla	✅	332s	353s	-6%
	LP64	z3*	✅	4s	2s	+100%
poly_reduce	LP64	bitwuzla	✅	7s	9s	-22%
	LP64	z3*	✅	2s	2s	+0%
poly_shiftl	LP64	bitwuzla	✅	9s	13s	-31%
	LP64	z3*	✅	3s	3s	+0%
poly_sub	LP64	bitwuzla	✅	15s	17s	-12%
	LP64	z3*	✅	2s	3s	-33%
poly_uniform	LP64	bitwuzla	✅	133s	166s	-20%
	LP64	z3*	✅	1s	3s	-67%
poly_uniform_4x	LP64	z3*	✅	6s	7s	-14%
poly_uniform_eta	LP64	bitwuzla	✅	148s	148s	+0%
	LP64	z3*	✅	3s	1s	+200%
poly_uniform_eta_4x	LP64	z3*	✅	8s	9s	-11%
poly_uniform_gamma1	LP64	cadical	✅	6s	3s	+100%
	LP64	z3*	✅	3s	3s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	12s	14s	-14%
	LP64	z3*	✅	2s	1s	+100%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	26s	23s	+13%
	LP64	z3*	✅	2s	4s	-50%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	14s	13s	+8%
	LP64	z3*	✅	4s	3s	+33%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	92s	93s	-1%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	31s	32s	-3%
	LP64	z3*	✅	3s	3s	+0%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	28s	33s	-15%
	LP64	z3*	✅	4s	1s	+300%
polyeta_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
polyeta_unpack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
polyt0_pack	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	2s	1s	+100%
polyt0_unpack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	6s	9s	-33%
polyt1_pack	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
polyt1_unpack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	82s	86s	-5%
polyvec_matrix_expand_serial	LP64	z3*	✅	15s	16s	-6%
polyvec_matrix_pointwise_montgomery_row	LP64	z3_no_bv_extract*	✅	1s	2s	-50%
polyvec_matrix_pointwise_montgomery_yvec	LP64	z3*	✅	18s	21s	-14%
polyveck_caddq	LP64	z3*	✅	5s	5s	+0%
polyveck_decompose_pack_w1	LP64	z3*	✅	7s	7s	+0%
polyveck_invntt_tomont	LP64	z3*	✅	3s	5s	-40%
polyveck_ntt	LP64	z3*	✅	4s	5s	-20%
polyveck_reduce	LP64	z3*	✅	3s	1s	+200%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	42s	39s	+8%
	LP64	z3*	✅	3s	2s	+50%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	19s	19s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyvecl_chknorm	LP64	z3*	✅	3s	3s	+0%
polyvecl_ntt	LP64	z3*	✅	4s	3s	+33%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	11s	11s	+0%
	LP64	z3_smt_only*	✅	3s	2s	+50%
polyvecl_pointwise_acc_montgomery_c	LP64	z3*	✅	130s	142s	-8%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	118s	114s	+4%
	LP64	z3_smt_only*	✅	1s	2s	-50%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	33s	36s	-8%
	LP64	z3*	✅	3s	3s	+0%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	36s	35s	+3%
	LP64	z3*	✅	1s	3s	-67%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	35s	36s	-3%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	36s	35s	+3%
	LP64	z3*	✅	1s	2s	-50%
polyw1_pack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
polyw1_pack_32	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	5s	2s	+150%
polyw1_pack_88	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyw1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	1s	+300%
polyw1_unpack_88	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
polyz_pack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	1s	+0%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_c	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	4s	-50%
polyz_unpack_native	LP64	bitwuzla	✅	25s	27s	-7%
	LP64	z3*	✅	3s	3s	+0%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	19s	18s	+6%
	LP64	z3*	✅	3s	3s	+0%
power2round	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
reduce32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
rej_eta	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
rej_eta_c	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	12s	13s	-8%
rej_eta_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	10s	12s	-17%
rej_uniform	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	12s	15s	-20%
rej_uniform_c	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	10s	11s	-9%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	3s	2s	+50%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3_smt_only*	✅	2s	3s	-33%
rej_uniform_native	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	19s	20s	-5%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	3s	3s	+0%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3_smt_only*	✅	10s	10s	+0%
shake128_absorb	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
shake128_finalize	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake128_init	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
shake128_release	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	2s	+100%
shake128_squeeze	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
shake128x4_absorb_once	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	1s	+0%
shake256	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
shake256_absorb	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
shake256_finalize	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
shake256_init	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
shake256_release	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
shake256_squeeze	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	3s	-33%
shake256x4_absorb_once	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
sig_unpack_hints	LP64	bitwuzla	✅	1364s	1493s	-9%
	LP64	z3*	✅	17s	18s	-6%
sign_keypair	LP64	z3*	✅	7s	5s	+40%
sign_keypair_internal	LP64	z3_no_bv_extract*	✅	19s	20s	-5%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	38s	39s	-3%
sign_signature	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_extmu	LP64	cadical	✅	35s	37s	-5%
	LP64	z3*	✅	4s	4s	+0%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	209s	231s	-10%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	4s	-50%
sign_signature_pre_hash_shake256	LP64	bitwuzla	✅	420s	371s	+13%
	LP64	z3*	✅	3s	4s	-25%
sign_verify	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
sign_verify_extmu	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	4s	-50%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	490s	523s	-6%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	5s	-20%
sk_s1hat_get_poly	LP64	bitwuzla	✅	36s	40s	-10%
	LP64	z3*	✅	2s	3s	-33%
sk_s2hat_get_poly	LP64	bitwuzla	✅	30s	33s	-9%
	LP64	z3*	✅	1s	2s	-50%
sk_t0hat_get_poly	LP64	bitwuzla	✅	30s	31s	-3%
	LP64	z3*	✅	2s	2s	+0%
sys_check_capability	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
unpack_pk_t1	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	3s	5s	-40%
unpack_sk	LP64	cadical	✅	57s	58s	-2%
	LP64	z3*	✅	1s	1s	+0%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	85s	90s	-6%
	LP64	z3*	✅	4s	3s	+33%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	161s	153s	+5%
	LP64	z3*	✅	3s	4s	-25%
unpack_sk_t0hat	LP64	z3*	✅	3s	5s	-40%
use_hint	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
yvec_get_poly	LP64	bitwuzla	✅	35s	34s	+3%
	LP64	z3*	✅	2s	2s	+0%
yvec_init	LP64	bitwuzla	✅	8s	10s	-20%
	LP64	z3*	✅	2s	2s	+0%

[oqs-bot]

CBMC Results (ML-DSA-87)

* default.

Full Results (415 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	3675s	3221s	+14.1%
caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	269s	231s	+16%
decompose	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	4s	3s	+33%
fqmul	LP64	bitwuzla*	✅	26s	22s	+18%
	LP64	z3_smt_only	✅	22s	21s	+5%
fqscale	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
intt_native_aarch64	LP64	bitwuzla	✅	24s	23s	+4%
	LP64	z3*	✅	2s	2s	+0%
intt_native_rv32im_fastmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	10s	8s	+25%
	LP64	z3	✅	5s	2s	+150%
intt_native_rv32im_slowmul	ILP32	z3*	✅	5s	1s	+400%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	4s	2s	+100%
intt_native_x86_64	LP64	bitwuzla	✅	19s	19s	+0%
	LP64	z3*	✅	2s	4s	-50%
keccak_absorb	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	6s	4s	+50%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	7s	8s	-12%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	1s	1s	+0%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	4s	+0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	3s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	1s	3s	-67%
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	4s	-50%
keccak_init	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
keccak_squeeze	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	1s	+200%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	6s	2s	+200%
	LP64	z3	✅	3s	4s	-25%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute_native	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	4s	-50%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	3s	3s	+0%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	3s	1s	+200%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	14s	11s	+27%
	LP64	z3*	✅	13s	13s	+0%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	4s	1s	+300%
make_hint	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	4s	-75%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	365s	290s	+26%
mld_check_pct	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	4s	5s	-20%
mld_compute_pack_z	LP64	cadical	✅	99s	97s	+2%
	LP64	z3_no_bv_extract*	✅	6s	4s	+50%
mld_ct_abs_i32	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	4s	4s	+0%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	3s	3s	+0%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	3s	-33%
mld_ct_memcmp	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	z3_no_bv_extract	✅	95s	81s	+17%
mld_ct_sel_int32	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	3s	-33%
mld_h	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
mld_invntt_layer	LP64	bitwuzla*	✅	68s	64s	+6%
	LP64	z3_smt_only	✅	97s	93s	+4%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	1s	+300%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	4s	6s	-33%
	LP64	z3*	✅	4s	2s	+100%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	14s	12s	+17%
	LP64	z3_no_bv_extract	✅	176s	156s	+13%
mld_ntt_layer	LP64	bitwuzla*	✅	29s	25s	+16%
	LP64	z3_no_bv_extract	✅	3s	2s	+50%
mld_polymat_expand_entry	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
mld_sample_pack_s1_s2	LP64	cadical	✅	93s	85s	+9%
	LP64	z3*	✅	9s	8s	+12%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	565s	555s	+2%
	LP64	z3*	✅	7s	6s	+17%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
mld_sign_finish	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	1s	+300%
mld_sign_resume	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	2s	+200%
mld_value_barrier_i64	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
mld_value_barrier_u32	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	3s	-67%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	2s	3s	-33%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
ntt_native_aarch64	LP64	bitwuzla	✅	25s	19s	+32%
	LP64	z3*	✅	3s	2s	+50%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	3s	-33%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	5s	6s	-17%
	LP64	z3	✅	2s	3s	-33%
ntt_native_x86_64	LP64	bitwuzla	✅	19s	16s	+19%
	LP64	z3*	✅	3s	3s	+0%
nttunpack_native_x86_64	LP64	bitwuzla	✅	198s	177s	+12%
	LP64	z3*	✅	3s	4s	-25%
pack_sig_c	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
pack_sig_h	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_no_bv_extract*	✅	5s	4s	+25%
pack_sig_z	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
pointwise_acc_native_aarch64	LP64	z3_smt_only*	✅	4s	5s	-20%
pointwise_acc_native_x86_64	LP64	cadical	✅	114s	102s	+12%
	LP64	z3_smt_only*	✅	5s	4s	+25%
pointwise_native_aarch64	LP64	bitwuzla	✅	24s	21s	+14%
	LP64	z3*	✅	2s	2s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	2s	3s	-33%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	5s	+60%
	LP64	z3	✅	5s	2s	+150%
pointwise_native_x86_64	LP64	bitwuzla	✅	22s	21s	+5%
	LP64	z3*	✅	2s	3s	-33%
poly_add	LP64	z3*	✅	3s	3s	+0%
poly_caddq	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_c	LP64	bitwuzla	✅	24s	18s	+33%
	LP64	z3*	✅	3s	2s	+50%
poly_caddq_native	LP64	bitwuzla	✅	111s	107s	+4%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	38s	34s	+12%
	LP64	z3*	✅	3s	1s	+200%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	133s	119s	+12%
	LP64	z3*	✅	2s	4s	-50%
poly_challenge	LP64	bitwuzla	✅	38s	32s	+19%
	LP64	z3*	✅	4s	3s	+33%
poly_chknorm	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	3s	-67%
poly_chknorm_c	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	8s	5s	+60%
poly_chknorm_native	LP64	bitwuzla	✅	8s	6s	+33%
	LP64	z3*	✅	5s	3s	+67%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	1s	+300%
poly_decompose	LP64	bitwuzla	✅	5s	8s	-38%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	10s	9s	+11%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
poly_decompose_c	LP64	z3*	✅	4s	2s	+100%
poly_decompose_native	LP64	cadical	✅	15s	17s	-12%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_native_x86_64	LP64	cadical	✅	11s	10s	+10%
	LP64	z3*	✅	2s	2s	+0%
poly_invntt_tomont	LP64	bitwuzla	✅	9s	5s	+80%
	LP64	z3*	✅	2s	2s	+0%
poly_invntt_tomont_c	LP64	bitwuzla	✅	156s	156s	+0%
	LP64	z3_smt_only*	✅	6s	8s	-25%
poly_invntt_tomont_native	LP64	bitwuzla	✅	51s	44s	+16%
	LP64	z3*	✅	3s	2s	+50%
poly_ntt	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	2s	+0%
poly_ntt_c	LP64	bitwuzla	✅	54s	46s	+17%
	LP64	z3_smt_only*	✅	11s	11s	+0%
poly_ntt_native	LP64	bitwuzla	✅	29s	25s	+16%
	LP64	z3*	✅	3s	2s	+50%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
poly_pointwise_montgomery	LP64	bitwuzla	✅	10s	9s	+11%
	LP64	z3*	✅	3s	2s	+50%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	196s	175s	+12%
	LP64	z3*	✅	52s	45s	+16%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	57s	53s	+8%
	LP64	z3*	✅	2s	4s	-50%
poly_power2round	LP64	bitwuzla	✅	344s	311s	+11%
	LP64	z3*	✅	3s	3s	+0%
poly_reduce	LP64	bitwuzla	✅	8s	11s	-27%
	LP64	z3*	✅	3s	2s	+50%
poly_shiftl	LP64	bitwuzla	✅	15s	11s	+36%
	LP64	z3*	✅	2s	1s	+100%
poly_sub	LP64	bitwuzla	✅	14s	16s	-12%
	LP64	z3*	✅	1s	3s	-67%
poly_uniform	LP64	bitwuzla	✅	159s	147s	+8%
	LP64	z3*	✅	3s	1s	+200%
poly_uniform_4x	LP64	z3*	✅	8s	7s	+14%
poly_uniform_eta	LP64	bitwuzla	✅	93s	81s	+15%
	LP64	z3*	✅	2s	4s	-50%
poly_uniform_eta_4x	LP64	z3*	✅	11s	8s	+38%
poly_uniform_gamma1	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	12s	13s	-8%
	LP64	z3*	✅	4s	1s	+300%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	25s	23s	+9%
	LP64	z3*	✅	4s	2s	+100%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	17s	11s	+55%
	LP64	z3*	✅	1s	2s	-50%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	88s	89s	-1%
	LP64	z3*	✅	3s	2s	+50%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	33s	29s	+14%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	31s	26s	+19%
	LP64	z3*	✅	1s	3s	-67%
polyeta_pack	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	3s	2s	+50%
polyeta_unpack	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	5s	6s	-17%
polyt0_pack	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	1s	1s	+0%
polyt0_unpack	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	9s	7s	+29%
polyt1_pack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
polyt1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	4s	+0%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	126s	115s	+10%
polyvec_matrix_expand_serial	LP64	z3*	✅	26s	21s	+24%
polyvec_matrix_pointwise_montgomery_row	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
polyvec_matrix_pointwise_montgomery_yvec	LP64	z3*	✅	16s	17s	-6%
polyveck_caddq	LP64	z3*	✅	6s	4s	+50%
polyveck_decompose_pack_w1	LP64	z3*	✅	8s	6s	+33%
polyveck_invntt_tomont	LP64	z3*	✅	5s	5s	+0%
polyveck_ntt	LP64	z3*	✅	4s	4s	+0%
polyveck_reduce	LP64	z3*	✅	2s	2s	+0%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	55s	55s	+0%
	LP64	z3*	✅	6s	4s	+50%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	18s	18s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyvecl_chknorm	LP64	z3*	✅	1s	2s	-50%
polyvecl_ntt	LP64	z3*	✅	4s	3s	+33%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	17s	15s	+13%
	LP64	z3_smt_only*	✅	4s	3s	+33%
polyvecl_pointwise_acc_montgomery_c	LP64	z3*	✅	164s	121s	+36%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	179s	177s	+1%
	LP64	z3_smt_only*	✅	4s	3s	+33%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	77s	77s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	48s	48s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	53s	47s	+13%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	51s	46s	+11%
	LP64	z3*	✅	4s	4s	+0%
polyw1_pack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
polyw1_pack_32	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack_88	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
polyz_pack	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
polyz_unpack	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	5s	3s	+67%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	5s	-60%
polyz_unpack_c	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	5s	4s	+25%
polyz_unpack_native	LP64	bitwuzla	✅	27s	27s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	17s	15s	+13%
	LP64	z3*	✅	1s	3s	-67%
power2round	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	4s	-75%
reduce32	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	3s	+0%
rej_eta	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
rej_eta_c	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	z3	✅	19s	18s	+6%
rej_eta_native	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	11s	12s	-8%
rej_uniform	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	13s	12s	+8%
rej_uniform_c	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	10s	10s	+0%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	2s	3s	-33%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3_smt_only*	✅	3s	2s	+50%
rej_uniform_native	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	22s	21s	+5%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	4s	3s	+33%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3_smt_only*	✅	11s	11s	+0%
shake128_absorb	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
shake128_finalize	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
shake128_init	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
shake128_release	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake128_squeeze	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
shake128x4_absorb_once	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	2s	2s	+0%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	3s	+0%
shake256	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
shake256_absorb	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	3s	+33%
shake256_finalize	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	4s	2s	+100%
shake256_init	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	4s	3s	+33%
shake256_release	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
shake256_squeeze	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	3s	2s	+50%
shake256x4_absorb_once	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	4s	2s	+100%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
sig_unpack_hints	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	16s	14s	+14%
sign_keypair	LP64	z3*	✅	4s	4s	+0%
sign_keypair_internal	LP64	z3_no_bv_extract*	✅	21s	24s	-12%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	34s	31s	+10%
sign_signature	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
sign_signature_extmu	LP64	cadical	✅	85s	64s	+33%
	LP64	z3*	✅	6s	4s	+50%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	463s	373s	+24%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	3s	4s	-25%
sign_signature_pre_hash_shake256	LP64	bitwuzla	✅	1786s	1541s	+16%
	LP64	z3*	✅	5s	5s	+0%
sign_verify	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
sign_verify_extmu	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	5s	-40%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	1329s	1207s	+10%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	3s	+0%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	4s	+0%
sk_s1hat_get_poly	LP64	bitwuzla	✅	35s	31s	+13%
	LP64	z3*	✅	3s	2s	+50%
sk_s2hat_get_poly	LP64	bitwuzla	✅	37s	33s	+12%
	LP64	z3*	✅	4s	2s	+100%
sk_t0hat_get_poly	LP64	bitwuzla	✅	36s	33s	+9%
	LP64	z3*	✅	4s	3s	+33%
sys_check_capability	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
unpack_pk_t1	LP64	bitwuzla	✅	14s	10s	+40%
	LP64	z3*	✅	4s	4s	+0%
unpack_sk	LP64	cadical	✅	79s	73s	+8%
	LP64	z3*	✅	4s	4s	+0%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	91s	87s	+5%
	LP64	z3*	✅	2s	3s	-33%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	320s	297s	+8%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk_t0hat	LP64	z3*	✅	4s	4s	+0%
use_hint	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
yvec_get_poly	LP64	bitwuzla	✅	39s	39s	+0%
	LP64	z3*	✅	2s	4s	-50%
yvec_init	LP64	bitwuzla	✅	16s	15s	+7%
	LP64	z3*	✅	3s	1s	+200%

[hanno-becker]

This is a bit difficult to read.

Can we express this as implications? E.g.

ensures(ctxlen > 255 ==> return_value == 0)`

[mkannwischer]

Yes.

[hanno-becker]

This is inconsistent with other public API which isn't checking for NULL pointers either.

[mkannwischer]

The contract change was just matching what the code does, but I agree that the code is currently not doing what our conventions suggest. I'll change it.

[hanno-becker]

Hm, we don't have this for the other backends, though... we should be consistent, whatever we do.

[mkannwischer]

I'm not aware of a case before that a backend can accidentally be assembled for an unsupported architecture instead of failing to assemble at all. If we do have more cases like that, we should guard it equally.

The x86_64 FIPS202 backend has a similar guard, but I think that's actually not needed:

mldsa-native/mldsa/src/fips202/native/x86_64/src/fips202_native_x86_64.h

Line 16 in 6daba60

#error Expecting a little-endian platform

[hanno-becker]

Some questions regarding consistency of the changes; see comments.