HOL-Light: Minor clean-ups by mkannwischer · Pull Request #1502 · pq-code-package/mldsa-native

mkannwischer · 2026-10-26T06:28:57Z

No description provided.

An instruction loop often applies the same arithmetic simplifier after each step. Building SIMD_SIMPLIFY_TAC inside the instruction callback rebuilds its rewrite conversion each time. The abbreviation variant also rebuilt that conversion for every selected register equation. Prepare the ARM/x86 step and SIMD tactics once before their loops. Move conversion construction and definition selection out of the abbreviation helper's per-fact callback. Still read local arithmetic equations from the current context: these change during execution. No converter-builder cache is needed. Prepared conversions capture the basic rewrite table; prepare again if it or the arithmetic rules change. Keep ordinary whole-context abbreviation, machine code and proof claims. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

After the NTT output congruence has been reduced to a real polynomial, REAL_INTEGER_TAC proves integer closure from the expression's structure. It does not consult context facts, but its recursive subgoals still carried the large execution context. Discard that context immediately before the four ARM/x86 NTT and INTT integer-closure calls. Leave instruction reasoning, congruence rewriting, output bounds and HOL Light's tactic unchanged. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

aarch64_utils.ml redefined SIMD_SIMPLIFY_CONV and SIMD_SIMPLIFY_TAC, shadowing the shared definitions in common/mldsa_specs.ml that it already loads. The conversion is identical and the shared tactic only additionally matches x86 int256 registers, which never occur in Arm goals, so use the shared definitions. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

ARM_STEPS_TAC and X86_STEPS_TAC do no work until they receive the step numbers, so binding them to the exec theorem outside a loop does not save anything. Only keep the prepared SIMD simplifier outside the loop. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

oqs-bot · 2026-10-26T06:53:06Z

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

* default.

Full Results (407 configurations)

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

oqs-bot · 2026-10-26T06:58:06Z

CBMC Results (ML-DSA-44)

* default.

