CBMC: Add CaDiCaL as a second solver for all remaining proofs by mkannwischer · Pull Request #1521 · pq-code-package/mldsa-native

mkannwischer · 2026-11-03T02:15:23Z

Testing a CBMC patch for diffblue/cbmc#9387.

CBMC skolemizes every asserted forall, but the propositional back end expands assumed foralls over their constant range. A bound handed from a callee's ensures to a caller's requires then becomes a symbolic read at a fresh index that the solver has to relate to every expanded instance, which makes the encoding very large for cadical. Patch CBMC 6.11.0 with --no-forall-skolemization, which passes asserted quantifiers to the back end unchanged so that they are expanded like assumed ones. The patch also treats an empty instantiation range as true (forall) or false (exists) instead of leaving the quantifier unconstrained. The flag is off by default. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-87, sign_signature_internal then takes about 560s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-87, attempt_signature_generation then takes about 420s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-87, compute_pack_t0_t1 then takes about 750s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-44, sign_verify_internal then takes about 210s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Pass --no-forall-skolemization for cadical only. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

oqs-bot · 2026-11-03T03:39:22Z

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

* default.

Full Results (440 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1531s	1535s	-0.3%
`caddq`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	3s	+0%
`compute_pack_t0_t1`	LP64	cadical	✅	51s	omitted	new
	LP64	z3_no_bv_extract*	✅	35s	37s	-5%
`decompose`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	27s	27s	+0%
	LP64	z3_smt_only	✅	23s	22s	+5%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`intt_native_aarch64`	LP64	bitwuzla	✅	23s	29s	-21%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	2s	1s	+100%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	1s	2s	-50%
`intt_native_x86_64`	LP64	bitwuzla	✅	20s	18s	+11%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	7s	-29%
	LP64	cvc5_arrays_exp	✅	9s	9s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
`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*	✅	4s	1s	+300%
	LP64	z3	✅	1s	6s	-83%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	3s	-67%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	5s	3s	+67%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	3s	-33%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	12s	+0%
	LP64	z3*	✅	13s	11s	+18%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	3s	1s	+200%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	cadical	✅	372s	omitted	new
	LP64	z3_no_bv_extract*	✅	166s	166s	+0%
`mld_check_pct`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	7s	6s	+17%
`mld_compute_pack_z`	LP64	cadical	✅	38s	41s	-7%
	LP64	z3_no_bv_extract*	✅	4s	2s	+100%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	1s	4s	-75%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	✅	83s	100s	-17%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	69s	73s	-5%
	LP64	z3_smt_only	✅	81s	83s	-2%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	5s	3s	+67%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	15s	-13%
	LP64	z3_no_bv_extract	✅	128s	141s	-9%
`mld_ntt_layer`	LP64	bitwuzla*	✅	30s	28s	+7%
	LP64	z3_no_bv_extract	✅	2s	4s	-50%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	5s	-40%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	4s	4s	+0%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	30s	30s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	93s	95s	-2%
	LP64	z3*	✅	3s	2s	+50%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	4s	2s	+100%
`ntt_native_aarch64`	LP64	bitwuzla	✅	25s	23s	+9%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	5s	4s	+25%
	LP64	z3	✅	3s	2s	+50%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	1s	2s	-50%
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	23s	-22%
	LP64	z3*	✅	4s	1s	+300%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	204s	199s	+3%
	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3_no_bv_extract*	✅	4s	2s	+100%
`pack_sig_z`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	4s	-50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	59s	60s	-2%
	LP64	z3_smt_only*	✅	7s	4s	+75%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	67s	58s	+16%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	23s	27s	-15%
	LP64	z3*	✅	1s	1s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	11s	-36%
	LP64	z3	✅	2s	3s	-33%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	8s	10s	-20%
	LP64	z3	✅	2s	1s	+100%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	24s	26s	-8%
	LP64	z3*	✅	3s	2s	+50%
`poly_add`	LP64	cadical	✅	50s	53s	-6%
	LP64	z3*	✅	15s	14s	+7%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_c`	LP64	bitwuzla	✅	20s	23s	-13%
	LP64	z3*	✅	4s	4s	+0%
`poly_caddq_native`	LP64	bitwuzla	✅	117s	132s	-11%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	37s	37s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	132s	146s	-10%
	LP64	z3*	✅	1s	2s	-50%
`poly_challenge`	LP64	bitwuzla	✅	26s	31s	-16%
	LP64	z3*	✅	4s	3s	+33%
`poly_chknorm`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	11s	-9%
	LP64	z3*	✅	7s	6s	+17%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	7s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	229s	248s	-8%
	LP64	z3*	✅	3s	5s	-40%
`poly_decompose_native`	LP64	cadical	✅	14s	16s	-12%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_native_x86_64`	LP64	cadical	✅	12s	11s	+9%
	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	156s	166s	-6%
	LP64	z3_smt_only*	✅	7s	9s	-22%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	50s	52s	-4%
	LP64	z3*	✅	3s	2s	+50%
`poly_ntt`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	1s	+100%
`poly_ntt_c`	LP64	bitwuzla	✅	50s	56s	-11%
	LP64	z3_smt_only*	✅	12s	11s	+9%
`poly_ntt_native`	LP64	bitwuzla	✅	30s	32s	-6%
	LP64	z3*	✅	4s	2s	+100%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	11s	11s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	203s	208s	-2%
	LP64	z3*	✅	86s	89s	-3%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	52s	55s	-5%
	LP64	z3*	✅	1s	1s	+0%
`poly_power2round`	LP64	bitwuzla	✅	312s	341s	-9%
	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_shiftl`	LP64	bitwuzla	✅	15s	11s	+36%
	LP64	z3*	✅	4s	1s	+300%
`poly_sub`	LP64	bitwuzla	✅	16s	19s	-16%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform`	LP64	bitwuzla	✅	199s	208s	-4%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_4x`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_eta`	LP64	bitwuzla	✅	83s	90s	-8%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_eta_4x`	LP64	cadical	✅	63s	64s	-2%
	LP64	z3*	✅	9s	10s	-10%
`poly_uniform_gamma1`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	1s	4s	-75%
	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	24s	24s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	11s	13s	-15%
	LP64	z3*	✅	4s	6s	-33%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	87s	87s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	35s	39s	-10%
	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	38s	37s	+3%
	LP64	z3*	✅	3s	2s	+50%
`polyeta_pack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	8s	9s	-11%
`polyt0_pack`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	2s	+100%
`polyt0_unpack`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	8s	7s	+14%
`polyt1_pack`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	5s	5s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_matrix_expand`	LP64	cadical	✅	1s	omitted	new
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	4s	omitted	new
	LP64	z3*	✅	3s	2s	+50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	37s	41s	-10%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	492s	499s	-1%
	LP64	z3*	✅	109s	113s	-4%
`polyveck_caddq`	LP64	cadical	✅	105s	132s	-20%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	109s	113s	-4%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_invntt_tomont`	LP64	cadical	✅	142s	146s	-3%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_ntt`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_reduce`	LP64	cadical	✅	139s	121s	+15%
	LP64	z3*	✅	3s	1s	+200%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	4s	1s	+300%
	LP64	z3*	✅	5s	3s	+67%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	17s	+6%
	LP64	z3*	✅	1s	4s	-75%
`polyvecl_chknorm`	LP64	cadical	✅	53s	55s	-4%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_ntt`	LP64	cadical	✅	119s	129s	-8%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3_smt_only*	✅	1s	1s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	4s	1s	+300%
	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	1s	1s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	33s	36s	-8%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	28s	31s	-10%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack_88`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`polyz_pack`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack`	LP64	bitwuzla	✅	6s	9s	-33%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	1s	+300%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	7s	8s	-12%
`polyz_unpack_native`	LP64	bitwuzla	✅	28s	34s	-18%
	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	18s	16s	+12%
	LP64	z3*	✅	2s	2s	+0%
`power2round`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3	✅	22s	27s	-19%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	17s	16s	+6%
`rej_uniform`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	14s	12s	+17%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	10s	10s	+0%
`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	✅	1s	2s	-50%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	✅	10s	11s	-9%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3_smt_only*	✅	13s	12s	+8%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	5s	2s	+150%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`shake128_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
`shake128_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	3s	1s	+200%
`shake256`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	bitwuzla	✅	3s	3s	+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	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`shake256_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	1s	+100%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	✅	57s	64s	-11%
	LP64	z3*	✅	40s	46s	-13%
`sign_keypair`	LP64	cadical	✅	52s	50s	+4%
	LP64	z3*	✅	6s	6s	+0%
`sign_keypair_internal`	LP64	cadical	✅	159s	154s	+3%
	LP64	z3_no_bv_extract*	✅	13s	12s	+8%
`sign_pk_from_sk`	LP64	cadical	✅	16s	omitted	new
	LP64	z3_no_bv_extract*	✅	47s	34s	+38%
`sign_signature`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	5s	+0%
`sign_signature_extmu`	LP64	cadical	✅	27s	24s	+12%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_internal`	LP64	cadical	✅	11s	omitted	new
	LP64	z3_no_bv_extract*	✅	13s	17s	-24%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	12s	12s	+0%
	LP64	z3*	✅	4s	5s	-20%
`sign_verify`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`sign_verify_internal`	LP64	cadical	✅	52s	omitted	new
	LP64	z3_no_bv_extract*	✅	282s	296s	-5%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	2s	+100%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	5s	-80%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk`	LP64	cadical	✅	1s	4s	-75%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_t0hat`	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_init`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-11-03T03:42:50Z

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	57s	31s	+84%

Full Results (440 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2303s	2064s	+11.6%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	5s	-40%
`compute_pack_t0_t1`	LP64	cadical	✅	165s	omitted	new
	LP64	z3_no_bv_extract*	✅	105s	92s	+14%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`fqmul`	LP64	bitwuzla*	✅	25s	24s	+4%
	LP64	z3_smt_only	✅	21s	20s	+5%
`fqscale`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`intt_native_aarch64`	LP64	bitwuzla	✅	23s	23s	+0%
	LP64	z3*	✅	4s	3s	+33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	4s	-50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	16s	+12%
	LP64	z3*	✅	2s	2s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	cvc5_arrays_exp	✅	8s	10s	-20%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	3s	2s	+50%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	1s	+200%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	3s	1s	+200%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	1s	+300%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	13s	+0%
	LP64	z3*	✅	12s	12s	+0%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	1s	4s	-75%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_attempt_signature_generation`	LP64	cadical	✅	177s	omitted	new
	LP64	z3_no_bv_extract*	✅	380s	349s	+9%
`mld_check_pct`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	5s	7s	-29%
`mld_compute_pack_z`	LP64	cadical	✅	67s	65s	+3%
	LP64	z3_no_bv_extract*	✅	6s	7s	-14%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	4s	5s	-20%
	ILP32	cvc5_arrays_exp	✅	1s	5s	-80%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	89s	77s	+16%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	1s	+300%
`mld_h`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	72s	61s	+18%
	LP64	z3_smt_only	✅	93s	92s	+1%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	3s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	12s	+17%
	LP64	z3_no_bv_extract	✅	177s	156s	+13%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	24s	+4%
	LP64	z3_no_bv_extract	✅	4s	5s	-20%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	4s	3s	+33%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	29s	28s	+4%
	LP64	z3*	✅	3s	3s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	94s	90s	+4%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_finish`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	2s	7s	-71%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	3s	1s	+200%
`ntt_native_aarch64`	LP64	bitwuzla	✅	21s	19s	+11%
	LP64	z3*	✅	3s	1s	+200%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	4s	2s	+100%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	5s	2s	+150%
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	17s	+6%
	LP64	z3*	✅	6s	4s	+50%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	200s	181s	+10%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	5s	2s	+150%
`pack_sig_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	58s	55s	+5%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	58s	54s	+7%
	LP64	z3_smt_only*	✅	5s	5s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	23s	22s	+5%
	LP64	z3*	✅	1s	3s	-67%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	4s	+75%
	LP64	z3	✅	4s	3s	+33%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	22s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_add`	LP64	cadical	✅	48s	46s	+4%
	LP64	z3*	✅	15s	15s	+0%
`poly_caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_c`	LP64	bitwuzla	✅	23s	16s	+44%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native`	LP64	bitwuzla	✅	125s	107s	+17%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	35s	35s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	119s	112s	+6%
	LP64	z3*	✅	3s	3s	+0%
`poly_challenge`	LP64	bitwuzla	✅	28s	23s	+22%
	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	1s	+300%
`poly_chknorm_c`	LP64	bitwuzla	✅	11s	9s	+22%
	LP64	z3*	✅	8s	10s	-20%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	5s	2s	+150%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	242s	179s	+35%
	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native`	LP64	cadical	✅	17s	15s	+13%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	cadical	✅	9s	9s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	172s	154s	+12%
	LP64	z3_smt_only*	✅	6s	7s	-14%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	43s	+9%
	LP64	z3*	✅	4s	3s	+33%
`poly_ntt`	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	bitwuzla	✅	56s	43s	+30%
	LP64	z3_smt_only*	✅	10s	10s	+0%
`poly_ntt_native`	LP64	bitwuzla	✅	28s	26s	+8%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	11s	-18%
	LP64	z3*	✅	4s	4s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	205s	185s	+11%
	LP64	z3*	✅	52s	47s	+11%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	55s	59s	-7%
	LP64	z3*	✅	1s	4s	-75%
`poly_power2round`	LP64	bitwuzla	✅	323s	256s	+26%
	LP64	z3*	✅	2s	2s	+0%
`poly_reduce`	LP64	bitwuzla	✅	12s	7s	+71%
	LP64	z3*	✅	1s	2s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	13s	11s	+18%
	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	bitwuzla	✅	18s	15s	+20%
	LP64	z3*	✅	1s	1s	+0%
`poly_uniform`	LP64	bitwuzla	✅	197s	159s	+24%
	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_4x`	LP64	cadical	✅	62s	61s	+2%
	LP64	z3*	✅	8s	6s	+33%
`poly_uniform_eta`	LP64	bitwuzla	✅	87s	77s	+13%
	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_eta_4x`	LP64	cadical	✅	63s	60s	+5%
	LP64	z3*	✅	10s	7s	+43%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	10s	10s	+0%
	LP64	z3*	✅	4s	4s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	24s	23s	+4%
	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	13s	10s	+30%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	94s	94s	+0%
	LP64	z3*	✅	4s	1s	+300%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	36s	30s	+20%
	LP64	z3*	✅	6s	2s	+200%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	34s	33s	+3%
	LP64	z3*	✅	3s	2s	+50%
`polyeta_pack`	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	1s	2s	-50%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	4s	+25%
`polyt0_pack`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	8s	7s	+14%
`polyt1_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	5s	+0%
`polyvec_matrix_expand`	LP64	cadical	✅	7s	omitted	new
	LP64	z3_no_bv_extract*	✅	16s	15s	+7%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	6s	omitted	new
	LP64	z3*	✅	5s	5s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	101s	100s	+1%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	243s	236s	+3%
	LP64	z3*	✅	8s	6s	+33%
`polyveck_caddq`	LP64	cadical	✅	105s	100s	+5%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	110s	113s	-3%
	LP64	z3*	✅	4s	2s	+100%
`polyveck_invntt_tomont`	LP64	cadical	✅	143s	135s	+6%
	LP64	z3*	✅	4s	3s	+33%
`polyveck_ntt`	LP64	cadical	✅	119s	113s	+5%
	LP64	z3*	✅	3s	3s	+0%
`polyveck_reduce`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	28s	27s	+4%
	LP64	z3*	✅	1s	1s	+0%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	17s	16s	+6%
	LP64	z3*	✅	3s	4s	-25%
`polyvecl_chknorm`	LP64	cadical	✅	52s	50s	+4%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_ntt`	LP64	cadical	✅	120s	114s	+5%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	8s	4s	+100%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	92s	90s	+2%
	LP64	z3_smt_only*	✅	211s	179s	+18%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	161s	156s	+3%
	LP64	z3_smt_only*	✅	1s	4s	-75%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	40s	37s	+8%
	LP64	z3*	✅	2s	1s	+100%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	43s	43s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	32s	33s	-3%
	LP64	z3*	✅	4s	2s	+100%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	29s	26s	+12%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
`polyw1_pack_88`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyz_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	6s	5s	+20%
`polyz_unpack_native`	LP64	bitwuzla	✅	27s	26s	+4%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	13s	+23%
	LP64	z3*	✅	2s	1s	+100%
`power2round`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	1s	+100%
`reduce32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	3s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	5s	1s	+400%
`rej_eta_c`	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	z3	✅	18s	18s	+0%
`rej_eta_native`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	16s	15s	+7%
`rej_uniform`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	7s	8s	-12%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	13s	9s	+44%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	1s	+100%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3_smt_only*	✅	1s	4s	-75%
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	11s	8s	+38%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	2s	4s	-50%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3_smt_only*	✅	11s	10s	+10%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	1s	+300%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	1s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	4s	1s	+300%
`shake256`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	6s	3s	+100%
`shake256_absorb`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	1s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	3s	3s	+0%
`sig_unpack_hints`	LP64	bitwuzla	✅	58s	52s	+12%
	LP64	z3*	✅	29s	24s	+21%
`sign_keypair`	LP64	cadical	✅	47s	44s	+7%
	LP64	z3*	✅	5s	6s	-17%
`sign_keypair_internal`	LP64	cadical	✅	163s	166s	-2%
	LP64	z3_no_bv_extract*	✅	16s	13s	+23%
`sign_pk_from_sk`	LP64	cadical	✅	18s	omitted	new
	LP64	z3_no_bv_extract*	⚠️	57s	31s	+84%
`sign_signature`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	cadical	✅	21s	22s	-5%
	LP64	z3*	✅	5s	2s	+150%
`sign_signature_internal`	LP64	cadical	✅	108s	omitted	new
	LP64	z3_no_bv_extract*	✅	265s	239s	+11%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	12s	10s	+20%
	LP64	z3*	✅	6s	5s	+20%
`sign_verify`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify_internal`	LP64	cadical	✅	165s	omitted	new
	LP64	z3_no_bv_extract*	✅	407s	373s	+9%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	5s	4s	+25%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	31s	27s	+15%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	30s	29s	+3%
	LP64	z3*	✅	4s	4s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	32s	29s	+10%
	LP64	z3*	✅	1s	4s	-75%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`unpack_pk_t1`	LP64	bitwuzla	✅	14s	14s	+0%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk`	LP64	cadical	✅	32s	39s	-18%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	261s	251s	+4%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	252s	246s	+2%
	LP64	z3*	✅	4s	2s	+100%
`unpack_sk_t0hat`	LP64	cadical	✅	40s	38s	+5%
	LP64	z3*	✅	4s	2s	+100%
`use_hint`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	6s	3s	+100%
`yvec_get_poly`	LP64	bitwuzla	✅	34s	32s	+6%
	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	bitwuzla	✅	42s	41s	+2%
	LP64	z3*	✅	3s	3s	+0%

oqs-bot · 2026-11-03T03:59:19Z

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

* default.

Full Results (440 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1446s	1546s	-6.5%
`caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`compute_pack_t0_t1`	LP64	cadical	✅	37s	omitted	new
	LP64	z3_no_bv_extract*	✅	36s	41s	-12%
`decompose`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	24s	26s	-8%
	LP64	z3_smt_only	✅	20s	22s	-9%
`fqscale`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3	✅	2s	1s	+100%
`intt_native_aarch64`	LP64	bitwuzla	✅	20s	26s	-23%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	4s	2s	+100%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	20s	-10%
	LP64	z3*	✅	2s	3s	-33%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	4s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	6s	+17%
	LP64	cvc5_arrays_exp	✅	8s	7s	+14%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	1s	+200%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`keccak_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	3s	-67%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	13s	-8%
	LP64	z3*	✅	12s	12s	+0%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	cadical	✅	151s	omitted	new
	LP64	z3_no_bv_extract*	✅	198s	210s	-6%
`mld_check_pct`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	3s	3s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	34s	44s	-23%
	LP64	z3_no_bv_extract*	✅	5s	2s	+150%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	5s	2s	+150%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_no_bv_extract	✅	79s	93s	-15%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_h`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	1s	+200%
`mld_invntt_layer`	LP64	bitwuzla*	✅	62s	72s	-14%
	LP64	z3_smt_only	✅	70s	79s	-11%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	5s	4s	+25%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	12s	-8%
	LP64	z3_no_bv_extract	✅	113s	134s	-16%
`mld_ntt_layer`	LP64	bitwuzla*	✅	22s	28s	-21%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	51s	49s	+4%
	LP64	z3*	✅	5s	5s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	227s	242s	-6%
	LP64	z3*	✅	4s	6s	-33%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	1s	2s	-50%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	1s	1s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	20s	-10%
	LP64	z3*	✅	3s	2s	+50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	3s	4s	-25%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	2s	2s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	✅	16s	21s	-24%
	LP64	z3*	✅	3s	5s	-40%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	178s	210s	-15%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	92s	81s	+14%
	LP64	z3_smt_only*	✅	5s	4s	+25%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	75s	82s	-9%
	LP64	z3_smt_only*	✅	4s	5s	-20%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	19s	23s	-17%
	LP64	z3*	✅	3s	4s	-25%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	2s	3s	-33%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	20s	24s	-17%
	LP64	z3*	✅	2s	6s	-67%
`poly_add`	LP64	cadical	✅	47s	51s	-8%
	LP64	z3*	✅	14s	15s	-7%
`poly_caddq`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	19s	+0%
	LP64	z3*	✅	4s	5s	-20%
`poly_caddq_native`	LP64	bitwuzla	✅	95s	123s	-23%
	LP64	z3*	✅	5s	2s	+150%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	36s	35s	+3%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	105s	145s	-28%
	LP64	z3*	✅	3s	4s	-25%
`poly_challenge`	LP64	bitwuzla	✅	22s	26s	-15%
	LP64	z3*	✅	4s	1s	+300%
`poly_chknorm`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	8s	12s	-33%
	LP64	z3*	✅	6s	8s	-25%
`poly_chknorm_native`	LP64	bitwuzla	✅	5s	9s	-44%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	5s	1s	+400%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	7s	8s	-12%
	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	219s	250s	-12%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_native`	LP64	cadical	✅	16s	14s	+14%
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_native_x86_64`	LP64	cadical	✅	10s	9s	+11%
	LP64	z3*	✅	4s	3s	+33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	4s	2s	+100%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	152s	174s	-13%
	LP64	z3_smt_only*	✅	9s	7s	+29%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	45s	49s	-8%
	LP64	z3*	✅	2s	1s	+100%
`poly_ntt`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	1s	+100%
`poly_ntt_c`	LP64	bitwuzla	✅	43s	55s	-22%
	LP64	z3_smt_only*	✅	10s	13s	-23%
`poly_ntt_native`	LP64	bitwuzla	✅	25s	28s	-11%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	3s	5s	-40%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	180s	207s	-13%
	LP64	z3*	✅	74s	83s	-11%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	46s	55s	-16%
	LP64	z3*	✅	3s	2s	+50%
`poly_power2round`	LP64	bitwuzla	✅	241s	341s	-29%
	LP64	z3*	✅	3s	3s	+0%
`poly_reduce`	LP64	bitwuzla	✅	11s	9s	+22%
	LP64	z3*	✅	2s	2s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	9s	12s	-25%
	LP64	z3*	✅	2s	2s	+0%
`poly_sub`	LP64	bitwuzla	✅	12s	15s	-20%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform`	LP64	bitwuzla	✅	172s	200s	-14%
	LP64	z3*	✅	3s	1s	+200%
`poly_uniform_4x`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_eta`	LP64	bitwuzla	✅	50s	58s	-14%
	LP64	z3*	✅	4s	2s	+100%
`poly_uniform_eta_4x`	LP64	cadical	✅	53s	57s	-7%
	LP64	z3*	✅	10s	9s	+11%
`poly_uniform_gamma1`	LP64	cadical	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	23s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	11s	14s	-21%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	91s	84s	+8%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	29s	31s	-6%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	28s	32s	-12%
	LP64	z3*	✅	1s	2s	-50%
`polyeta_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	4s	6s	-33%
`polyt0_pack`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	3s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	7s	8s	-12%
`polyt1_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	cadical	✅	4s	omitted	new
	LP64	z3_no_bv_extract*	✅	2s	1s	+100%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	2s	omitted	new
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	38s	43s	-12%
	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	736s	828s	-11%
	LP64	z3*	✅	114s	139s	-18%
`polyveck_caddq`	LP64	cadical	✅	222s	271s	-18%
	LP64	z3*	✅	3s	4s	-25%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	168s	182s	-8%
	LP64	z3*	✅	4s	4s	+0%
`polyveck_invntt_tomont`	LP64	cadical	✅	178s	198s	-10%
	LP64	z3*	✅	3s	4s	-25%
`polyveck_ntt`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	4s	2s	+100%
`polyveck_reduce`	LP64	cadical	✅	170s	187s	-9%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	18s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_chknorm`	LP64	cadical	✅	69s	72s	-4%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_ntt`	LP64	cadical	✅	158s	169s	-7%
	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	3s	4s	-25%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	33s	36s	-8%
	LP64	z3*	✅	5s	4s	+25%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	32s	37s	-14%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	5s	2s	+150%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	4s	8s	-50%
	LP64	z3*	✅	3s	1s	+200%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_native`	LP64	bitwuzla	✅	26s	29s	-10%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	18s	-22%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	16s	17s	-6%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	14s	18s	-22%
`rej_uniform`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	11s	13s	-15%
`rej_uniform_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	9s	10s	-10%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	9s	9s	+0%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	3s	1s	+200%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3_smt_only*	✅	9s	12s	-25%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake128_release`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	3s	-33%
`shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`shake256_release`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	4s	2s	+100%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	bitwuzla	✅	1262s	1571s	-20%
	LP64	z3*	✅	18s	18s	+0%
`sign_keypair`	LP64	cadical	✅	438s	521s	-16%
	LP64	z3*	✅	4s	5s	-20%
`sign_keypair_internal`	LP64	cadical	✅	176s	188s	-6%
	LP64	z3_no_bv_extract*	✅	20s	18s	+11%
`sign_pk_from_sk`	LP64	cadical	✅	20s	omitted	new
	LP64	z3_no_bv_extract*	✅	53s	36s	+47%
`sign_signature`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	4s	-25%
`sign_signature_extmu`	LP64	cadical	✅	28s	33s	-15%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_internal`	LP64	cadical	✅	11s	omitted	new
	LP64	z3_no_bv_extract*	✅	14s	16s	-12%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	3s	5s	-40%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	13s	15s	-13%
	LP64	z3*	✅	5s	4s	+25%
`sign_verify`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	cadical	✅	57s	omitted	new
	LP64	z3_no_bv_extract*	✅	220s	247s	-11%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`unpack_pk_t1`	LP64	bitwuzla	✅	11s	10s	+10%
	LP64	z3*	✅	4s	3s	+33%
`unpack_sk`	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	cadical	✅	1s	4s	-75%
	LP64	z3*	✅	3s	3s	+0%
`use_hint`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%

oqs-bot · 2026-11-03T04:09:56Z

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	60s	35s	+71%

Full Results (440 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2263s	2071s	+9.3%
`caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
`compute_pack_t0_t1`	LP64	cadical	✅	241s	omitted	new
	LP64	z3_no_bv_extract*	✅	155s	136s	+14%
`decompose`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`fqmul`	LP64	bitwuzla*	✅	26s	25s	+4%
	LP64	z3_smt_only	✅	22s	20s	+10%
`fqscale`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	✅	24s	20s	+20%
	LP64	z3*	✅	2s	2s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	3s	2s	+50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	10s	7s	+43%
	LP64	z3	✅	1s	2s	-50%
`intt_native_x86_64`	LP64	bitwuzla	✅	20s	17s	+18%
	LP64	z3*	✅	2s	1s	+100%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
	LP64	z3*	✅	6s	5s	+20%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	5s	+40%
	LP64	cvc5_arrays_exp	✅	10s	6s	+67%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`keccak_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	4s	3s	+33%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	5s	-40%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	4s	3s	+33%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	12s	+8%
	LP64	z3*	✅	13s	13s	+0%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`make_hint`	LP64	cvc5_arrays_exp	✅	4s	5s	-20%
	LP64	z3*	✅	2s	1s	+100%
`mld_attempt_signature_generation`	LP64	cadical	✅	222s	omitted	new
	LP64	z3_no_bv_extract*	✅	213s	210s	+1%
`mld_check_pct`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	4s	7s	-43%
`mld_compute_pack_z`	LP64	cadical	✅	74s	69s	+7%
	LP64	z3_no_bv_extract*	✅	5s	4s	+25%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	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	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	2s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	✅	96s	77s	+25%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	2s	+100%
`mld_h`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	78s	62s	+26%
	LP64	z3_smt_only	✅	94s	80s	+18%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	3s	8s	-62%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	1s	1s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	13s	+0%
	LP64	z3_no_bv_extract	✅	172s	153s	+12%
`mld_ntt_layer`	LP64	bitwuzla*	✅	28s	25s	+12%
	LP64	z3_no_bv_extract	✅	3s	4s	-25%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	6s	-83%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	48s	47s	+2%
	LP64	z3*	✅	3s	3s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	240s	227s	+6%
	LP64	z3*	✅	4s	4s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	3s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	24s	20s	+20%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	3s	3s	+0%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	6s	+0%
	LP64	z3	✅	2s	3s	-33%
`ntt_native_x86_64`	LP64	bitwuzla	✅	21s	20s	+5%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	189s	174s	+9%
	LP64	z3*	✅	2s	4s	-50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`pack_sig_h`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`pack_sig_z`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	82s	76s	+8%
	LP64	z3_smt_only*	✅	3s	5s	-40%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	80s	78s	+3%
	LP64	z3_smt_only*	✅	7s	4s	+75%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	24s	22s	+9%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	1s	1s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	20s	+10%
	LP64	z3*	✅	2s	1s	+100%
`poly_add`	LP64	cadical	✅	53s	48s	+10%
	LP64	z3*	✅	19s	13s	+46%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	17s	+12%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	✅	127s	109s	+17%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	36s	31s	+16%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	146s	106s	+38%
	LP64	z3*	✅	3s	4s	-25%
`poly_challenge`	LP64	bitwuzla	✅	25s	22s	+14%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	1s	+200%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	12s	-17%
	LP64	z3*	✅	8s	8s	+0%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	9s	7s	+29%
	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	263s	226s	+16%
	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_native`	LP64	cadical	✅	16s	15s	+7%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_native_x86_64`	LP64	cadical	✅	14s	9s	+56%
	LP64	z3*	✅	5s	3s	+67%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	1s	4s	-75%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	177s	150s	+18%
	LP64	z3_smt_only*	✅	8s	6s	+33%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	45s	+4%
	LP64	z3*	✅	4s	1s	+300%
`poly_ntt`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_ntt_c`	LP64	bitwuzla	✅	58s	44s	+32%
	LP64	z3_smt_only*	✅	13s	10s	+30%
`poly_ntt_native`	LP64	bitwuzla	✅	27s	24s	+12%
	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	11s	8s	+38%
	LP64	z3*	✅	1s	2s	-50%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	210s	171s	+23%
	LP64	z3*	✅	52s	45s	+16%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	56s	57s	-2%
	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	bitwuzla	✅	361s	301s	+20%
	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	bitwuzla	✅	11s	8s	+38%
	LP64	z3*	✅	2s	2s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	13s	10s	+30%
	LP64	z3*	✅	2s	2s	+0%
`poly_sub`	LP64	bitwuzla	✅	17s	12s	+42%
	LP64	z3*	✅	1s	6s	-83%
`poly_uniform`	LP64	bitwuzla	✅	201s	175s	+15%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	cadical	✅	67s	58s	+16%
	LP64	z3*	✅	9s	9s	+0%
`poly_uniform_eta`	LP64	bitwuzla	✅	60s	53s	+13%
	LP64	z3*	✅	6s	3s	+100%
`poly_uniform_eta_4x`	LP64	cadical	✅	56s	53s	+6%
	LP64	z3*	✅	10s	11s	-9%
`poly_uniform_gamma1`	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	13s	11s	+18%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	25s	22s	+14%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	13s	13s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	86s	93s	-8%
	LP64	z3*	✅	3s	7s	-57%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	33s	28s	+18%
	LP64	z3*	✅	2s	6s	-67%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	28s	+7%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	4s	-75%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	2s	+200%
`polyt0_pack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	4s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	8s	8s	+0%
`polyt1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	cadical	✅	13s	omitted	new
	LP64	z3_no_bv_extract*	✅	89s	76s	+17%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	6s	omitted	new
	LP64	z3*	✅	17s	13s	+31%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	280s	243s	+15%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	427s	404s	+6%
	LP64	z3*	✅	10s	8s	+25%
`polyveck_caddq`	LP64	cadical	✅	229s	203s	+13%
	LP64	z3*	✅	3s	3s	+0%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	178s	170s	+5%
	LP64	z3*	✅	2s	4s	-50%
`polyveck_invntt_tomont`	LP64	cadical	✅	197s	179s	+10%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_ntt`	LP64	cadical	✅	203s	194s	+5%
	LP64	z3*	✅	5s	3s	+67%
`polyveck_reduce`	LP64	cadical	✅	4s	2s	+100%
	LP64	z3*	✅	1s	3s	-67%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	43s	38s	+13%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	21s	17s	+24%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_chknorm`	LP64	cadical	✅	74s	69s	+7%
	LP64	z3*	✅	3s	3s	+0%
`polyvecl_ntt`	LP64	cadical	✅	168s	158s	+6%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	121s	111s	+9%
	LP64	z3_smt_only*	✅	155s	143s	+8%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	122s	113s	+8%
	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	33s	33s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	31s	34s	-9%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	36s	33s	+9%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	35s	32s	+9%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	1s	+400%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	1s	+200%
`polyw1_unpack_88`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	1s	+100%
`polyz_pack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_native`	LP64	bitwuzla	✅	30s	27s	+11%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	15s	+13%
	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`reduce32`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	1s	+200%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	14s	11s	+27%
`rej_eta_native`	LP64	bitwuzla*	✅	5s	3s	+67%
	LP64	z3_smt_only	✅	17s	14s	+21%
`rej_uniform`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	7s	7s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	14s	10s	+40%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	2s	1s	+100%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	11s	10s	+10%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3_smt_only*	✅	11s	10s	+10%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`shake128_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`shake256`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	5s	2s	+150%
`shake256_absorb`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	4s	2s	+100%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	4s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_release`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	4s	3s	+33%
`sig_unpack_hints`	LP64	bitwuzla	✅	1581s	1243s	+27%
	LP64	z3*	✅	20s	17s	+18%
`sign_keypair`	LP64	cadical	✅	531s	391s	+36%
	LP64	z3*	✅	6s	8s	-25%
`sign_keypair_internal`	LP64	cadical	✅	189s	189s	+0%
	LP64	z3_no_bv_extract*	✅	19s	18s	+6%
`sign_pk_from_sk`	LP64	cadical	✅	21s	omitted	new
	LP64	z3_no_bv_extract*	⚠️	60s	35s	+71%
`sign_signature`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	6s	-33%
`sign_signature_extmu`	LP64	cadical	✅	31s	27s	+15%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_internal`	LP64	cadical	✅	221s	omitted	new
	LP64	z3_no_bv_extract*	✅	230s	177s	+30%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	14s	16s	-12%
	LP64	z3*	✅	4s	6s	-33%
`sign_verify`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
`sign_verify_internal`	LP64	cadical	✅	342s	omitted	new
	LP64	z3_no_bv_extract*	✅	496s	452s	+10%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	5s	2s	+150%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	39s	39s	+0%
	LP64	z3*	✅	2s	1s	+100%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	34s	33s	+3%
	LP64	z3*	✅	2s	1s	+100%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	37s	29s	+28%
	LP64	z3*	✅	4s	4s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	3s	2s	+50%
`unpack_pk_t1`	LP64	bitwuzla	✅	13s	11s	+18%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk`	LP64	cadical	✅	49s	45s	+9%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	89s	83s	+7%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	162s	154s	+5%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	89s	83s	+7%
	LP64	z3*	✅	2s	4s	-50%
`use_hint`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	35s	32s	+9%
	LP64	z3*	✅	4s	4s	+0%
`yvec_init`	LP64	bitwuzla	✅	11s	9s	+22%
	LP64	z3*	✅	1s	3s	-67%

oqs-bot · 2026-11-03T04:32:25Z

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

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	63s	33s	+91%

Full Results (440 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1473s	1426s	+3.3%
`caddq`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`compute_pack_t0_t1`	LP64	cadical	✅	42s	omitted	new
	LP64	z3_no_bv_extract*	✅	26s	29s	-10%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	26s	22s	+18%
	LP64	z3_smt_only	✅	20s	22s	-9%
`fqscale`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	20s	+10%
	LP64	z3*	✅	3s	3s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	1s	+200%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	5s	-40%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	3s	3s	+0%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	15s	+20%
	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	3s	6s	-50%
	LP64	cvc5_arrays_exp	✅	7s	7s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	4s	2s	+100%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	13s	-8%
	LP64	z3*	✅	13s	14s	-7%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	4s	-50%
`mld_attempt_signature_generation`	LP64	cadical	✅	205s	omitted	new
	LP64	z3_no_bv_extract*	✅	206s	190s	+8%
`mld_check_pct`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	6s	5s	+20%
`mld_compute_pack_z`	LP64	cadical	✅	35s	34s	+3%
	LP64	z3_no_bv_extract*	✅	6s	2s	+200%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	3s	2s	+50%
	ILP32	z3	✅	2s	1s	+100%
	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	3s	2s	+50%
`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	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	77s	80s	-4%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	63s	63s	+0%
	LP64	z3_smt_only	✅	70s	72s	-3%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	6s	3s	+100%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	12s	+8%
	LP64	z3_no_bv_extract	✅	108s	115s	-6%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	28s	-11%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	71s	72s	-1%
	LP64	z3*	✅	5s	7s	-29%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	539s	530s	+2%
	LP64	z3*	✅	4s	4s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	18s	+0%
	LP64	z3*	✅	4s	2s	+100%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	3s	2s	+50%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	2s	3s	-33%
`ntt_native_x86_64`	LP64	bitwuzla	✅	16s	19s	-16%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	176s	176s	+0%
	LP64	z3*	✅	1s	1s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`pack_sig_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_no_bv_extract*	✅	1s	4s	-75%
`pack_sig_z`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	2s	+0%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	87s	86s	+1%
	LP64	z3_smt_only*	✅	4s	5s	-20%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	87s	86s	+1%
	LP64	z3_smt_only*	✅	4s	4s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	20s	19s	+5%
	LP64	z3*	✅	3s	1s	+200%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	1s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	3s	3s	+0%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	2s	4s	-50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	23s	22s	+5%
	LP64	z3*	✅	1s	3s	-67%
`poly_add`	LP64	cadical	✅	46s	46s	+0%
	LP64	z3*	✅	14s	16s	-12%
`poly_caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	18s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native`	LP64	bitwuzla	✅	106s	93s	+14%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	33s	+3%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	110s	114s	-4%
	LP64	z3*	✅	1s	2s	-50%
`poly_challenge`	LP64	bitwuzla	✅	34s	31s	+10%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	4s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	8s	+25%
	LP64	z3*	✅	6s	7s	-14%
`poly_chknorm_native`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	9s	10s	-10%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	220s	199s	+11%
	LP64	z3*	✅	4s	5s	-20%
`poly_decompose_native`	LP64	cadical	✅	11s	12s	-8%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_native_x86_64`	LP64	cadical	✅	8s	7s	+14%
	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	141s	148s	-5%
	LP64	z3_smt_only*	✅	6s	5s	+20%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	43s	46s	-7%
	LP64	z3*	✅	4s	3s	+33%
`poly_ntt`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`poly_ntt_c`	LP64	bitwuzla	✅	46s	45s	+2%
	LP64	z3_smt_only*	✅	11s	9s	+22%
`poly_ntt_native`	LP64	bitwuzla	✅	24s	24s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	182s	165s	+10%
	LP64	z3*	✅	75s	71s	+6%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	55s	58s	-5%
	LP64	z3*	✅	2s	1s	+100%
`poly_power2round`	LP64	bitwuzla	✅	258s	241s	+7%
	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	bitwuzla	✅	6s	8s	-25%
	LP64	z3*	✅	1s	2s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	10s	9s	+11%
	LP64	z3*	✅	1s	4s	-75%
`poly_sub`	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	1s	2s	-50%
`poly_uniform`	LP64	bitwuzla	✅	165s	152s	+9%
	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_4x`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_eta`	LP64	bitwuzla	✅	77s	78s	-1%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_eta_4x`	LP64	cadical	✅	69s	61s	+13%
	LP64	z3*	✅	10s	8s	+25%
`poly_uniform_gamma1`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	4s	1s	+300%
	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	23s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	11s	12s	-8%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	84s	94s	-11%
	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	29s	27s	+7%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	28s	26s	+8%
	LP64	z3*	✅	3s	2s	+50%
`polyeta_pack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	7s	7s	+0%
`polyt0_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	7s	11s	-36%
`polyt1_pack`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	cadical	✅	2s	omitted	new
	LP64	z3_no_bv_extract*	✅	2s	1s	+100%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	1s	omitted	new
	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	43s	43s	+0%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	1239s	1232s	+1%
	LP64	z3*	✅	115s	115s	+0%
`polyveck_caddq`	LP64	cadical	✅	1186s	1206s	-2%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	195s	196s	-1%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_invntt_tomont`	LP64	cadical	✅	302s	301s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_ntt`	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`polyveck_reduce`	LP64	cadical	✅	246s	245s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	16s	16s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_chknorm`	LP64	cadical	✅	134s	136s	-1%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_ntt`	LP64	cadical	✅	180s	181s	-1%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	3s	1s	+200%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	46s	46s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	43s	45s	-4%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_88`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	5s	-20%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	2s	+100%
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	4s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	23s	27s	-15%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	13s	14s	-7%
	LP64	z3*	✅	2s	2s	+0%
`power2round`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	21s	20s	+5%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	14s	15s	-7%
`rej_uniform`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	12s	11s	+9%
`rej_uniform_c`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	10s	9s	+11%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	4s	1s	+300%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	10s	8s	+25%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	4s	-50%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3_smt_only*	✅	12s	10s	+20%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`shake128_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	1s	+100%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
`sig_unpack_hints`	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	19s	16s	+19%
`sign_keypair`	LP64	cadical	✅	500s	491s	+2%
	LP64	z3*	✅	5s	5s	+0%
`sign_keypair_internal`	LP64	cadical	✅	212s	212s	+0%
	LP64	z3_no_bv_extract*	✅	26s	23s	+13%
`sign_pk_from_sk`	LP64	cadical	✅	186s	omitted	new
	LP64	z3_no_bv_extract*	⚠️	63s	33s	+91%
`sign_signature`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	7s	-71%
`sign_signature_extmu`	LP64	cadical	✅	53s	52s	+2%
	LP64	z3*	✅	5s	3s	+67%
`sign_signature_internal`	LP64	cadical	✅	14s	omitted	new
	LP64	z3_no_bv_extract*	✅	13s	16s	-19%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	20s	23s	-13%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`sign_verify_internal`	LP64	cadical	✅	80s	omitted	new
	LP64	z3_no_bv_extract*	✅	252s	232s	+9%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	3s	+33%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	2s	+50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	2s	-50%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	2s	5s	-60%
`unpack_sk`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`use_hint`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%

oqs-bot · 2026-11-03T05:04:53Z

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	67s	38s	+76%

Full Results (440 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	3688s	3745s	-1.5%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`compute_pack_t0_t1`	LP64	cadical	✅	773s	omitted	new
	LP64	z3_no_bv_extract*	✅	268s	270s	-1%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`fqmul`	LP64	bitwuzla*	✅	23s	25s	-8%
	LP64	z3_smt_only	✅	24s	23s	+4%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	2s	+50%
`intt_native_aarch64`	LP64	bitwuzla	✅	23s	23s	+0%
	LP64	z3*	✅	1s	4s	-75%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	2s	3s	-33%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	1s	2s	-50%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	18s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	5s	-40%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	7s	-43%
	LP64	cvc5_arrays_exp	✅	8s	9s	-11%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`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*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`keccak_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	4s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	14s	14s	+0%
	LP64	z3*	✅	13s	11s	+18%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mld_attempt_signature_generation`	LP64	cadical	✅	270s	omitted	new
	LP64	z3_no_bv_extract*	✅	307s	362s	-15%
`mld_check_pct`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	6s	-33%
`mld_compute_pack_z`	LP64	cadical	✅	82s	84s	-2%
	LP64	z3_no_bv_extract*	✅	6s	6s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	2s	4s	-50%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`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	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	3s	-67%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	✅	85s	88s	-3%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
`mld_h`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	2s	+100%
`mld_invntt_layer`	LP64	bitwuzla*	✅	70s	70s	+0%
	LP64	z3_smt_only	✅	96s	95s	+1%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	3s	+67%
	LP64	z3*	✅	5s	3s	+67%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	13s	-8%
	LP64	z3_no_bv_extract	✅	169s	175s	-3%
`mld_ntt_layer`	LP64	bitwuzla*	✅	27s	26s	+4%
	LP64	z3_no_bv_extract	✅	4s	5s	-20%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	77s	76s	+1%
	LP64	z3*	✅	9s	6s	+50%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	549s	559s	-2%
	LP64	z3*	✅	5s	5s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	6s	-50%
`mld_sign_finish`	LP64	bitwuzla	✅	1s	6s	-83%
	LP64	z3*	✅	5s	4s	+25%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	2s	+100%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	4s	1s	+300%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	21s	-10%
	LP64	z3*	✅	4s	2s	+100%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	5s	-60%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	2s	1s	+100%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	4s	-75%
	LP64	cvc5_mbqi_enum	✅	5s	9s	-44%
	LP64	z3	✅	3s	1s	+200%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	18s	+6%
	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	198s	200s	-1%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_h`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	4s	-50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	91s	92s	-1%
	LP64	z3_smt_only*	✅	7s	4s	+75%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	97s	92s	+5%
	LP64	z3_smt_only*	✅	6s	5s	+20%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	10s	9s	+11%
	LP64	z3	✅	1s	3s	-67%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	5s	2s	+150%
	LP64	cvc5_mbqi_enum	✅	10s	10s	+0%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	4s	2s	+100%
`poly_add`	LP64	cadical	✅	61s	59s	+3%
	LP64	z3*	✅	15s	16s	-6%
`poly_caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	bitwuzla	✅	21s	20s	+5%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	✅	118s	119s	-1%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	36s	32s	+12%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	130s	130s	+0%
	LP64	z3*	✅	5s	4s	+25%
`poly_challenge`	LP64	bitwuzla	✅	37s	34s	+9%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm_c`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	10s	7s	+43%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	10s	-40%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	1s	+400%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	8s	8s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	197s	248s	-21%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_native`	LP64	cadical	✅	12s	14s	-14%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	cadical	✅	8s	10s	-20%
	LP64	z3*	✅	3s	1s	+200%
`poly_invntt_tomont`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	166s	168s	-1%
	LP64	z3_smt_only*	✅	7s	7s	+0%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	46s	+2%
	LP64	z3*	✅	4s	2s	+100%
`poly_ntt`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_ntt_c`	LP64	bitwuzla	✅	50s	52s	-4%
	LP64	z3_smt_only*	✅	16s	9s	+78%
`poly_ntt_native`	LP64	bitwuzla	✅	30s	28s	+7%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	14s	10s	+40%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	197s	198s	-1%
	LP64	z3*	✅	49s	56s	-12%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	52s	56s	-7%
	LP64	z3*	✅	4s	4s	+0%
`poly_power2round`	LP64	bitwuzla	✅	335s	337s	-1%
	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	bitwuzla	✅	10s	8s	+25%
	LP64	z3*	✅	3s	3s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	3s	3s	+0%
`poly_sub`	LP64	bitwuzla	✅	15s	14s	+7%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform`	LP64	bitwuzla	✅	191s	166s	+15%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_4x`	LP64	cadical	✅	62s	62s	+0%
	LP64	z3*	✅	6s	7s	-14%
`poly_uniform_eta`	LP64	bitwuzla	✅	79s	82s	-4%
	LP64	z3*	✅	4s	3s	+33%
`poly_uniform_eta_4x`	LP64	cadical	✅	73s	66s	+11%
	LP64	z3*	✅	11s	10s	+10%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	13s	12s	+8%
	LP64	z3*	✅	4s	2s	+100%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	25s	23s	+9%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	15s	11s	+36%
	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	95s	83s	+14%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	30s	30s	+0%
	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	31s	32s	-3%
	LP64	z3*	✅	1s	3s	-67%
`polyeta_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyeta_unpack`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	8s	5s	+60%
`polyt0_pack`	LP64	bitwuzla	✅	8s	5s	+60%
	LP64	z3*	✅	3s	1s	+200%
`polyt0_unpack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	8s	8s	+0%
`polyt1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	6s	4s	+50%
`polyvec_matrix_expand`	LP64	cadical	✅	20s	omitted	new
	LP64	z3_no_bv_extract*	✅	124s	115s	+8%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	14s	omitted	new
	LP64	z3*	✅	25s	24s	+4%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	590s	595s	-1%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	780s	782s	-0%
	LP64	z3*	✅	11s	9s	+22%
`polyveck_caddq`	LP64	cadical	✅	1224s	1243s	-2%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	208s	210s	-1%
	LP64	z3*	✅	4s	5s	-20%
`polyveck_invntt_tomont`	LP64	cadical	✅	320s	327s	-2%
	LP64	z3*	✅	4s	3s	+33%
`polyveck_ntt`	LP64	cadical	✅	1078s	1086s	-1%
	LP64	z3*	✅	4s	2s	+100%
`polyveck_reduce`	LP64	cadical	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	54s	54s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	21s	-14%
	LP64	z3*	✅	3s	5s	-40%
`polyvecl_chknorm`	LP64	cadical	✅	141s	168s	-16%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_ntt`	LP64	cadical	✅	228s	195s	+17%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	13s	14s	-7%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	155s	156s	-1%
	LP64	z3_smt_only*	✅	271s	316s	-14%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	170s	185s	-8%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	78s	77s	+1%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	50s	48s	+4%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	48s	45s	+7%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	47s	47s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	1s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	4s	+25%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	25s	27s	-7%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	18s	-6%
	LP64	z3*	✅	3s	2s	+50%
`power2round`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	1s	2s	-50%
`reduce32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	5s	3s	+67%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	19s	19s	+0%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	18s	16s	+12%
`rej_uniform`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	7s	7s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	10s	13s	-23%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	4s	2s	+100%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	10s	11s	-9%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	6s	3s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	8s	-50%
	LP64	z3_smt_only*	✅	11s	12s	-8%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3	✅	2s	2s	+0%
`shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	2s	1s	+100%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	4s	-25%
`shake256_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	1s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	4s	3s	+33%
`sig_unpack_hints`	LP64	bitwuzla	✅	26s	26s	+0%
	LP64	z3*	✅	16s	18s	-11%
`sign_keypair`	LP64	cadical	✅	625s	631s	-1%
	LP64	z3*	✅	4s	5s	-20%
`sign_keypair_internal`	LP64	cadical	✅	223s	224s	-0%
	LP64	z3_no_bv_extract*	✅	21s	26s	-19%
`sign_pk_from_sk`	LP64	cadical	✅	196s	omitted	new
	LP64	z3_no_bv_extract*	⚠️	67s	38s	+76%
`sign_signature`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_extmu`	LP64	cadical	✅	58s	61s	-5%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_internal`	LP64	cadical	✅	541s	omitted	new
	LP64	z3_no_bv_extract*	✅	452s	453s	-0%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	27s	25s	+8%
	LP64	z3*	✅	7s	5s	+40%
`sign_verify`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`sign_verify_internal`	LP64	cadical	✅	697s	omitted	new
	LP64	z3_no_bv_extract*	✅	1304s	1318s	-1%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	34s	34s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	35s	34s	+3%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	35s	35s	+0%
	LP64	z3*	✅	3s	4s	-25%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`unpack_pk_t1`	LP64	bitwuzla	✅	11s	11s	+0%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk`	LP64	cadical	✅	67s	79s	-15%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	89s	91s	-2%
	LP64	z3*	✅	1s	1s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	319s	315s	+1%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	cadical	✅	113s	115s	-2%
	LP64	z3*	✅	3s	3s	+0%
`use_hint`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	2s	+100%
`yvec_get_poly`	LP64	bitwuzla	✅	40s	40s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_init`	LP64	bitwuzla	✅	17s	16s	+6%
	LP64	z3*	✅	5s	4s	+25%

With the loop contracts, the matrix entries sampled in each iteration are havocked at a symbolic offset into mld_polymat_eager, which makes the propositional encoding very large. For cadical only, fully unroll the sampling loops instead, so that each entry is written at a constant offset. Unwinding assertions check that the bounds cover all parameter sets. Also pass --no-forall-skolemization for cadical. The z3 configurations and the code are unchanged. Add cadical as a second solver for polyvec_matrix_expand and polyvec_matrix_expand_serial. Locally for ML-DSA-87, they take about 30s and 20s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Replace the combined NULL check of the seven allocations by one check per allocation. With the instrumented malloc/free, the combined check made the propositional encoding of the sign_pk_from_sk proof too large for cadical. Locally for ML-DSA-87, the proof now takes about 220s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer · 2026-11-03T11:45:01Z

Opened a CBMC issue for the issue identified here: diffblue/cbmc#9387

mkannwischer added 6 commits November 3, 2026 10:12

CBMC: Add CaDiCaL as a second solver for sign_signature_internal

07608b1

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-87, sign_signature_internal then takes about 560s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

CBMC: Add CaDiCaL as a second solver for attempt_signature_generation

fce7648

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-87, attempt_signature_generation then takes about 420s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

CBMC: Add CaDiCaL as a second solver for compute_pack_t0_t1

6323348

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-87, compute_pack_t0_t1 then takes about 750s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

CBMC: Add CaDiCaL as a second solver for sign_verify_internal

e55c4a7

Pass --no-forall-skolemization for cadical only. Locally for ML-DSA-44, sign_verify_internal then takes about 210s with cadical. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

CBMC: Add CaDiCaL as a second solver for sign_pk_from_sk

52fbe60

Pass --no-forall-skolemization for cadical only. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer changed the title ~~CBMC: Add CaDiCaL as a second solver for sign_signature_internal~~ CBMC: Add CaDiCaL as a second solver for sign_signature_internal (malloc) Nov 3, 2026

mkannwischer added 2 commits November 3, 2026 18:33

mkannwischer mentioned this pull request Nov 3, 2026

CBMC: Add CaDiCaL as a second solver for polyvec_matrix_expand(_serial) #1515

Closed

mkannwischer changed the title ~~CBMC: Add CaDiCaL as a second solver for sign_signature_internal (malloc)~~ CBMC: Add CaDiCaL as a second solver for all remaining proofs Nov 3, 2026

mkannwischer mentioned this pull request Nov 3, 2026

SAT back end: asserted forall handed over from an ensures is very expensive diffblue/cbmc#9387

Open

This was referenced Nov 3, 2026

CBMC: Work around quantifier skolemization to add CaDiCaL for 7 proofs #1523

Open

CBMC: Add CaDiCaL as second solver for five top level proofs (stack alloc) #1522

Closed

mkannwischer added the DO-NOT-MERGE label Nov 3, 2026

This was referenced Nov 5, 2026

CBMC: Discharge every CBMC proof with at least two solvers #1527

Open

SOUNDNESS.md: Document CBMC proofs discharged by a single solver #1528

Open

Navigation Menu

Repository navigation

CBMC: Add CaDiCaL as a second solver for all remaining proofs - #1521

CBMC: Add CaDiCaL as a second solver for all remaining proofs#1521
mkannwischer wants to merge 8 commits into
mainfrom
cbmc-no-forall-skolemization

mkannwischer commented Nov 3, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Nov 3, 2026 •

edited

Loading

Uh oh!

mkannwischer commented Nov 3, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mkannwischer commented Nov 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Nov 3, 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 Nov 3, 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 Nov 3, 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 Nov 3, 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 Nov 3, 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 Nov 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

mkannwischer commented Nov 3, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

mkannwischer commented Nov 3, 2026 •

edited

Loading

oqs-bot commented Nov 3, 2026 •

edited

Loading

oqs-bot commented Nov 3, 2026 •

edited

Loading

oqs-bot commented Nov 3, 2026 •

edited

Loading

oqs-bot commented Nov 3, 2026 •

edited

Loading

oqs-bot commented Nov 3, 2026 •

edited

Loading

oqs-bot commented Nov 3, 2026 •

edited

Loading