HOL-Light: Tweaks for better proof performance by hanno-becker · Pull Request #1499 · pq-code-package/mldsa-native

hanno-becker · 2026-10-25T19:52:06Z

This PR makes two small changes to improve proof performance:

First, it hoists the preparation of SIMD_SIMPLIFY_TAC out of a binder; everything under a binder is lazily evaluated, hence SIMD_SIMPLIFY_TAC was re-instantiated with every symbolic execution step. As a general rule, one should always hoist generic code out of repeated binders -- so let's watch out for it -- but this step in particular stood out so far.

Second, drop assumptions prior to running REAL_INTEGER_TAC; the tactic doesn't need it.

No change to the underlying s2n-bignum pin is made.

Proof	Baseline	Before	#1499	Change
AArch64 NTT	#1462	1:56:29	0:37:19	−68.0%
AArch64 INTT	#1462	2:15:59	0:47:22	−65.2%
x86_64 NTT	#1462	2:01:27	0:41:02	−66.2%
x86_64 INTT	#1462	2:39:16	0:45:11	−71.6%
AArch64 rej_uniform_eta2	#1398	0:15:37	0:15:40	+0.3%
AArch64 rej_uniform_eta4	#1398	0:10:09	0:10:00	−1.5%
x86_64 rej_uniform_eta2	#1398	0:44:57	0:32:29	−27.7%
x86_64 rej_uniform_eta4	#1398	0:14:15	0:07:02	−50.6%

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>

oqs-bot · 2026-10-25T20:16:26Z

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

* default.

Full Results (397 configurations)

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

oqs-bot · 2026-10-25T20:19:38Z

CBMC Results (ML-DSA-44)

* default.

Full Results (397 configurations)

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

oqs-bot · 2026-10-25T20:32:07Z

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

* default.

Full Results (397 configurations)

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

oqs-bot · 2026-10-25T20:36:01Z

CBMC Results (ML-DSA-65)

* default.

Full Results (397 configurations)

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

oqs-bot · 2026-10-25T20:37:57Z

CBMC Results (ML-DSA-87)

* default.

Full Results (397 configurations)

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

oqs-bot · 2026-10-25T20:38:16Z

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

* default.

Full Results (397 configurations)

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

mkannwischer

Amazing speed-ups. Thank you!

hanno-becker added 2 commits October 25, 2026 19:48

hanno-becker requested a review from a team as a code owner October 25, 2026 19:52

hanno-becker force-pushed the hol-speedup branch from 9c2127f to fd04909 Compare October 25, 2026 19:56

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

hanno-becker mentioned this pull request Oct 26, 2026

HOL-Light: Avoid repeated work in proof loops pq-code-package/mlkem-native#1962

Merged

hanno-becker added enhancement New feature or request hol-light labels Oct 26, 2026

mkannwischer approved these changes Oct 26, 2026

View reviewed changes

mkannwischer added this pull request to the merge queue Oct 26, 2026

Merged via the queue into main with commit 33031ee Oct 26, 2026
469 checks passed

mkannwischer deleted the hol-speedup branch October 26, 2026 09:20

github-actions Bot mentioned this pull request Oct 26, 2026

Port: HOL-Light: Tweaks for better proof performance pq-code-package/mlkem-native#1963

Closed

Navigation Menu

Repository navigation

HOL-Light: Tweaks for better proof performance - #1499

HOL-Light: Tweaks for better proof performance#1499
mkannwischer merged 2 commits into
mainfrom
hol-speedup

hanno-becker commented Oct 25, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 25, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 25, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 25, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 25, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 25, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 25, 2026 •

edited

Loading

Uh oh!

mkannwischer left a comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

hanno-becker commented Oct 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

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

Uh oh!

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

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hanno-becker commented Oct 25, 2026 •

edited

Loading

oqs-bot commented Oct 25, 2026 •

edited

Loading

oqs-bot commented Oct 25, 2026 •

edited

Loading

oqs-bot commented Oct 25, 2026 •

edited

Loading

oqs-bot commented Oct 25, 2026 •

edited

Loading

oqs-bot commented Oct 25, 2026 •

edited

Loading

oqs-bot commented Oct 25, 2026 •

edited

Loading