CBMC: Add CaDiCaL as a second solver for polyvec_matrix_expand(_serial) by mkannwischer · Pull Request #1515 · pq-code-package/mldsa-native

mkannwischer · 2026-10-30T09:42:40Z

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. The z3 configurations and the code are unchanged.

Add cadical as a second solver for polyvec_matrix_expand and polyvec_matrix_expand_serial.

oqs-bot · 2026-10-30T10:55:29Z

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

* default.

Full Results (435 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1407s	1577s	-10.8%
`caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	31s	37s	-16%
`decompose`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`fqmul`	LP64	bitwuzla*	✅	25s	27s	-7%
	LP64	z3_smt_only	✅	19s	21s	-10%
`fqscale`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	3s	-67%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	27s	-19%
	LP64	z3*	✅	3s	2s	+50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	2s	+0%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	1s	1s	+0%
`intt_native_x86_64`	LP64	bitwuzla	✅	16s	21s	-24%
	LP64	z3*	✅	2s	3s	-33%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	6s	4s	+50%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	5s	+20%
	LP64	cvc5_arrays_exp	✅	6s	7s	-14%
`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*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	4s	-50%
`keccak_init`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	3s	-33%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	14s	-14%
	LP64	z3*	✅	11s	12s	-8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	4s	-75%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	140s	178s	-21%
`mld_check_pct`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	6s	5s	+20%
`mld_compute_pack_z`	LP64	cadical	✅	38s	41s	-7%
	LP64	z3_no_bv_extract*	✅	5s	4s	+25%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	4s	-25%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	1s	+100%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	79s	99s	-20%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	64s	75s	-15%
	LP64	z3_smt_only	✅	70s	86s	-19%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	5s	3s	+67%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	14s	+0%
	LP64	z3_no_bv_extract	✅	116s	139s	-17%
`mld_ntt_layer`	LP64	bitwuzla*	✅	28s	30s	-7%
	LP64	z3_no_bv_extract	✅	4s	4s	+0%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	28s	38s	-26%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	90s	93s	-3%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_finish`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	25s	-28%
	LP64	z3*	✅	2s	1s	+100%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	2s	2s	+0%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	2s	3s	-33%
`ntt_native_x86_64`	LP64	bitwuzla	✅	18s	21s	-14%
	LP64	z3*	✅	3s	5s	-40%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	180s	196s	-8%
	LP64	z3*	✅	2s	4s	-50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	4s	-25%
`pack_sig_h`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
`pack_sig_z`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	56s	63s	-11%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	55s	60s	-8%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	22s	26s	-15%
	LP64	z3*	✅	4s	3s	+33%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	1s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	5s	4s	+25%
	LP64	cvc5_mbqi_enum	✅	10s	9s	+11%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	23s	24s	-4%
	LP64	z3*	✅	2s	3s	-33%
`poly_add`	LP64	cadical	✅	46s	66s	-30%
	LP64	z3*	✅	13s	16s	-19%
`poly_caddq`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	26s	-27%
	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native`	LP64	bitwuzla	✅	112s	117s	-4%
	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	39s	-13%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	122s	150s	-19%
	LP64	z3*	✅	3s	2s	+50%
`poly_challenge`	LP64	bitwuzla	✅	24s	30s	-20%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	8s	8s	+0%
	LP64	z3*	✅	10s	10s	+0%
`poly_chknorm_native`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	1s	1s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	2s	+100%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	219s	259s	-15%
	LP64	z3*	✅	4s	4s	+0%
`poly_decompose_native`	LP64	cadical	✅	18s	14s	+29%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_native_x86_64`	LP64	cadical	✅	8s	11s	-27%
	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	150s	188s	-20%
	LP64	z3_smt_only*	✅	8s	7s	+14%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	51s	-8%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	✅	45s	58s	-22%
	LP64	z3_smt_only*	✅	12s	12s	+0%
`poly_ntt_native`	LP64	bitwuzla	✅	27s	31s	-13%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	8s	13s	-38%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	188s	224s	-16%
	LP64	z3*	✅	77s	93s	-17%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	53s	54s	-2%
	LP64	z3*	✅	2s	2s	+0%
`poly_power2round`	LP64	bitwuzla	✅	295s	324s	-9%
	LP64	z3*	✅	3s	2s	+50%
`poly_reduce`	LP64	bitwuzla	✅	8s	11s	-27%
	LP64	z3*	✅	1s	1s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	3s	2s	+50%
`poly_sub`	LP64	bitwuzla	✅	14s	17s	-18%
	LP64	z3*	✅	4s	2s	+100%
`poly_uniform`	LP64	bitwuzla	✅	182s	214s	-15%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_4x`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_eta`	LP64	bitwuzla	✅	77s	91s	-15%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_eta_4x`	LP64	cadical	✅	59s	80s	-26%
	LP64	z3*	✅	7s	10s	-30%
`poly_uniform_gamma1`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	22s	27s	-19%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	15s	-20%
	LP64	z3*	✅	1s	4s	-75%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	95s	91s	+4%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	31s	39s	-21%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	33s	37s	-11%
	LP64	z3*	✅	2s	5s	-60%
`polyeta_pack`	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	2s	1s	+100%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	8s	9s	-11%
`polyt0_pack`	LP64	bitwuzla	✅	4s	8s	-50%
	LP64	z3*	✅	4s	2s	+100%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	7s	7s	+0%
`polyt1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_matrix_expand`	LP64	cadical	✅	2s	omitted	new
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	2s	omitted	new
	LP64	z3*	✅	2s	2s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	39s	39s	+0%
	LP64	z3_no_bv_extract*	✅	3s	4s	-25%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	459s	503s	-9%
	LP64	z3*	✅	104s	120s	-13%
`polyveck_caddq`	LP64	cadical	✅	102s	109s	-6%
	LP64	z3*	✅	1s	4s	-75%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	105s	113s	-7%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_invntt_tomont`	LP64	cadical	✅	138s	147s	-6%
	LP64	z3*	✅	2s	4s	-50%
`polyveck_ntt`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	5s	-80%
`polyveck_reduce`	LP64	cadical	✅	110s	119s	-8%
	LP64	z3*	✅	1s	3s	-67%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	14s	18s	-22%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_chknorm`	LP64	cadical	✅	58s	57s	+2%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_ntt`	LP64	cadical	✅	137s	123s	+11%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3_smt_only*	✅	2s	4s	-50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	30s	34s	-12%
	LP64	z3*	✅	1s	1s	+0%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	28s	28s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyz_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	1s	+200%
`polyz_unpack`	LP64	bitwuzla	✅	5s	7s	-29%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	6s	6s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	24s	31s	-23%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	15s	18s	-17%
	LP64	z3*	✅	3s	4s	-25%
`power2round`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`reduce32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	20s	28s	-29%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	16s	17s	-6%
`rej_uniform`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	13s	11s	+18%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	9s	10s	-10%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3_smt_only*	✅	1s	2s	-50%
`rej_uniform_native`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	8s	10s	-20%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3_smt_only*	✅	9s	13s	-31%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	1s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`shake128_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	5s	2s	+150%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	3s	-67%
`shake256`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`shake256_release`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	1s	+100%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	bitwuzla	✅	54s	62s	-13%
	LP64	z3*	✅	38s	43s	-12%
`sign_keypair`	LP64	cadical	✅	46s	57s	-19%
	LP64	z3*	✅	6s	3s	+100%
`sign_keypair_internal`	LP64	cadical	✅	147s	155s	-5%
	LP64	z3_no_bv_extract*	✅	13s	13s	+0%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	30s	35s	-14%
`sign_signature`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	4s	-50%
`sign_signature_extmu`	LP64	cadical	✅	20s	30s	-33%
	LP64	z3*	✅	2s	4s	-50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	14s	17s	-18%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	13s	13s	+0%
	LP64	z3*	✅	5s	5s	+0%
`sign_verify`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
`sign_verify_extmu`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	272s	313s	-13%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	1s	+100%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	1s	+200%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	11s	12s	-8%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`use_hint`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	1s	+200%
`yvec_init`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-10-30T10:59:54Z

CBMC Results (ML-DSA-44)

* default.

Full Results (435 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2222s	2164s	+2.7%
`caddq`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	4s	-25%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	104s	89s	+17%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	27s	22s	+23%
	LP64	z3_smt_only	✅	23s	22s	+5%
`fqscale`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`intt_native_aarch64`	LP64	bitwuzla	✅	23s	27s	-15%
	LP64	z3*	✅	2s	3s	-33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	3s	1s	+200%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	3s	1s	+200%
`intt_native_x86_64`	LP64	bitwuzla	✅	21s	18s	+17%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	4s	+50%
	LP64	cvc5_arrays_exp	✅	8s	9s	-11%
`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*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	4s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccak_init`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	4s	3s	+33%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	14s	13s	+8%
	LP64	z3*	✅	12s	12s	+0%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	6s	3s	+100%
`make_hint`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	385s	420s	-8%
`mld_check_pct`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	6s	5s	+20%
`mld_compute_pack_z`	LP64	cadical	✅	68s	64s	+6%
	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	1s	+100%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	ILP32	z3	✅	2s	1s	+100%
	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	97s	86s	+13%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	74s	61s	+21%
	LP64	z3_smt_only	✅	106s	97s	+9%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	6s	-17%
	LP64	z3*	✅	4s	4s	+0%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	13s	+0%
	LP64	z3_no_bv_extract	✅	189s	152s	+24%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	24s	+4%
	LP64	z3_no_bv_extract	✅	3s	4s	-25%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	2s	+150%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	3s	+100%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	37s	30s	+23%
	LP64	z3*	✅	4s	3s	+33%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	95s	86s	+10%
	LP64	z3*	✅	1s	4s	-75%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	7s	3s	+133%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	bitwuzla	✅	24s	22s	+9%
	LP64	z3*	✅	2s	2s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	6s	5s	+20%
	LP64	z3	✅	3s	1s	+200%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	3s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	17s	+12%
	LP64	z3*	✅	2s	4s	-50%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	216s	187s	+16%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	4s	4s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	61s	58s	+5%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	58s	54s	+7%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	25s	20s	+25%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	1s	2s	-50%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	1s	2s	-50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	24s	23s	+4%
	LP64	z3*	✅	3s	2s	+50%
`poly_add`	LP64	cadical	✅	62s	46s	+35%
	LP64	z3*	✅	15s	14s	+7%
`poly_caddq`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_caddq_c`	LP64	bitwuzla	✅	24s	19s	+26%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	bitwuzla	✅	129s	116s	+11%
	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	40s	35s	+14%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	146s	117s	+25%
	LP64	z3*	✅	1s	2s	-50%
`poly_challenge`	LP64	bitwuzla	✅	29s	26s	+12%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	5s	3s	+67%
`poly_chknorm_c`	LP64	bitwuzla	✅	13s	9s	+44%
	LP64	z3*	✅	8s	7s	+14%
`poly_chknorm_native`	LP64	bitwuzla	✅	8s	6s	+33%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	255s	189s	+35%
	LP64	z3*	✅	4s	3s	+33%
`poly_decompose_native`	LP64	cadical	✅	17s	14s	+21%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_native_x86_64`	LP64	cadical	✅	9s	10s	-10%
	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	187s	168s	+11%
	LP64	z3_smt_only*	✅	9s	7s	+29%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	50s	47s	+6%
	LP64	z3*	✅	3s	4s	-25%
`poly_ntt`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	bitwuzla	✅	59s	53s	+11%
	LP64	z3_smt_only*	✅	11s	9s	+22%
`poly_ntt_native`	LP64	bitwuzla	✅	30s	25s	+20%
	LP64	z3*	✅	4s	2s	+100%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	11s	8s	+38%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	192s	184s	+4%
	LP64	z3*	✅	55s	51s	+8%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	55s	51s	+8%
	LP64	z3*	✅	3s	1s	+200%
`poly_power2round`	LP64	bitwuzla	✅	329s	306s	+8%
	LP64	z3*	✅	4s	3s	+33%
`poly_reduce`	LP64	bitwuzla	✅	10s	8s	+25%
	LP64	z3*	✅	2s	2s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_sub`	LP64	bitwuzla	✅	17s	17s	+0%
	LP64	z3*	✅	5s	4s	+25%
`poly_uniform`	LP64	bitwuzla	✅	201s	183s	+10%
	LP64	z3*	✅	4s	2s	+100%
`poly_uniform_4x`	LP64	cadical	✅	64s	60s	+7%
	LP64	z3*	✅	10s	8s	+25%
`poly_uniform_eta`	LP64	bitwuzla	✅	92s	76s	+21%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_eta_4x`	LP64	cadical	✅	64s	61s	+5%
	LP64	z3*	✅	11s	8s	+38%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	13s	9s	+44%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	25s	24s	+4%
	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	15s	15s	+0%
	LP64	z3*	✅	5s	1s	+400%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	93s	100s	-7%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	37s	33s	+12%
	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	38s	32s	+19%
	LP64	z3*	✅	3s	4s	-25%
`polyeta_pack`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	1s	4s	-75%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	5s	-20%
`polyt0_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	8s	7s	+14%
`polyt1_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	2s	-50%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`polyvec_matrix_expand`	LP64	cadical	✅	8s	omitted	new
	LP64	z3_no_bv_extract*	✅	15s	13s	+15%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	4s	omitted	new
	LP64	z3*	✅	6s	4s	+50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	103s	100s	+3%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	246s	233s	+6%
	LP64	z3*	✅	7s	6s	+17%
`polyveck_caddq`	LP64	cadical	✅	109s	100s	+9%
	LP64	z3*	✅	3s	3s	+0%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	111s	133s	-17%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_invntt_tomont`	LP64	cadical	✅	146s	135s	+8%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_ntt`	LP64	cadical	✅	121s	113s	+7%
	LP64	z3*	✅	2s	1s	+100%
`polyveck_reduce`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	27s	28s	-4%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	17s	18s	-6%
	LP64	z3*	✅	3s	3s	+0%
`polyvecl_chknorm`	LP64	cadical	✅	55s	51s	+8%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_ntt`	LP64	cadical	✅	130s	110s	+18%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	5s	5s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	95s	104s	-9%
	LP64	z3_smt_only*	✅	187s	174s	+7%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	175s	166s	+5%
	LP64	z3_smt_only*	✅	2s	4s	-50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	41s	39s	+5%
	LP64	z3*	✅	3s	4s	-25%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	40s	40s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	33s	33s	+0%
	LP64	z3*	✅	3s	5s	-40%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	28s	25s	+12%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	3s	-67%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_pack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	5s	-40%
`polyz_unpack`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	6s	5s	+20%
`polyz_unpack_native`	LP64	bitwuzla	✅	28s	24s	+17%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	12s	+42%
	LP64	z3*	✅	4s	3s	+33%
`power2round`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`reduce32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	4s	2s	+100%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	21s	16s	+31%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	17s	13s	+31%
`rej_uniform`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	8s	8s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	10s	9s	+11%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	9s	10s	-10%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3_smt_only*	✅	14s	10s	+40%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`shake128_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`shake128_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	1s	+200%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	1s	+200%
`shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_absorb`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	4s	1s	+300%
`shake256_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	1s	+100%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	3s	-33%
`sig_unpack_hints`	LP64	bitwuzla	✅	57s	53s	+8%
	LP64	z3*	✅	30s	29s	+3%
`sign_keypair`	LP64	cadical	✅	52s	55s	-5%
	LP64	z3*	✅	6s	5s	+20%
`sign_keypair_internal`	LP64	cadical	✅	155s	146s	+6%
	LP64	z3_no_bv_extract*	✅	15s	16s	-6%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	33s	29s	+14%
`sign_signature`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	5s	4s	+25%
`sign_signature_extmu`	LP64	cadical	✅	21s	21s	+0%
	LP64	z3*	✅	2s	3s	-33%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	276s	239s	+15%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	7s	2s	+250%
	LP64	z3*	✅	2s	2s	+0%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	13s	14s	-7%
	LP64	z3*	✅	5s	4s	+25%
`sign_verify`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	377s	390s	-3%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	2s	4s	-50%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	33s	29s	+14%
	LP64	z3*	✅	5s	4s	+25%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	33s	30s	+10%
	LP64	z3*	✅	2s	3s	-33%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	3s	1s	+200%
`unpack_sk`	LP64	cadical	✅	34s	35s	-3%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	260s	254s	+2%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	259s	244s	+6%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_t0hat`	LP64	cadical	✅	41s	37s	+11%
	LP64	z3*	✅	3s	3s	+0%
`use_hint`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	bitwuzla	✅	35s	35s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_init`	LP64	bitwuzla	✅	41s	37s	+11%
	LP64	z3*	✅	3s	3s	+0%

oqs-bot · 2026-10-30T11:01:10Z

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

* default.

Full Results (435 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1490s	1555s	-4.2%
`caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	37s	43s	-14%
`decompose`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	1s	+200%
`fqmul`	LP64	bitwuzla*	✅	26s	26s	+0%
	LP64	z3_smt_only	✅	20s	21s	-5%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	bitwuzla	✅	24s	25s	-4%
	LP64	z3*	✅	3s	3s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	3s	2s	+50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	17s	19s	-11%
	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	9s	11s	-18%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`keccak_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	13s	+0%
	LP64	z3*	✅	13s	13s	+0%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	203s	217s	-6%
`mld_check_pct`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	5s	8s	-38%
`mld_compute_pack_z`	LP64	cadical	✅	36s	36s	+0%
	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	1s	+200%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	4s	2s	+100%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	2s	+50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	87s	92s	-5%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`mld_h`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	66s	77s	-14%
	LP64	z3_smt_only	✅	73s	89s	-18%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	5s	+0%
	LP64	z3*	✅	5s	2s	+150%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	13s	-8%
	LP64	z3_no_bv_extract	✅	119s	129s	-8%
`mld_ntt_layer`	LP64	bitwuzla*	✅	26s	26s	+0%
	LP64	z3_no_bv_extract	✅	4s	4s	+0%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	47s	48s	-2%
	LP64	z3*	✅	3s	3s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	234s	240s	-3%
	LP64	z3*	✅	4s	4s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	4s	2s	+100%
`mld_sign_finish`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	✅	23s	20s	+15%
	LP64	z3*	✅	3s	3s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	2s	3s	-33%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	7s	5s	+40%
	LP64	z3	✅	4s	2s	+100%
`ntt_native_x86_64`	LP64	bitwuzla	✅	21s	22s	-5%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	189s	206s	-8%
	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	6s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	79s	80s	-1%
	LP64	z3_smt_only*	✅	5s	5s	+0%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	79s	80s	-1%
	LP64	z3_smt_only*	✅	4s	2s	+100%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	20s	22s	-9%
	LP64	z3*	✅	4s	1s	+300%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	21s	24s	-12%
	LP64	z3*	✅	3s	2s	+50%
`poly_add`	LP64	cadical	✅	50s	50s	+0%
	LP64	z3*	✅	15s	15s	+0%
`poly_caddq`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	6s	1s	+500%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	22s	-18%
	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native`	LP64	bitwuzla	✅	114s	121s	-6%
	LP64	z3*	✅	4s	1s	+300%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	33s	34s	-3%
	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	125s	139s	-10%
	LP64	z3*	✅	2s	3s	-33%
`poly_challenge`	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	10s	-10%
	LP64	z3*	✅	7s	7s	+0%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	8s	-25%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	6s	2s	+200%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	9s	8s	+12%
	LP64	z3*	✅	4s	3s	+33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	238s	262s	-9%
	LP64	z3*	✅	4s	4s	+0%
`poly_decompose_native`	LP64	cadical	✅	14s	12s	+17%
	LP64	z3*	✅	5s	1s	+400%
`poly_decompose_native_x86_64`	LP64	cadical	✅	8s	10s	-20%
	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	150s	170s	-12%
	LP64	z3_smt_only*	✅	5s	8s	-38%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	45s	50s	-10%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_ntt_c`	LP64	bitwuzla	✅	53s	56s	-5%
	LP64	z3_smt_only*	✅	12s	12s	+0%
`poly_ntt_native`	LP64	bitwuzla	✅	29s	27s	+7%
	LP64	z3*	✅	4s	1s	+300%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	8s	11s	-27%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	181s	208s	-13%
	LP64	z3*	✅	81s	87s	-7%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	53s	55s	-4%
	LP64	z3*	✅	4s	2s	+100%
`poly_power2round`	LP64	bitwuzla	✅	320s	338s	-5%
	LP64	z3*	✅	5s	3s	+67%
`poly_reduce`	LP64	bitwuzla	✅	8s	7s	+14%
	LP64	z3*	✅	2s	1s	+100%
`poly_shiftl`	LP64	bitwuzla	✅	11s	13s	-15%
	LP64	z3*	✅	3s	4s	-25%
`poly_sub`	LP64	bitwuzla	✅	14s	16s	-12%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform`	LP64	bitwuzla	✅	185s	206s	-10%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_4x`	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_eta`	LP64	bitwuzla	✅	56s	61s	-8%
	LP64	z3*	✅	5s	3s	+67%
`poly_uniform_eta_4x`	LP64	cadical	✅	55s	59s	-7%
	LP64	z3*	✅	10s	9s	+11%
`poly_uniform_gamma1`	LP64	cadical	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	24s	25s	-4%
	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	✅	94s	86s	+9%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	29s	32s	-9%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	30s	33s	-9%
	LP64	z3*	✅	3s	2s	+50%
`polyeta_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyt0_pack`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	2s	2s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	8s	10s	-20%
`polyt1_pack`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_expand`	LP64	cadical	✅	3s	omitted	new
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	2s	omitted	new
	LP64	z3*	✅	1s	4s	-75%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	41s	44s	-7%
	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	826s	816s	+1%
	LP64	z3*	✅	133s	139s	-4%
`polyveck_caddq`	LP64	cadical	✅	217s	226s	-4%
	LP64	z3*	✅	3s	3s	+0%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	175s	218s	-20%
	LP64	z3*	✅	3s	4s	-25%
`polyveck_invntt_tomont`	LP64	cadical	✅	188s	192s	-2%
	LP64	z3*	✅	5s	4s	+25%
`polyveck_ntt`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyveck_reduce`	LP64	cadical	✅	179s	181s	-1%
	LP64	z3*	✅	3s	1s	+200%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	2s	6s	-67%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	18s	+6%
	LP64	z3*	✅	2s	1s	+100%
`polyvecl_chknorm`	LP64	cadical	✅	70s	73s	-4%
	LP64	z3*	✅	4s	1s	+300%
`polyvecl_ntt`	LP64	cadical	✅	159s	168s	-5%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	1s	2s	-50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	34s	33s	+3%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	34s	32s	+6%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack_32`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	5s	4s	+25%
`polyz_unpack_native`	LP64	bitwuzla	✅	28s	27s	+4%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	16s	+0%
	LP64	z3*	✅	3s	2s	+50%
`power2round`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
`reduce32`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	4s	3s	+33%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	17s	19s	-11%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	14s	14s	+0%
`rej_uniform`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	12s	13s	-8%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	8s	11s	-27%
`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	4s	-75%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	9s	10s	-10%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	4s	2s	+100%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3_smt_only*	✅	12s	14s	-14%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`shake128_release`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	2s	1s	+100%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	1s	+100%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	✅	1407s	1489s	-6%
	LP64	z3*	✅	17s	17s	+0%
`sign_keypair`	LP64	cadical	✅	454s	496s	-8%
	LP64	z3*	✅	5s	5s	+0%
`sign_keypair_internal`	LP64	cadical	✅	181s	182s	-1%
	LP64	z3_no_bv_extract*	✅	17s	22s	-23%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	34s	40s	-15%
`sign_signature`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	7s	-57%
`sign_signature_extmu`	LP64	cadical	✅	29s	29s	+0%
	LP64	z3*	✅	2s	5s	-60%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	15s	16s	-6%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	5s	3s	+67%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	16s	15s	+7%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	234s	249s	-6%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	1s	+300%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	4s	-25%
`unpack_pk_t1`	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	3s	1s	+200%
`unpack_sk`	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	1s	4s	-75%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	7s	8s	-12%
	LP64	z3*	✅	1s	2s	-50%
`yvec_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%

oqs-bot · 2026-10-30T11:16:06Z

CBMC Results (ML-DSA-65)

* default.

Full Results (435 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2173s	2057s	+5.6%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	153s	143s	+7%
`decompose`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`fqmul`	LP64	bitwuzla*	✅	26s	26s	+0%
	LP64	z3_smt_only	✅	22s	21s	+5%
`fqscale`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	2s	+0%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	21s	+5%
	LP64	z3*	✅	5s	4s	+25%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	3s	2s	+50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	19s	16s	+19%
	LP64	z3*	✅	4s	2s	+100%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	5s	3s	+67%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	cvc5_arrays_exp	✅	7s	7s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`keccak_init`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	15s	14s	+7%
	LP64	z3*	✅	13s	12s	+8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	232s	216s	+7%
`mld_check_pct`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	5s	5s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	71s	72s	-1%
	LP64	z3_no_bv_extract*	✅	7s	2s	+250%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	3s	2s	+50%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	83s	81s	+2%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`mld_h`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	5s	2s	+150%
`mld_invntt_layer`	LP64	bitwuzla*	✅	72s	64s	+12%
	LP64	z3_smt_only	✅	95s	87s	+9%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	5s	2s	+150%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	13s	-8%
	LP64	z3_no_bv_extract	✅	174s	157s	+11%
`mld_ntt_layer`	LP64	bitwuzla*	✅	28s	26s	+8%
	LP64	z3_no_bv_extract	✅	7s	4s	+75%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	48s	46s	+4%
	LP64	z3*	✅	4s	5s	-20%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	230s	229s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	4s	-75%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_finish`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	2s	+150%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	4s	-75%
`ntt_native_aarch64`	LP64	bitwuzla	✅	25s	18s	+39%
	LP64	z3*	✅	5s	2s	+150%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	5s	2s	+150%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	7s	5s	+40%
	LP64	z3	✅	1s	3s	-67%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	21s	-10%
	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	200s	179s	+12%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_h`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3_no_bv_extract*	✅	1s	2s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	79s	77s	+3%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	79s	79s	+0%
	LP64	z3_smt_only*	✅	3s	7s	-57%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	24s	20s	+20%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	5s	+60%
	LP64	z3	✅	2s	3s	-33%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	23s	22s	+5%
	LP64	z3*	✅	2s	2s	+0%
`poly_add`	LP64	cadical	✅	51s	49s	+4%
	LP64	z3*	✅	13s	13s	+0%
`poly_caddq`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_c`	LP64	bitwuzla	✅	23s	17s	+35%
	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_native`	LP64	bitwuzla	✅	118s	110s	+7%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	30s	32s	-6%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	134s	121s	+11%
	LP64	z3*	✅	4s	2s	+100%
`poly_challenge`	LP64	bitwuzla	✅	24s	22s	+9%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	8s	7s	+14%
	LP64	z3*	✅	7s	8s	-12%
`poly_chknorm_native`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	1s	2s	-50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	8s	8s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	1s	+300%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	206s	232s	-11%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native`	LP64	cadical	✅	12s	13s	-8%
	LP64	z3*	✅	5s	2s	+150%
`poly_decompose_native_x86_64`	LP64	cadical	✅	9s	8s	+12%
	LP64	z3*	✅	5s	5s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	171s	153s	+12%
	LP64	z3_smt_only*	✅	6s	5s	+20%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	51s	46s	+11%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	✅	48s	47s	+2%
	LP64	z3_smt_only*	✅	12s	10s	+20%
`poly_ntt_native`	LP64	bitwuzla	✅	30s	26s	+15%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	9s	+11%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	206s	188s	+10%
	LP64	z3*	✅	50s	52s	-4%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	53s	56s	-5%
	LP64	z3*	✅	3s	1s	+200%
`poly_power2round`	LP64	bitwuzla	✅	317s	261s	+21%
	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	bitwuzla	✅	8s	6s	+33%
	LP64	z3*	✅	3s	2s	+50%
`poly_shiftl`	LP64	bitwuzla	✅	13s	10s	+30%
	LP64	z3*	✅	6s	3s	+100%
`poly_sub`	LP64	bitwuzla	✅	16s	13s	+23%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform`	LP64	bitwuzla	✅	196s	176s	+11%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_4x`	LP64	cadical	✅	60s	61s	-2%
	LP64	z3*	✅	8s	7s	+14%
`poly_uniform_eta`	LP64	bitwuzla	✅	57s	52s	+10%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_eta_4x`	LP64	cadical	✅	63s	56s	+12%
	LP64	z3*	✅	10s	10s	+0%
`poly_uniform_gamma1`	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	12s	11s	+9%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	26s	-12%
	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	12s	+0%
	LP64	z3*	✅	5s	2s	+150%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	83s	93s	-11%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	31s	30s	+3%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	31s	28s	+11%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	5s	-80%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyt0_pack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	3s	+33%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	7s	9s	-22%
`polyt1_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_matrix_expand`	LP64	cadical	✅	12s	omitted	new
	LP64	z3_no_bv_extract*	✅	85s	76s	+12%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	7s	omitted	new
	LP64	z3*	✅	15s	13s	+15%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	252s	260s	-3%
	LP64	z3_no_bv_extract*	✅	1s	2s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	424s	415s	+2%
	LP64	z3*	✅	7s	7s	+0%
`polyveck_caddq`	LP64	cadical	✅	226s	213s	+6%
	LP64	z3*	✅	3s	4s	-25%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	174s	169s	+3%
	LP64	z3*	✅	3s	3s	+0%
`polyveck_invntt_tomont`	LP64	cadical	✅	189s	185s	+2%
	LP64	z3*	✅	4s	1s	+300%
`polyveck_ntt`	LP64	cadical	✅	195s	197s	-1%
	LP64	z3*	✅	4s	6s	-33%
`polyveck_reduce`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	43s	40s	+7%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	17s	+12%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_chknorm`	LP64	cadical	✅	71s	71s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_ntt`	LP64	cadical	✅	162s	155s	+5%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	10s	8s	+25%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	116s	117s	-1%
	LP64	z3_smt_only*	✅	168s	143s	+17%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	120s	116s	+3%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	34s	35s	-3%
	LP64	z3*	✅	2s	5s	-60%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	34s	33s	+3%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	34s	34s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	36s	33s	+9%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	5s	-60%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	5s	2s	+150%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`polyz_pack`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	3s	1s	+200%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	28s	27s	+4%
	LP64	z3*	✅	3s	1s	+200%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	18s	16s	+12%
	LP64	z3*	✅	4s	2s	+100%
`power2round`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	13s	11s	+18%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	14s	14s	+0%
`rej_uniform`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	8s	8s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	11s	12s	-8%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	10s	10s	+0%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	8s	5s	+60%
	LP64	z3_smt_only*	✅	13s	8s	+62%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake128_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
`shake256`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`shake256_release`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	1s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	bitwuzla	✅	1472s	1335s	+10%
	LP64	z3*	✅	20s	17s	+18%
`sign_keypair`	LP64	cadical	✅	464s	427s	+9%
	LP64	z3*	✅	4s	4s	+0%
`sign_keypair_internal`	LP64	cadical	✅	188s	180s	+4%
	LP64	z3_no_bv_extract*	✅	20s	20s	+0%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	36s	35s	+3%
`sign_signature`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	6s	4s	+50%
`sign_signature_extmu`	LP64	cadical	✅	29s	27s	+7%
	LP64	z3*	✅	5s	2s	+150%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	190s	206s	-8%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	2s	1s	+100%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	15s	15s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	2s	+100%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	449s	459s	-2%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	40s	36s	+11%
	LP64	z3*	✅	2s	1s	+100%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	32s	30s	+7%
	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	33s	28s	+18%
	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	4s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	4s	2s	+100%
`unpack_sk`	LP64	cadical	✅	57s	46s	+24%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	87s	85s	+2%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	159s	154s	+3%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_t0hat`	LP64	cadical	✅	85s	85s	+0%
	LP64	z3*	✅	2s	6s	-67%
`use_hint`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	4s	2s	+100%
`yvec_get_poly`	LP64	bitwuzla	✅	33s	31s	+6%
	LP64	z3*	✅	2s	4s	-50%
`yvec_init`	LP64	bitwuzla	✅	11s	9s	+22%
	LP64	z3*	✅	1s	3s	-67%

oqs-bot · 2026-10-30T11:24:27Z

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

* default.

Full Results (435 configurations)

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

oqs-bot · 2026-10-30T12:21:11Z

CBMC Results (ML-DSA-87)

* default.

Full Results (435 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	3422s	3745s	-8.6%
`caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	231s	270s	-14%
`decompose`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	23s	25s	-8%
	LP64	z3_smt_only	✅	22s	23s	-4%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	2s	+50%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	4s	4s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	3s	+0%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	2s	2s	+0%
`intt_native_x86_64`	LP64	bitwuzla	✅	16s	18s	-11%
	LP64	z3*	✅	2s	1s	+100%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	3s	5s	-40%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	7s	-14%
	LP64	cvc5_arrays_exp	✅	9s	9s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	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*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	5s	3s	+67%
`keccak_init`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	1s	+200%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	4s	2s	+100%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`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	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	14s	-14%
	LP64	z3*	✅	13s	11s	+18%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	5s	-40%
	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	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	326s	362s	-10%
`mld_check_pct`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	6s	6s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	81s	84s	-4%
	LP64	z3_no_bv_extract*	✅	6s	6s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	4s	2s	+100%
	ILP32	z3	✅	3s	4s	-25%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	5s	1s	+400%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	77s	88s	-12%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
`mld_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	64s	70s	-9%
	LP64	z3_smt_only	✅	85s	95s	-11%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	13s	-8%
	LP64	z3_no_bv_extract	✅	148s	175s	-15%
`mld_ntt_layer`	LP64	bitwuzla*	✅	24s	26s	-8%
	LP64	z3_no_bv_extract	✅	6s	5s	+20%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	4s	-50%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	82s	76s	+8%
	LP64	z3*	✅	9s	6s	+50%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	536s	559s	-4%
	LP64	z3*	✅	7s	5s	+40%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	6s	-50%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	5s	3s	+67%
	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	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	21s	-14%
	LP64	z3*	✅	4s	2s	+100%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	5s	-40%
	LP64	cvc5_mbqi_enum	✅	6s	6s	+0%
	LP64	z3	✅	3s	1s	+200%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	4s	9s	-56%
	LP64	z3	✅	3s	1s	+200%
`ntt_native_x86_64`	LP64	bitwuzla	✅	16s	18s	-11%
	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	171s	200s	-15%
	LP64	z3*	✅	1s	2s	-50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	1s	2s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	4s	-50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	88s	92s	-4%
	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	87s	92s	-5%
	LP64	z3_smt_only*	✅	4s	5s	-20%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	19s	23s	-17%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	2s	3s	-33%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	9s	10s	-10%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	3s	2s	+50%
`poly_add`	LP64	cadical	✅	46s	59s	-22%
	LP64	z3*	✅	14s	16s	-12%
`poly_caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	bitwuzla	✅	17s	20s	-15%
	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_native`	LP64	bitwuzla	✅	103s	119s	-13%
	LP64	z3*	✅	4s	1s	+300%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	33s	32s	+3%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	110s	130s	-15%
	LP64	z3*	✅	3s	4s	-25%
`poly_challenge`	LP64	bitwuzla	✅	34s	34s	+0%
	LP64	z3*	✅	5s	2s	+150%
`poly_chknorm`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	10s	-30%
	LP64	z3*	✅	8s	7s	+14%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	10s	-40%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	2s	+100%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	9s	8s	+12%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	212s	248s	-15%
	LP64	z3*	✅	4s	3s	+33%
`poly_decompose_native`	LP64	cadical	✅	12s	14s	-14%
	LP64	z3*	✅	5s	3s	+67%
`poly_decompose_native_x86_64`	LP64	cadical	✅	8s	10s	-20%
	LP64	z3*	✅	3s	1s	+200%
`poly_invntt_tomont`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	2s	+100%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	139s	168s	-17%
	LP64	z3_smt_only*	✅	5s	7s	-29%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	46s	46s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_ntt`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_ntt_c`	LP64	bitwuzla	✅	45s	52s	-13%
	LP64	z3_smt_only*	✅	11s	9s	+22%
`poly_ntt_native`	LP64	bitwuzla	✅	28s	28s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	178s	198s	-10%
	LP64	z3*	✅	47s	56s	-16%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	53s	56s	-5%
	LP64	z3*	✅	2s	4s	-50%
`poly_power2round`	LP64	bitwuzla	✅	291s	337s	-14%
	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	bitwuzla	✅	7s	8s	-12%
	LP64	z3*	✅	3s	3s	+0%
`poly_shiftl`	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	bitwuzla	✅	12s	14s	-14%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	bitwuzla	✅	157s	166s	-5%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	cadical	✅	56s	62s	-10%
	LP64	z3*	✅	7s	7s	+0%
`poly_uniform_eta`	LP64	bitwuzla	✅	76s	82s	-7%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_eta_4x`	LP64	cadical	✅	69s	66s	+5%
	LP64	z3*	✅	8s	10s	-20%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	11s	12s	-8%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	25s	23s	+9%
	LP64	z3*	✅	4s	2s	+100%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	11s	11s	+0%
	LP64	z3*	✅	5s	5s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	90s	83s	+8%
	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	28s	30s	-7%
	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	29s	32s	-9%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	6s	2s	+200%
`polyeta_unpack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	6s	5s	+20%
`polyt0_pack`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	5s	1s	+400%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	9s	8s	+12%
`polyt1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	5s	4s	+25%
`polyvec_matrix_expand`	LP64	cadical	✅	18s	omitted	new
	LP64	z3_no_bv_extract*	✅	109s	115s	-5%
`polyvec_matrix_expand_serial`	LP64	cadical	✅	13s	omitted	new
	LP64	z3*	✅	22s	24s	-8%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	581s	595s	-2%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	755s	782s	-3%
	LP64	z3*	✅	11s	9s	+22%
`polyveck_caddq`	LP64	cadical	✅	1183s	1243s	-5%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	196s	210s	-7%
	LP64	z3*	✅	3s	5s	-40%
`polyveck_invntt_tomont`	LP64	cadical	✅	305s	327s	-7%
	LP64	z3*	✅	6s	3s	+100%
`polyveck_ntt`	LP64	cadical	✅	1049s	1086s	-3%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_reduce`	LP64	cadical	✅	4s	4s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	53s	54s	-2%
	LP64	z3*	✅	3s	1s	+200%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	21s	-10%
	LP64	z3*	✅	3s	5s	-40%
`polyvecl_chknorm`	LP64	cadical	✅	134s	168s	-20%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_ntt`	LP64	cadical	✅	183s	195s	-6%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	13s	14s	-7%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	146s	156s	-6%
	LP64	z3_smt_only*	✅	276s	316s	-13%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	169s	185s	-9%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	77s	77s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	46s	48s	-4%
	LP64	z3*	✅	5s	2s	+150%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	46s	45s	+2%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	46s	47s	-2%
	LP64	z3*	✅	4s	3s	+33%
`polyw1_pack`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack_32`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	4s	1s	+300%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	4s	-50%
`polyw1_unpack`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack_32`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_unpack_88`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`polyz_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack_c`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	25s	27s	-7%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	18s	-22%
	LP64	z3*	✅	1s	2s	-50%
`power2round`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	5s	2s	+150%
`reduce32`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	16s	19s	-16%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	15s	16s	-6%
`rej_uniform`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	7s	7s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	9s	13s	-31%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	10s	11s	-9%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	8s	-50%
	LP64	z3_smt_only*	✅	10s	12s	-17%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	5s	1s	+400%
`shake128_init`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
`shake256`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	3s	-67%
`shake256_absorb`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	4s	-50%
`shake256_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	1s	+400%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	1s	+200%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	4s	3s	+33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`sig_unpack_hints`	LP64	bitwuzla	✅	27s	26s	+4%
	LP64	z3*	✅	15s	18s	-17%
`sign_keypair`	LP64	cadical	✅	605s	631s	-4%
	LP64	z3*	✅	4s	5s	-20%
`sign_keypair_internal`	LP64	cadical	✅	215s	224s	-4%
	LP64	z3_no_bv_extract*	✅	19s	26s	-27%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	30s	38s	-21%
`sign_signature`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	cadical	✅	51s	61s	-16%
	LP64	z3*	✅	4s	3s	+33%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	417s	453s	-8%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	6s	4s	+50%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	20s	25s	-20%
	LP64	z3*	✅	4s	5s	-20%
`sign_verify`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	2s	+150%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	1169s	1318s	-11%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	33s	34s	-3%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	33s	34s	-3%
	LP64	z3*	✅	3s	3s	+0%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	32s	35s	-9%
	LP64	z3*	✅	3s	4s	-25%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk`	LP64	cadical	✅	63s	79s	-20%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	85s	91s	-7%
	LP64	z3*	✅	3s	1s	+200%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	303s	315s	-4%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	cadical	✅	110s	115s	-4%
	LP64	z3*	✅	3s	3s	+0%
`use_hint`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	37s	40s	-7%
	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	bitwuzla	✅	15s	16s	-6%
	LP64	z3*	✅	1s	4s	-75%

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>

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>

mkannwischer · 2026-11-03T10:47:02Z

I've included this in #1521.

mkannwischer marked this pull request as ready for review October 30, 2026 11:28

mkannwischer requested a review from a team as a code owner October 30, 2026 11:28

mkannwischer force-pushed the cbmc-matrix-expand-unroll branch from f498524 to 2f76958 Compare October 30, 2026 14:07

mkannwischer marked this pull request as draft October 31, 2026 02:04

mkannwischer added the DO-NOT-MERGE label Oct 31, 2026

mkannwischer added 2 commits November 3, 2026 10:12

mkannwischer force-pushed the cbmc-matrix-expand-unroll branch from 2f76958 to 95244a5 Compare November 3, 2026 05:14

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

mkannwischer closed this Nov 3, 2026

Navigation Menu

Repository navigation

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

CBMC: Add CaDiCaL as a second solver for polyvec_matrix_expand(_serial)#1515
mkannwischer wants to merge 2 commits into
mainfrom
cbmc-matrix-expand-unroll

mkannwischer commented Oct 30, 2026

Uh oh!

oqs-bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

mkannwischer commented Nov 3, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mkannwischer commented Oct 30, 2026

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

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

Uh oh!

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

Uh oh!

oqs-bot commented Oct 30, 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!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

oqs-bot commented Oct 30, 2026 •

edited

Loading

oqs-bot commented Oct 30, 2026 •

edited

Loading

oqs-bot commented Oct 30, 2026 •

edited

Loading

oqs-bot commented Oct 30, 2026 •

edited

Loading

oqs-bot commented Oct 30, 2026 •

edited

Loading

oqs-bot commented Oct 30, 2026 •

edited

Loading