Full Results (407 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2127s	2156s	-1.3%
`caddq`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	99s	102s	-3%
`decompose`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	26s	25s	+4%
	LP64	z3_smt_only	✅	20s	21s	-5%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	2s	2s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	2s	+50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	3s	4s	-25%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	18s	+0%
	LP64	z3*	✅	2s	5s	-60%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	8s	3s	+167%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	5s	+20%
	LP64	cvc5_arrays_exp	✅	9s	7s	+29%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`keccak_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	1s	+200%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	13s	-8%
	LP64	z3*	✅	13s	11s	+18%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	3s	1s	+200%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	362s	395s	-8%
`mld_check_pct`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	6s	5s	+20%
`mld_compute_pack_z`	LP64	cadical	✅	77s	79s	-3%
	LP64	z3_no_bv_extract*	✅	5s	5s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	3s	-67%
	ILP32	cvc5_arrays_exp	✅	3s	2s	+50%
	ILP32	z3	✅	4s	2s	+100%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	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	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	1s	3s	-67%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	88s	85s	+4%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	71s	71s	+0%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	5s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	15s	-7%
`mld_ntt_layer`	LP64	bitwuzla*	✅	27s	30s	-10%
	LP64	z3_no_bv_extract	✅	3s	2s	+50%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	36s	34s	+6%
	LP64	z3*	✅	2s	4s	-50%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	94s	92s	+2%
	LP64	z3*	✅	1s	3s	-67%
`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*	✅	2s	5s	-60%
`mld_sign_resume`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	1s	+100%
`ntt_native_aarch64`	LP64	bitwuzla	✅	20s	22s	-9%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	1s	2s	-50%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	2s	1s	+100%
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	22s	-18%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	z3*	✅	4s	2s	+100%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`pack_sig_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	3s	+0%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	70s	71s	-1%
	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	24s	23s	+4%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	1s	3s	-67%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	9s	9s	+0%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	24s	-8%
	LP64	z3*	✅	2s	1s	+100%
`poly_add`	LP64	z3*	✅	4s	4s	+0%
`poly_caddq`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	bitwuzla	✅	21s	21s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native`	LP64	bitwuzla	✅	118s	116s	+2%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	35s	36s	-3%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	117s	117s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_challenge`	LP64	bitwuzla	✅	25s	26s	-4%
	LP64	z3*	✅	4s	3s	+33%
`poly_chknorm`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	8s	+12%
	LP64	z3*	✅	7s	6s	+17%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	7s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	4s	4s	+0%
`poly_decompose`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_c`	LP64	z3*	✅	5s	5s	+0%
`poly_decompose_native`	LP64	cadical	✅	18s	18s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	cadical	✅	13s	12s	+8%
	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	9s	-56%
	LP64	z3*	✅	2s	1s	+100%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	8s	7s	+14%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	49s	50s	-2%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	4s	-50%
`poly_ntt_c`	LP64	bitwuzla	✅	53s	51s	+4%
	LP64	z3_smt_only*	✅	11s	10s	+10%
`poly_ntt_native`	LP64	bitwuzla	✅	31s	28s	+11%
	LP64	z3*	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	11s	11s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	55s	52s	+6%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	55s	53s	+4%
	LP64	z3*	✅	3s	2s	+50%
`poly_power2round`	LP64	bitwuzla	✅	286s	328s	-13%
	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	bitwuzla	✅	9s	11s	-18%
	LP64	z3*	✅	4s	1s	+300%
`poly_shiftl`	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	1s	3s	-67%
`poly_sub`	LP64	bitwuzla	✅	14s	18s	-22%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform`	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_4x`	LP64	z3*	✅	6s	7s	-14%
`poly_uniform_eta`	LP64	z3*	✅	3s	8s	-62%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	8s	+0%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	15s	14s	+7%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	24s	24s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	15s	11s	+36%
	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	83s	84s	-1%
	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	37s	34s	+9%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	35s	35s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyeta_pack`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	6s	-33%
`polyt0_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	7s	8s	-12%
`polyt1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	3s	+67%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	14s	16s	-12%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	6s	-50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	12s	13s	-8%
`polyveck_caddq`	LP64	z3*	✅	3s	2s	+50%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	4s	1s	+300%
`polyveck_invntt_tomont`	LP64	z3*	✅	2s	4s	-50%
`polyveck_ntt`	LP64	z3*	✅	4s	4s	+0%
`polyveck_reduce`	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	28s	29s	-3%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	17s	18s	-6%
	LP64	z3*	✅	2s	4s	-50%
`polyvecl_chknorm`	LP64	z3*	✅	1s	1s	+0%
`polyvecl_ntt`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	182s	161s	+13%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	40s	40s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	44s	43s	+2%
	LP64	z3*	✅	2s	1s	+100%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	33s	31s	+6%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	26s	26s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	5s	2s	+150%
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_unpack_88`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`polyz_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	6s	8s	-25%
	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	5s	+20%
`polyz_unpack_native`	LP64	bitwuzla	✅	27s	27s	+0%
	LP64	z3*	✅	4s	1s	+300%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	16s	+0%
	LP64	z3*	✅	2s	1s	+100%
`power2round`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`reduce32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	17s	18s	-6%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	12s	13s	-8%
`rej_uniform`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	16s	13s	+23%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	11s	12s	-8%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	4s	3s	+33%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	18s	20s	-10%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	9s	9s	+0%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	1s	+0%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`shake256`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	5s	3s	+67%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake256_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	1s	+200%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	✅	60s	55s	+9%
	LP64	z3*	✅	27s	28s	-4%
`sign_keypair`	LP64	z3*	✅	3s	4s	-25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	17s	14s	+21%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	32s	33s	-3%
`sign_signature`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`sign_signature_extmu`	LP64	cadical	✅	27s	28s	-4%
	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	256s	257s	-0%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	5s	-40%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	5s	5s	+0%
`sign_verify`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	352s	370s	-5%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	5s	3s	+67%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	31s	31s	+0%
	LP64	z3*	✅	1s	3s	-67%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	29s	31s	-6%
	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	13s	13s	+0%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk`	LP64	cadical	✅	39s	38s	+3%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	259s	251s	+3%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	244s	260s	-6%
	LP64	z3*	✅	1s	1s	+0%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	3s	-33%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	33s	32s	+3%
	LP64	z3*	✅	3s	2s	+50%
`yvec_init`	LP64	bitwuzla	✅	41s	40s	+2%
	LP64	z3*	✅	3s	3s	+0%

oqs-bot · 2026-10-26T07:11:06Z

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

* default.

Full Results (407 configurations)

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

oqs-bot · 2026-10-26T07:12:33Z

CBMC Results (ML-DSA-65)

* default.

Full Results (407 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2086s	2030s	+2.8%
`caddq`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	150s	137s	+9%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	25s	23s	+9%
	LP64	z3_smt_only	✅	21s	19s	+11%
`fqscale`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	1s	+100%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	20s	+10%
	LP64	z3*	✅	2s	1s	+100%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	2s	+0%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	19s	16s	+19%
	LP64	z3*	✅	1s	3s	-67%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	5s	4s	+25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	6s	-17%
	LP64	cvc5_arrays_exp	✅	9s	6s	+50%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	1s	5s	-80%
`keccak_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	z3	✅	3s	1s	+200%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	6s	3s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	13s	+0%
	LP64	z3*	✅	12s	13s	-8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	224s	207s	+8%
`mld_check_pct`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	7s	-43%
`mld_compute_pack_z`	LP64	cadical	✅	83s	78s	+6%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	1s	+100%
	ILP32	cvc5_arrays_exp	✅	1s	2s	-50%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	79s	79s	+0%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_h`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	68s	63s	+8%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	3s	+67%
	LP64	z3*	✅	4s	4s	+0%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	12s	-8%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	26s	-12%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	55s	51s	+8%
	LP64	z3*	✅	5s	4s	+25%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	229s	227s	+1%
	LP64	z3*	✅	4s	3s	+33%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_finish`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_resume`	LP64	bitwuzla	✅	4s	2s	+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	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	✅	21s	19s	+11%
	LP64	z3*	✅	3s	2s	+50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	2s	+0%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	1s	3s	-67%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	19s	+0%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	z3*	✅	4s	2s	+100%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
`pack_sig_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`pack_sig_z`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	5s	2s	+150%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	3s	+0%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	92s	87s	+6%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	21s	20s	+5%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	2s	3s	-33%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	3s	1s	+200%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	24s	19s	+26%
	LP64	z3*	✅	3s	6s	-50%
`poly_add`	LP64	z3*	✅	4s	3s	+33%
`poly_caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	bitwuzla	✅	20s	17s	+18%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	bitwuzla	✅	113s	102s	+11%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	35s	33s	+6%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	127s	113s	+12%
	LP64	z3*	✅	3s	1s	+200%
`poly_challenge`	LP64	bitwuzla	✅	23s	20s	+15%
	LP64	z3*	✅	5s	2s	+150%
`poly_chknorm`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_c`	LP64	bitwuzla	✅	13s	7s	+86%
	LP64	z3*	✅	8s	6s	+33%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	7s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	11s	11s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_c`	LP64	z3*	✅	4s	4s	+0%
`poly_decompose_native`	LP64	cadical	✅	14s	12s	+17%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	cadical	✅	10s	10s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	7s	-14%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	45s	42s	+7%
	LP64	z3*	✅	3s	5s	-40%
`poly_ntt`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	1s	+300%
`poly_ntt_c`	LP64	bitwuzla	✅	52s	46s	+13%
	LP64	z3_smt_only*	✅	12s	9s	+33%
`poly_ntt_native`	LP64	bitwuzla	✅	26s	25s	+4%
	LP64	z3*	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	4s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	8s	8s	+0%
	LP64	z3*	✅	4s	3s	+33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	48s	45s	+7%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	54s	56s	-4%
	LP64	z3*	✅	3s	3s	+0%
`poly_power2round`	LP64	bitwuzla	✅	304s	276s	+10%
	LP64	z3*	✅	3s	2s	+50%
`poly_reduce`	LP64	bitwuzla	✅	8s	8s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_shiftl`	LP64	bitwuzla	✅	14s	11s	+27%
	LP64	z3*	✅	1s	3s	-67%
`poly_sub`	LP64	bitwuzla	✅	14s	13s	+8%
	LP64	z3*	✅	1s	4s	-75%
`poly_uniform`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	z3*	✅	9s	6s	+50%
`poly_uniform_eta`	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_eta_4x`	LP64	z3*	✅	6s	6s	+0%
`poly_uniform_gamma1`	LP64	cadical	✅	7s	4s	+75%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	15s	12s	+25%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	25s	22s	+14%
	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	11s	10s	+10%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	91s	89s	+2%
	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	26s	28s	-7%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	26s	+15%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyt0_pack`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	4s	-25%
`polyt0_unpack`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	7s	8s	-12%
`polyt1_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	3s	+67%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	74s	72s	+3%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	14s	15s	-7%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	18s	17s	+6%
`polyveck_caddq`	LP64	z3*	✅	4s	5s	-20%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	7s	8s	-12%
`polyveck_invntt_tomont`	LP64	z3*	✅	5s	3s	+67%
`polyveck_ntt`	LP64	z3*	✅	7s	4s	+75%
`polyveck_reduce`	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	39s	40s	-3%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	19s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyvecl_chknorm`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_ntt`	LP64	z3*	✅	4s	4s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	9s	9s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	116s	114s	+2%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	4s	-50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	34s	32s	+6%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	33s	34s	-3%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	35s	35s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	33s	31s	+6%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	2s	+150%
`polyw1_unpack_88`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	1s	+100%
`polyz_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_native`	LP64	bitwuzla	✅	26s	25s	+4%
	LP64	z3*	✅	4s	1s	+300%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	15s	-7%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	6s	3s	+100%
	LP64	z3	✅	13s	8s	+62%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	9s	9s	+0%
`rej_uniform`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	13s	14s	-7%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	10s	10s	+0%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	4s	2s	+100%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	17s	16s	+6%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	3s	2s	+50%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3_smt_only*	✅	8s	10s	-20%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`shake128_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`shake128_release`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	4s	-50%
`shake256`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	6s	-83%
`shake256_absorb`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	1s	+300%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`sig_unpack_hints`	LP64	bitwuzla	✅	1356s	1222s	+11%
	LP64	z3*	✅	22s	17s	+29%
`sign_keypair`	LP64	z3*	✅	4s	5s	-20%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	18s	17s	+6%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	35s	33s	+6%
`sign_signature`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_extmu`	LP64	cadical	✅	34s	32s	+6%
	LP64	z3*	✅	5s	3s	+67%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	197s	197s	+0%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	4s	-75%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	345s	339s	+2%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	4s	-25%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	452s	453s	-0%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	40s	37s	+8%
	LP64	z3*	✅	3s	3s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	1s	1s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	29s	28s	+4%
	LP64	z3*	✅	2s	4s	-50%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk`	LP64	cadical	✅	56s	51s	+10%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	88s	85s	+4%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	152s	150s	+1%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_t0hat`	LP64	z3*	✅	3s	6s	-50%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	34s	31s	+10%
	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	bitwuzla	✅	11s	8s	+38%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-10-26T07:16:37Z

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

* default.

Full Results (407 configurations)

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

oqs-bot · 2026-10-26T07:17:15Z

CBMC Results (ML-DSA-87)

* default.

Full Results (407 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	3293s	3376s	-2.5%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	244s	236s	+3%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	5s	-60%
`fqmul`	LP64	bitwuzla*	✅	23s	27s	-15%
	LP64	z3_smt_only	✅	20s	21s	-5%
`fqscale`	LP64	bitwuzla*	✅	5s	3s	+67%
	LP64	z3	✅	1s	4s	-75%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	21s	+5%
	LP64	z3*	✅	3s	2s	+50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	8s	10s	-20%
	LP64	z3	✅	3s	2s	+50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	4s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	17s	18s	-6%
	LP64	z3*	✅	1s	2s	-50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	cvc5_arrays_exp	✅	10s	9s	+11%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`keccak_init`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	4s	1s	+300%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	1s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	6s	2s	+200%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	4s	1s	+300%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	14s	14s	+0%
	LP64	z3*	✅	13s	12s	+8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	317s	312s	+2%
`mld_check_pct`	LP64	bitwuzla	✅	4s	8s	-50%
	LP64	z3*	✅	5s	5s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	93s	93s	+0%
	LP64	z3_no_bv_extract*	✅	5s	6s	-17%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	5s	-60%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	1s	4s	-75%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_no_bv_extract	✅	79s	82s	-4%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	63s	68s	-7%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	13s	+8%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	26s	-4%
	LP64	z3_no_bv_extract	✅	4s	7s	-43%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	1s	3s	-67%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	5s	5s	+0%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	81s	86s	-6%
	LP64	z3*	✅	8s	8s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	540s	541s	-0%
	LP64	z3*	✅	6s	4s	+50%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_sign_finish`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_sign_resume`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	2s	2s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	✅	20s	21s	-5%
	LP64	z3*	✅	2s	5s	-60%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	2s	+50%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	2s	2s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	19s	+0%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
`pack_sig_h`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	4s	3s	+33%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	1s	+100%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	5s	-40%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	101s	109s	-7%
	LP64	z3_smt_only*	✅	4s	7s	-43%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	23s	23s	+0%
	LP64	z3*	✅	4s	2s	+100%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	2s	4s	-50%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	1s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	10s	-30%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	22s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_add`	LP64	z3*	✅	3s	6s	-50%
`poly_caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	21s	-14%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native`	LP64	bitwuzla	✅	101s	112s	-10%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	35s	35s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	114s	117s	-3%
	LP64	z3*	✅	3s	4s	-25%
`poly_challenge`	LP64	bitwuzla	✅	33s	35s	-6%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	1s	+300%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	6s	6s	+0%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	9s	9s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_native`	LP64	cadical	✅	14s	15s	-7%
	LP64	z3*	✅	4s	1s	+300%
`poly_decompose_native_x86_64`	LP64	cadical	✅	11s	10s	+10%
	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	7s	-14%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	43s	47s	-9%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	3s	6s	-50%
`poly_ntt_c`	LP64	bitwuzla	✅	45s	47s	-4%
	LP64	z3_smt_only*	✅	11s	9s	+22%
`poly_ntt_native`	LP64	bitwuzla	✅	26s	26s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	5s	-80%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	10s	-10%
	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	46s	50s	-8%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	56s	56s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_power2round`	LP64	bitwuzla	✅	291s	255s	+14%
	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	bitwuzla	✅	8s	9s	-11%
	LP64	z3*	✅	1s	1s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	11s	10s	+10%
	LP64	z3*	✅	2s	2s	+0%
`poly_sub`	LP64	bitwuzla	✅	13s	16s	-19%
	LP64	z3*	✅	5s	2s	+150%
`poly_uniform`	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_4x`	LP64	z3*	✅	7s	8s	-12%
`poly_uniform_eta`	LP64	z3*	✅	3s	5s	-40%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	11s	-18%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	12s	16s	-25%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	23s	+0%
	LP64	z3*	✅	4s	4s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	11s	11s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	93s	93s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	28s	29s	-3%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	29s	33s	-12%
	LP64	z3*	✅	1s	2s	-50%
`polyeta_pack`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	10s	6s	+67%
`polyt0_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	7s	7s	+0%
`polyt1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	4s	-25%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	107s	115s	-7%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	22s	23s	-4%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	4s	-25%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	14s	16s	-12%
`polyveck_caddq`	LP64	z3*	✅	5s	8s	-38%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	7s	7s	+0%
`polyveck_invntt_tomont`	LP64	z3*	✅	6s	3s	+100%
`polyveck_ntt`	LP64	z3*	✅	7s	5s	+40%
`polyveck_reduce`	LP64	z3*	✅	3s	3s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	51s	56s	-9%
	LP64	z3*	✅	3s	1s	+200%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	20s	-10%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_chknorm`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_ntt`	LP64	z3*	✅	4s	5s	-20%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	14s	12s	+17%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	142s	139s	+2%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	76s	74s	+3%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	44s	46s	-4%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	46s	48s	-4%
	LP64	z3*	✅	5s	3s	+67%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	48s	49s	-2%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyz_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	4s	1s	+300%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	6s	-17%
`polyz_unpack_native`	LP64	bitwuzla	✅	26s	27s	-4%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	14s	+14%
	LP64	z3*	✅	3s	2s	+50%
`power2round`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	4s	4s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	17s	16s	+6%
`rej_eta_native`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	12s	13s	-8%
`rej_uniform`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	12s	13s	-8%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	9s	11s	-18%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	5s	4s	+25%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	19s	16s	+19%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3_smt_only*	✅	8s	9s	-11%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	4s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
`shake128_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake128_release`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	5s	2s	+150%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	1s	+100%
`shake256`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	3s	+33%
`shake256_absorb`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`shake256_release`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	bitwuzla	✅	28s	28s	+0%
	LP64	z3*	✅	15s	17s	-12%
`sign_keypair`	LP64	z3*	✅	7s	5s	+40%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	21s	21s	+0%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	31s	34s	-9%
`sign_signature`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	3s	-33%
`sign_signature_extmu`	LP64	cadical	✅	72s	72s	+0%
	LP64	z3*	✅	1s	4s	-75%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	404s	424s	-5%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	✅	1521s	1613s	-6%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	1189s	1232s	-3%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	31s	35s	-11%
	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	34s	36s	-6%
	LP64	z3*	✅	4s	1s	+300%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	32s	33s	-3%
	LP64	z3*	✅	4s	2s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	12s	-17%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk`	LP64	cadical	✅	77s	77s	+0%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	85s	85s	+0%
	LP64	z3*	✅	6s	4s	+50%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	306s	309s	-1%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_t0hat`	LP64	z3*	✅	5s	2s	+150%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	35s	40s	-12%
	LP64	z3*	✅	3s	1s	+200%
`yvec_init`	LP64	bitwuzla	✅	16s	16s	+0%
	LP64	z3*	✅	2s	4s	-50%

hanno-becker and others added 4 commits October 25, 2026 19:48

mkannwischer added the needs-mlkem-native-port label Oct 26, 2026

Navigation Menu

Repository navigation

HOL-Light: Minor clean-ups - #1502

HOL-Light: Minor clean-ups#1502
mkannwischer wants to merge 4 commits into
mainfrom
hol-speedup-followup

mkannwischer commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mkannwischer commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

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

Uh oh!

oqs-bot commented Oct 26, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Oct 26, 2026

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

Uh oh!

oqs-bot commented Oct 26, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Oct 26, 2026

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

Uh oh!

oqs-bot commented Oct 26, 2026

CBMC Results (ML-DSA-87)

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants