CBMC: Use constant quantifier ranges in some loop invariants by mkannwischer · Pull Request #1495 · pq-code-package/mldsa-native

mkannwischer · 2026-10-25T14:40:46Z

CBMC's propositional backend only expands a quantifier whose range
bounds simplify to constants. Otherwise it replaces the quantifier
by an unconstrained literal ("warning: ignoring forall"), which can
lead to spurious failures. Loop invariants of the form
forall(k, 0, i, P) or forall(k, i, N, P), with i the loop counter,
therefore cannot be checked with cadical.

Rewrite these invariants as forall(k, 0, N, k < i ==> P) and
forall(k, 0, N, k >= i ==> P), respectively. This is equivalent
given the existing invariant i <= N.

With this, add cadical as a second solver for 8 proofs: poly_add,
polyveck_caddq, polyveck_decompose_pack_w1, polyveck_invntt_tomont,
polyveck_ntt, polyveck_reduce, polyvecl_ntt and unpack_sk_t0hat.
Most of these are slow with cadical, locally between about 250s and
600s for ML-DSA-87.

oqs-bot · 2026-10-25T15:07:44Z

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

* default.

Full Results (423 configurations)

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

oqs-bot · 2026-10-25T15:12:30Z

CBMC Results (ML-DSA-44)

* default.

Full Results (423 configurations)

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

oqs-bot · 2026-10-25T15:24:33Z

CBMC Results (ML-DSA-65)

* default.

Full Results (423 configurations)

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

oqs-bot · 2026-10-25T15:25:45Z

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

* default.

Full Results (423 configurations)

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

oqs-bot · 2026-10-25T15:30:12Z

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

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`sign_signature_pre_hash_shake256`	LP64	bitwuzla	❌	-	1753s	-

Full Results (423 configurations)

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

oqs-bot · 2026-10-25T15:30:28Z

CBMC Results (ML-DSA-87)

* default.

Full Results (423 configurations)

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

CBMC's propositional backend only expands a quantifier whose range bounds simplify to constants. Otherwise it replaces the quantifier by an unconstrained literal ("warning: ignoring forall"), which can lead to spurious failures. Loop invariants of the form forall(k, 0, i, P) or forall(k, i, N, P), with i the loop counter, therefore cannot be checked with cadical. Rewrite these invariants as forall(k, 0, N, k < i ==> P) and forall(k, 0, N, k >= i ==> P), respectively. This is equivalent given the existing invariant i <= N. With this, add cadical as a second solver for 8 proofs: poly_add, polyveck_caddq, polyveck_decompose_pack_w1, polyveck_invntt_tomont, polyveck_ntt, polyveck_reduce, polyvecl_ntt and unpack_sk_t0hat. Most of these are slow with cadical, locally between about 250s and 600s for ML-DSA-87. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Mark the cadical solver profile as expensive so that CaDiCaL configurations run in the existing expensive job pool. This limits concurrent SAT array expansion and reduces memory pressure. Other proofs retain their existing scheduling, and disabling pools still permits unrestricted execution. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer force-pushed the cbmc-bounded-invariants branch from adb933d to b0fa28c Compare October 26, 2026 12:51

mkannwischer force-pushed the cbmc-bounded-invariants branch from b0fa28c to 9b62763 Compare October 26, 2026 12:52

Navigation Menu

Repository navigation

CBMC: Use constant quantifier ranges in some loop invariants - #1495

CBMC: Use constant quantifier ranges in some loop invariants #1495
mkannwischer wants to merge 2 commits into
mainfrom
cbmc-bounded-invariants

mkannwischer commented Oct 25, 2026

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!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mkannwischer commented Oct 25, 2026

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)

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-87, 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-87)

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

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