Port abicheck: Use the native build's CPU feature flags by mkannwischer · Pull Request #1532 · pq-code-package/mldsa-native

mkannwischer · 2026-11-05T07:40:17Z

Backend assembly is gated by backend and parameter-set macros. The ABI checker enables those macros for every kernel and adds CPU feature flags so the files assemble. It cannot simply use the platform's flags while unsupported files still contain instructions. Guard backend assembly with the architecture and feature macros for its instructions. Use `__ARM_FEATURE_SHA3` for the SHA3 kernels alongside `MLD_SYS_AARCH64_NEON`, and `MLD_SYS_RISCV32_M` for the RV32IM kernels. Apply matching guards to the ABI stubs and generated checks. Define `MLD_SYS_ARMV81M_MVE` only when `__ARM_FEATURE_MVE` is present: Armv8.1-M architecture support alone does not enable MVE. GCC exposes the feature macro only with a softfp or hard float ABI, so use `-mfloat-abi=hard` when autogen regenerates MVE assembly. The AWS-LC importer replaces `common.h` with s2n-bignum headers after running `unifdef`. Add a pre-import patch that resolves the NEON and AVX2 guards for the selected assembly, so imported files do not depend on mldsa-native's system macros. Ports pq-code-package/mlkem-native#1945. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

The ABI checker adds CPU feature flags to individual assembly objects. This can enable kernels which the platform disabled and leaves Make responsible for compiler capabilities that a custom build, such as Zephyr, determines itself. The preceding commit guards assembly with the same architecture and feature checks as the generated C tests. Compile the fixed source list with the platform's flags and let those guards omit unsupported kernels. Remove the generated feature makefiles, the separate SHA3 source filter and the RV32 `-march` selection. Ports pq-code-package/mlkem-native#1945. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

The Zig 0.17 jobs skip ABI checks because the checker previously added AArch64 `-march` flags which Zig parses as CPU names. The checker now uses the platform's CPU flags, so that restriction no longer applies. Remove `--no-abicheck` from the Extended compiler matrix and the Linux and macOS legacy matrices. Drop the comments about the old `-march` flags. Ports pq-code-package/mlkem-native#1945. Resolves #1488. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

oqs-bot · 2026-11-05T08:27:01Z

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

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1331s	1384s	-3.8%
`caddq`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	24s	27s	-11%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`fqmul`	LP64	bitwuzla*	✅	25s	25s	+0%
	LP64	z3_smt_only	✅	20s	20s	+0%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	bitwuzla	✅	23s	25s	-8%
	LP64	z3*	✅	2s	4s	-50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	2s	4s	-50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	16s	+12%
	LP64	z3*	✅	3s	2s	+50%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	5s	6s	-17%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	cvc5_arrays_exp	✅	9s	9s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	5s	-40%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	5s	-60%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	14s	14s	+0%
	LP64	z3*	✅	14s	13s	+8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	1s	1s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	129s	123s	+5%
`mld_check_pct`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	6s	5s	+20%
`mld_compute_pack_z`	LP64	cadical	✅	41s	37s	+11%
	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	3s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	3s	1s	+200%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	5s	3s	+67%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`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	✅	48s	50s	-4%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	4s	+0%
`mld_h`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	66s	81s	-19%
	LP64	z3_smt_only	✅	74s	83s	-11%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	14s	+0%
	LP64	z3_no_bv_extract	✅	180s	220s	-18%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	24s	+4%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	27s	30s	-10%
	LP64	z3*	✅	3s	3s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	92s	95s	-3%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_sign_finish`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	3s	-67%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	✅	18s	24s	-25%
	LP64	z3*	✅	1s	3s	-67%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	5s	-40%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	1s	3s	-67%
`ntt_native_x86_64`	LP64	bitwuzla	✅	15s	17s	-12%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	181s	211s	-14%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	5s	3s	+67%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	63s	60s	+5%
	LP64	z3_smt_only*	✅	3s	5s	-40%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	56s	58s	-3%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	21s	24s	-12%
	LP64	z3*	✅	2s	3s	-33%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	5s	2s	+150%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	5s	-80%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	4s	2s	+100%
`poly_add`	LP64	cadical	✅	48s	51s	-6%
	LP64	z3*	✅	12s	12s	+0%
`poly_caddq`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	5s	1s	+400%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	22s	-18%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native`	LP64	bitwuzla	✅	103s	120s	-14%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	36s	-6%
	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	117s	128s	-9%
	LP64	z3*	✅	5s	2s	+150%
`poly_challenge`	LP64	bitwuzla	✅	26s	25s	+4%
	LP64	z3*	✅	14s	11s	+27%
`poly_chknorm`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	7s	8s	-12%
`poly_chknorm_native`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	4s	1s	+300%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	1s	1s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	204s	249s	-18%
	LP64	z3*	✅	3s	5s	-40%
`poly_decompose_native`	LP64	cadical	✅	16s	16s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_native_x86_64`	LP64	cadical	✅	10s	10s	+0%
	LP64	z3*	✅	4s	3s	+33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	4s	+0%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	140s	185s	-24%
	LP64	z3_smt_only*	✅	5s	4s	+25%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	51s	-8%
	LP64	z3*	✅	4s	4s	+0%
`poly_ntt`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_ntt_c`	LP64	bitwuzla	✅	46s	54s	-15%
	LP64	z3_smt_only*	✅	8s	9s	-11%
`poly_ntt_native`	LP64	bitwuzla	✅	27s	30s	-10%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	3s	+33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	4s	1s	+300%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	186s	213s	-13%
	LP64	z3*	✅	37s	43s	-14%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	52s	57s	-9%
	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	bitwuzla	✅	282s	329s	-14%
	LP64	z3*	✅	2s	1s	+100%
`poly_reduce`	LP64	bitwuzla	✅	7s	9s	-22%
	LP64	z3*	✅	3s	2s	+50%
`poly_shiftl`	LP64	bitwuzla	✅	10s	11s	-9%
	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	bitwuzla	✅	10s	17s	-41%
	LP64	z3*	✅	3s	1s	+200%
`poly_uniform`	LP64	bitwuzla	✅	172s	205s	-16%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_4x`	LP64	cadical	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta`	LP64	bitwuzla	✅	76s	92s	-17%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_eta_4x`	LP64	cadical	✅	61s	63s	-3%
	LP64	z3*	✅	10s	8s	+25%
`poly_uniform_gamma1`	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	25s	-8%
	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	12s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	96s	92s	+4%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	31s	37s	-16%
	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	32s	38s	-16%
	LP64	z3*	✅	2s	4s	-50%
`polyeta_pack`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	4s	-75%
`polyeta_unpack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	10s	9s	+11%
`polyt0_pack`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	3s	3s	+0%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	8s	8s	+0%
`polyt1_pack`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	4s	2s	+100%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	35s	37s	-5%
	LP64	z3_no_bv_extract*	✅	5s	5s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	456s	492s	-7%
	LP64	z3*	✅	136s	148s	-8%
`polyveck_caddq`	LP64	cadical	✅	100s	108s	-7%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	106s	110s	-4%
	LP64	z3*	✅	4s	3s	+33%
`polyveck_invntt_tomont`	LP64	cadical	✅	138s	144s	-4%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_ntt`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_reduce`	LP64	cadical	✅	110s	116s	-5%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	15s	16s	-6%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_chknorm`	LP64	cadical	✅	54s	69s	-22%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_ntt`	LP64	cadical	✅	114s	121s	-6%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3_smt_only*	✅	2s	1s	+100%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	29s	32s	-9%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	25s	27s	-7%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack_32`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	4s	4s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	3s	+100%
`polyz_pack`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_c`	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	7s	7s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	26s	28s	-7%
	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	14s	17s	-18%
	LP64	z3*	✅	3s	4s	-25%
`power2round`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`reduce32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	14s	14s	+0%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3_smt_only	✅	16s	18s	-11%
`rej_uniform`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	9s	10s	-10%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	9s	7s	+29%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	1s	4s	-75%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	10s	10s	+0%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	2s	1s	+100%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3_smt_only*	✅	8s	9s	-11%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3_smt_only	✅	2s	1s	+100%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`shake256_absorb`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`shake256_release`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	1s	+300%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	1s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
`sig_unpack_hints`	LP64	bitwuzla	✅	54s	57s	-5%
	LP64	z3*	✅	26s	23s	+13%
`sign_keypair`	LP64	cadical	✅	44s	49s	-10%
	LP64	z3*	✅	4s	7s	-43%
`sign_keypair_internal`	LP64	cadical	✅	145s	167s	-13%
	LP64	z3_no_bv_extract*	✅	14s	14s	+0%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	29s	34s	-15%
`sign_signature`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	5s	-60%
`sign_signature_extmu`	LP64	cadical	✅	24s	27s	-11%
	LP64	z3*	✅	2s	2s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	11s	11s	+0%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	2s	3s	-33%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	13s	12s	+8%
	LP64	z3*	✅	2s	4s	-50%
`sign_verify`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	213s	217s	-2%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	4s	-50%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	3s	-67%
`unpack_pk_t1`	LP64	bitwuzla	✅	11s	13s	-15%
	LP64	z3*	✅	4s	2s	+100%
`unpack_sk`	LP64	cadical	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`use_hint`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`yvec_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%

oqs-bot · 2026-11-05T08:28:48Z

CBMC Results (ML-DSA-44)

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1641s	1890s	-13.2%
`caddq`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	64s	75s	-15%
`decompose`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	4s	-50%
`fqmul`	LP64	bitwuzla*	✅	23s	26s	-12%
	LP64	z3_smt_only	✅	18s	21s	-14%
`fqscale`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	5s	-40%
`intt_native_aarch64`	LP64	bitwuzla	✅	21s	29s	-28%
	LP64	z3*	✅	4s	2s	+100%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	11s	-27%
	LP64	z3	✅	3s	2s	+50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	10s	-10%
	LP64	z3	✅	3s	2s	+50%
`intt_native_x86_64`	LP64	bitwuzla	✅	17s	23s	-26%
	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	7s	8s	-12%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	6s	+17%
	LP64	cvc5_arrays_exp	✅	8s	11s	-27%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	3s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	4s	-25%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	4s	3s	+33%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_permute`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	11s	+18%
	LP64	z3*	✅	13s	13s	+0%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	209s	255s	-18%
`mld_check_pct`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	9s	-78%
`mld_compute_pack_z`	LP64	cadical	✅	66s	72s	-8%
	LP64	z3_no_bv_extract*	✅	4s	3s	+33%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	1s	3s	-67%
	ILP32	z3	✅	1s	4s	-75%
	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	1s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_no_bv_extract	✅	44s	53s	-17%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_invntt_layer`	LP64	bitwuzla*	✅	65s	76s	-14%
	LP64	z3_smt_only	✅	86s	100s	-14%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	5s	3s	+67%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	13s	+8%
	LP64	z3_no_bv_extract	✅	65s	76s	-14%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	28s	-11%
	LP64	z3_no_bv_extract	✅	7s	5s	+40%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	4s	-25%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	27s	31s	-13%
	LP64	z3*	✅	3s	5s	-40%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	91s	96s	-5%
	LP64	z3*	✅	4s	3s	+33%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	4s	5s	-20%
`mld_sign_finish`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	1s	2s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	20s	26s	-23%
	LP64	z3*	✅	1s	2s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	5s	8s	-38%
	LP64	z3	✅	1s	5s	-80%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	5s	6s	-17%
	LP64	z3	✅	2s	4s	-50%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	20s	-5%
	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	186s	218s	-15%
	LP64	z3*	✅	2s	1s	+100%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`pack_sig_z`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	57s	61s	-7%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	55s	58s	-5%
	LP64	z3_smt_only*	✅	3s	3s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	23s	25s	-8%
	LP64	z3*	✅	2s	3s	-33%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	10s	9s	+11%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	23s	26s	-12%
	LP64	z3*	✅	3s	3s	+0%
`poly_add`	LP64	cadical	✅	47s	53s	-11%
	LP64	z3*	✅	10s	12s	-17%
`poly_caddq`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	21s	-10%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native`	LP64	bitwuzla	✅	104s	134s	-22%
	LP64	z3*	✅	1s	5s	-80%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	35s	-3%
	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	122s	152s	-20%
	LP64	z3*	✅	2s	1s	+100%
`poly_challenge`	LP64	bitwuzla	✅	25s	29s	-14%
	LP64	z3*	✅	11s	13s	-15%
`poly_chknorm`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	6s	3s	+100%
`poly_chknorm_c`	LP64	bitwuzla	✅	7s	9s	-22%
	LP64	z3*	✅	7s	10s	-30%
`poly_chknorm_native`	LP64	bitwuzla	✅	8s	7s	+14%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	5s	-60%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	3s	7s	-57%
	LP64	z3*	✅	1s	1s	+0%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	9s	6s	+50%
	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	214s	223s	-4%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_native`	LP64	cadical	✅	14s	18s	-22%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	LP64	cadical	✅	11s	11s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	4s	2s	+100%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	157s	166s	-5%
	LP64	z3_smt_only*	✅	3s	6s	-50%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	53s	-11%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt_c`	LP64	bitwuzla	✅	45s	56s	-20%
	LP64	z3_smt_only*	✅	8s	10s	-20%
`poly_ntt_native`	LP64	bitwuzla	✅	27s	31s	-13%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	168s	223s	-25%
	LP64	z3*	✅	60s	73s	-18%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	52s	57s	-9%
	LP64	z3*	✅	2s	2s	+0%
`poly_power2round`	LP64	bitwuzla	✅	290s	365s	-21%
	LP64	z3*	✅	3s	3s	+0%
`poly_reduce`	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_sub`	LP64	bitwuzla	✅	15s	14s	+7%
	LP64	z3*	✅	1s	2s	-50%
`poly_uniform`	LP64	bitwuzla	✅	180s	202s	-11%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_4x`	LP64	cadical	✅	60s	63s	-5%
	LP64	z3*	✅	5s	7s	-29%
`poly_uniform_eta`	LP64	bitwuzla	✅	74s	92s	-20%
	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_eta_4x`	LP64	cadical	✅	62s	65s	-5%
	LP64	z3*	✅	8s	11s	-27%
`poly_uniform_gamma1`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	11s	11s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	25s	-8%
	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	13s	11s	+18%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	92s	93s	-1%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	33s	38s	-13%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	33s	36s	-8%
	LP64	z3*	✅	3s	3s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	8s	8s	+0%
`polyt0_pack`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	9s	11s	-18%
`polyt1_pack`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	1s	1s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	4s	+25%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	11s	12s	-8%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	5s	6s	-17%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	99s	106s	-7%
	LP64	z3_no_bv_extract*	✅	1s	1s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	237s	269s	-12%
	LP64	z3*	✅	4s	4s	+0%
`polyveck_caddq`	LP64	cadical	✅	103s	112s	-8%
	LP64	z3*	✅	2s	5s	-60%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	123s	113s	+9%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_invntt_tomont`	LP64	cadical	✅	138s	147s	-6%
	LP64	z3*	✅	4s	2s	+100%
`polyveck_ntt`	LP64	cadical	✅	117s	124s	-6%
	LP64	z3*	✅	1s	4s	-75%
`polyveck_reduce`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	27s	31s	-13%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	16s	16s	+0%
	LP64	z3*	✅	2s	4s	-50%
`polyvecl_chknorm`	LP64	cadical	✅	53s	54s	-2%
	LP64	z3*	✅	2s	1s	+100%
`polyvecl_ntt`	LP64	cadical	✅	129s	123s	+5%
	LP64	z3*	✅	3s	1s	+200%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	4s	6s	-33%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	92s	95s	-3%
	LP64	z3_smt_only*	✅	102s	123s	-17%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	162s	169s	-4%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	39s	42s	-7%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	43s	44s	-2%
	LP64	z3*	✅	3s	1s	+200%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	32s	35s	-9%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	27s	30s	-10%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack_32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack_88`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyz_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	1s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	7s	7s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	23s	30s	-23%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	15s	17s	-12%
	LP64	z3*	✅	2s	2s	+0%
`power2round`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`rej_eta`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	3s	2s	+50%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	13s	16s	-19%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	16s	19s	-16%
`rej_uniform`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	9s	10s	-10%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	13s	18s	-28%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	3s	3s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	4s	1s	+300%
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	7s	11s	-36%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	1s	+100%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3_smt_only*	✅	8s	8s	+0%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	5s	1s	+400%
`shake128_init`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`shake128_release`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3_smt_only	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	3s	1s	+200%
`shake256`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	1s	+200%
`shake256_absorb`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake256_release`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	1s	+400%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	bitwuzla	✅	52s	61s	-15%
	LP64	z3*	✅	34s	42s	-19%
`sign_keypair`	LP64	cadical	✅	44s	52s	-15%
	LP64	z3*	✅	4s	7s	-43%
`sign_keypair_internal`	LP64	cadical	✅	147s	155s	-5%
	LP64	z3_no_bv_extract*	✅	9s	10s	-10%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	29s	34s	-15%
`sign_signature`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	cadical	✅	20s	23s	-13%
	LP64	z3*	✅	5s	2s	+150%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	101s	114s	-11%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	13s	17s	-24%
	LP64	z3*	✅	4s	7s	-43%
`sign_verify`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	327s	376s	-13%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	5s	1s	+400%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	29s	31s	-6%
	LP64	z3*	✅	1s	1s	+0%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	28s	32s	-12%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	31s	36s	-14%
	LP64	z3*	✅	3s	3s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	6s	-50%
`unpack_pk_t1`	LP64	bitwuzla	✅	11s	14s	-21%
	LP64	z3*	✅	3s	5s	-40%
`unpack_sk`	LP64	cadical	✅	33s	36s	-8%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	253s	273s	-7%
	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	244s	267s	-9%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	38s	41s	-7%
	LP64	z3*	✅	1s	3s	-67%
`use_hint`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	bitwuzla	✅	30s	37s	-19%
	LP64	z3*	✅	3s	4s	-25%
`yvec_init`	LP64	bitwuzla	✅	39s	43s	-9%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-11-05T08:44:37Z

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

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1227s	1285s	-4.5%
`caddq`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	32s	34s	-6%
`decompose`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	24s	27s	-11%
	LP64	z3_smt_only	✅	20s	21s	-5%
`fqscale`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	4s	-75%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	26s	-15%
	LP64	z3*	✅	3s	5s	-40%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	2s	3s	-33%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	9s	6s	+50%
	LP64	z3	✅	1s	5s	-80%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	17s	+6%
	LP64	z3*	✅	2s	2s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	6s	8s	-25%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	7s	8s	-12%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
`keccak_init`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	4s	3s	+33%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	1s	+300%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	4s	1s	+300%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	3s	-33%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	1s	+0%
	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	✅	12s	12s	+0%
	LP64	z3*	✅	12s	13s	-8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	108s	122s	-11%
`mld_check_pct`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	5s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	37s	38s	-3%
	LP64	z3_no_bv_extract*	✅	4s	6s	-33%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	1s	+0%
	ILP32	cvc5_arrays_exp	✅	1s	2s	-50%
	ILP32	z3	✅	2s	3s	-33%
	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	1s	+300%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	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	✅	4s	2s	+100%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	49s	51s	-4%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_h`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	66s	78s	-15%
	LP64	z3_smt_only	✅	73s	90s	-19%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	5s	4s	+25%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	13s	-15%
	LP64	z3_no_bv_extract	✅	190s	221s	-14%
`mld_ntt_layer`	LP64	bitwuzla*	✅	27s	28s	-4%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	1s	2s	-50%
	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	✅	48s	51s	-6%
	LP64	z3*	✅	4s	4s	+0%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	228s	229s	-0%
	LP64	z3*	✅	2s	4s	-50%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
`mld_sign_finish`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	2s	+150%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	✅	20s	24s	-17%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	1s	2s	-50%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	4s	1s	+300%
`ntt_native_x86_64`	LP64	bitwuzla	✅	19s	20s	-5%
	LP64	z3*	✅	5s	2s	+150%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	190s	199s	-5%
	LP64	z3*	✅	1s	2s	-50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`pack_sig_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
`pack_sig_z`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	80s	81s	-1%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	78s	82s	-5%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	22s	26s	-15%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	1s	4s	-75%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	2s	+50%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	21s	21s	+0%
	LP64	z3*	✅	4s	3s	+33%
`poly_add`	LP64	cadical	✅	45s	49s	-8%
	LP64	z3*	✅	10s	13s	-23%
`poly_caddq`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_c`	LP64	bitwuzla	✅	21s	22s	-5%
	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_native`	LP64	bitwuzla	✅	112s	129s	-13%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	35s	-3%
	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	127s	145s	-12%
	LP64	z3*	✅	5s	3s	+67%
`poly_challenge`	LP64	bitwuzla	✅	25s	25s	+0%
	LP64	z3*	✅	12s	13s	-8%
`poly_chknorm`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	8s	8s	+0%
	LP64	z3*	✅	8s	11s	-27%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	4s	1s	+300%
`poly_decompose`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	8s	9s	-11%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	185s	261s	-29%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_native`	LP64	cadical	✅	12s	12s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	LP64	cadical	✅	9s	9s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont`	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	153s	185s	-17%
	LP64	z3_smt_only*	✅	5s	5s	+0%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	47s	51s	-8%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_ntt_c`	LP64	bitwuzla	✅	51s	54s	-6%
	LP64	z3_smt_only*	✅	11s	12s	-8%
`poly_ntt_native`	LP64	bitwuzla	✅	29s	32s	-9%
	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	12s	-17%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	193s	193s	+0%
	LP64	z3*	✅	40s	43s	-7%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	57s	56s	+2%
	LP64	z3*	✅	1s	2s	-50%
`poly_power2round`	LP64	bitwuzla	✅	264s	301s	-12%
	LP64	z3*	✅	1s	4s	-75%
`poly_reduce`	LP64	bitwuzla	✅	8s	7s	+14%
	LP64	z3*	✅	1s	3s	-67%
`poly_shiftl`	LP64	bitwuzla	✅	13s	13s	+0%
	LP64	z3*	✅	3s	4s	-25%
`poly_sub`	LP64	bitwuzla	✅	16s	16s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	bitwuzla	✅	186s	210s	-11%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform_4x`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_eta`	LP64	bitwuzla	✅	54s	62s	-13%
	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta_4x`	LP64	cadical	✅	54s	57s	-5%
	LP64	z3*	✅	9s	11s	-18%
`poly_uniform_gamma1`	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	23s	22s	+5%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	10s	15s	-33%
	LP64	z3*	✅	4s	3s	+33%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	85s	86s	-1%
	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	31s	34s	-9%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	31s	31s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`polyt0_pack`	LP64	bitwuzla	✅	3s	7s	-57%
	LP64	z3*	✅	2s	4s	-50%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	9s	7s	+29%
`polyt1_pack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	2s	2s	+0%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	41s	41s	+0%
	LP64	z3_no_bv_extract*	✅	6s	4s	+50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	761s	817s	-7%
	LP64	z3*	✅	80s	97s	-18%
`polyveck_caddq`	LP64	cadical	✅	262s	225s	+16%
	LP64	z3*	✅	1s	3s	-67%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	169s	186s	-9%
	LP64	z3*	✅	16s	16s	+0%
`polyveck_invntt_tomont`	LP64	cadical	✅	187s	234s	-20%
	LP64	z3*	✅	3s	4s	-25%
`polyveck_ntt`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`polyveck_reduce`	LP64	cadical	✅	175s	187s	-6%
	LP64	z3*	✅	4s	1s	+300%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	19s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_chknorm`	LP64	cadical	✅	68s	74s	-8%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_ntt`	LP64	cadical	✅	154s	168s	-8%
	LP64	z3*	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	2s	1s	+100%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	1s	3s	-67%
	LP64	z3_smt_only*	✅	1s	1s	+0%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	4s	2s	+100%
	LP64	z3_smt_only*	✅	3s	1s	+200%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	32s	35s	-9%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	33s	34s	-3%
	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	5s	-60%
`polyw1_pack_88`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	1s	+0%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	1s	+200%
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`polyz_pack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_native`	LP64	bitwuzla	✅	26s	25s	+4%
	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	17s	-6%
	LP64	z3*	✅	3s	4s	-25%
`power2round`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`reduce32`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	1s	+200%
`rej_eta`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	5s	4s	+25%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	14s	16s	-12%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	11s	12s	-8%
`rej_uniform`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	12s	9s	+33%
`rej_uniform_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	10s	9s	+11%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	4s	-25%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3_smt_only*	✅	3s	1s	+200%
`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	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3_smt_only*	✅	9s	9s	+0%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	3s	+0%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`shake128_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	5s	-80%
	LP64	z3	✅	2s	1s	+100%
`shake256`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_absorb`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`shake256_release`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	1s	+100%
`sig_unpack_hints`	LP64	bitwuzla	✅	1326s	1511s	-12%
	LP64	z3*	✅	17s	20s	-15%
`sign_keypair`	LP64	cadical	✅	424s	507s	-16%
	LP64	z3*	✅	3s	5s	-40%
`sign_keypair_internal`	LP64	cadical	✅	181s	189s	-4%
	LP64	z3_no_bv_extract*	✅	15s	15s	+0%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	25s	27s	-7%
`sign_signature`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_extmu`	LP64	cadical	✅	28s	29s	-3%
	LP64	z3*	✅	5s	5s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	14s	14s	+0%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	5s	2s	+150%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	15s	14s	+7%
	LP64	z3*	✅	4s	4s	+0%
`sign_verify`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`sign_verify_extmu`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	193s	185s	+4%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	4s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	3s	-33%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
`unpack_pk_t1`	LP64	bitwuzla	✅	13s	13s	+0%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk`	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_t0hat`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	4s	-75%
`yvec_init`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	4s	2s	+100%

oqs-bot · 2026-11-05T08:46:50Z

CBMC Results (ML-DSA-65)

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2041s	2339s	-12.7%
`caddq`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	122s	154s	-21%
`decompose`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	23s	27s	-15%
	LP64	z3_smt_only	✅	20s	21s	-5%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	1s	+0%
`intt_native_aarch64`	LP64	bitwuzla	✅	21s	27s	-22%
	LP64	z3*	✅	3s	2s	+50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	1s	4s	-75%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	4s	-75%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	2s	3s	-33%
`intt_native_x86_64`	LP64	bitwuzla	✅	17s	21s	-19%
	LP64	z3*	✅	4s	1s	+300%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	6s	7s	-14%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	cvc5_arrays_exp	✅	8s	10s	-20%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	3s	1s	+200%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	3s	-67%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	2s	5s	-60%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	4s	3s	+33%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	12s	13s	-8%
	LP64	z3*	✅	13s	12s	+8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	224s	267s	-16%
`mld_check_pct`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	6s	5s	+20%
`mld_compute_pack_z`	LP64	cadical	✅	73s	75s	-3%
	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	4s	2s	+100%
	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	44s	51s	-14%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	4s	-50%
`mld_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	5s	-40%
`mld_invntt_layer`	LP64	bitwuzla*	✅	63s	83s	-24%
	LP64	z3_smt_only	✅	86s	108s	-20%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	2s	+150%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	4s	5s	-20%
	LP64	z3*	✅	4s	4s	+0%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	5s	2s	+150%
	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	10s	15s	-33%
	LP64	z3_no_bv_extract	✅	61s	80s	-24%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	31s	-26%
	LP64	z3_no_bv_extract	✅	3s	5s	-40%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	4s	-25%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	43s	48s	-10%
	LP64	z3*	✅	4s	5s	-20%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	229s	254s	-10%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`mld_sign_finish`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	2s	+150%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	4s	-25%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	27s	-30%
	LP64	z3*	✅	3s	4s	-25%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	5s	3s	+67%
	LP64	cvc5_mbqi_enum	✅	5s	5s	+0%
	LP64	z3	✅	2s	3s	-33%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	3s	2s	+50%
`ntt_native_x86_64`	LP64	bitwuzla	✅	15s	23s	-35%
	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	179s	224s	-20%
	LP64	z3*	✅	2s	2s	+0%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	4s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	3s	+67%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	74s	84s	-12%
	LP64	z3_smt_only*	✅	4s	2s	+100%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	79s	86s	-8%
	LP64	z3_smt_only*	✅	5s	5s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	20s	26s	-23%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	2s	1s	+100%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	4s	-75%
	LP64	cvc5_mbqi_enum	✅	7s	11s	-36%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	20s	25s	-20%
	LP64	z3*	✅	4s	3s	+33%
`poly_add`	LP64	cadical	✅	47s	54s	-13%
	LP64	z3*	✅	9s	15s	-40%
`poly_caddq`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`poly_caddq_c`	LP64	bitwuzla	✅	18s	26s	-31%
	LP64	z3*	✅	3s	4s	-25%
`poly_caddq_native`	LP64	bitwuzla	✅	113s	142s	-20%
	LP64	z3*	✅	3s	1s	+200%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	35s	41s	-15%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	116s	162s	-28%
	LP64	z3*	✅	4s	1s	+300%
`poly_challenge`	LP64	bitwuzla	✅	23s	25s	-8%
	LP64	z3*	✅	11s	12s	-8%
`poly_chknorm`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_c`	LP64	bitwuzla	✅	8s	10s	-20%
	LP64	z3*	✅	8s	8s	+0%
`poly_chknorm_native`	LP64	bitwuzla	✅	7s	8s	-12%
	LP64	z3*	✅	5s	3s	+67%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
`poly_decompose`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	1s	+100%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	7s	8s	-12%
	LP64	z3*	✅	3s	4s	-25%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	227s	288s	-21%
	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_native`	LP64	cadical	✅	13s	14s	-7%
	LP64	z3*	✅	4s	2s	+100%
`poly_decompose_native_x86_64`	LP64	cadical	✅	8s	9s	-11%
	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	158s	211s	-25%
	LP64	z3_smt_only*	✅	5s	6s	-17%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	43s	53s	-19%
	LP64	z3*	✅	1s	2s	-50%
`poly_ntt`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
`poly_ntt_c`	LP64	bitwuzla	✅	46s	66s	-30%
	LP64	z3_smt_only*	✅	9s	12s	-25%
`poly_ntt_native`	LP64	bitwuzla	✅	24s	31s	-23%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	8s	12s	-33%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	176s	233s	-24%
	LP64	z3*	✅	65s	71s	-8%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	54s	58s	-7%
	LP64	z3*	✅	3s	2s	+50%
`poly_power2round`	LP64	bitwuzla	✅	288s	420s	-31%
	LP64	z3*	✅	2s	3s	-33%
`poly_reduce`	LP64	bitwuzla	✅	9s	11s	-18%
	LP64	z3*	✅	2s	3s	-33%
`poly_shiftl`	LP64	bitwuzla	✅	10s	15s	-33%
	LP64	z3*	✅	3s	2s	+50%
`poly_sub`	LP64	bitwuzla	✅	15s	18s	-17%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform`	LP64	bitwuzla	✅	156s	226s	-31%
	LP64	z3*	✅	1s	2s	-50%
`poly_uniform_4x`	LP64	cadical	✅	60s	66s	-9%
	LP64	z3*	✅	9s	9s	+0%
`poly_uniform_eta`	LP64	bitwuzla	✅	50s	64s	-22%
	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_eta_4x`	LP64	cadical	✅	53s	61s	-13%
	LP64	z3*	✅	9s	10s	-10%
`poly_uniform_gamma1`	LP64	cadical	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	10s	13s	-23%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	24s	25s	-4%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	14s	-14%
	LP64	z3*	✅	4s	1s	+300%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	91s	98s	-7%
	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	27s	35s	-23%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	29s	36s	-19%
	LP64	z3*	✅	2s	1s	+100%
`polyeta_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	2s	-50%
`polyeta_unpack`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	4s	-25%
`polyt0_pack`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	8s	9s	-11%
`polyt1_pack`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	6s	3s	+100%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	57s	71s	-20%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	11s	12s	-8%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	246s	270s	-9%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	414s	443s	-7%
	LP64	z3*	✅	8s	6s	+33%
`polyveck_caddq`	LP64	cadical	✅	206s	239s	-14%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	166s	185s	-10%
	LP64	z3*	✅	7s	8s	-12%
`polyveck_invntt_tomont`	LP64	cadical	✅	181s	207s	-13%
	LP64	z3*	✅	4s	4s	+0%
`polyveck_ntt`	LP64	cadical	✅	191s	211s	-9%
	LP64	z3*	✅	4s	4s	+0%
`polyveck_reduce`	LP64	cadical	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	42s	46s	-9%
	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	18s	20s	-10%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_chknorm`	LP64	cadical	✅	82s	79s	+4%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_ntt`	LP64	cadical	✅	153s	174s	-12%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	10s	11s	-9%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	110s	123s	-11%
	LP64	z3_smt_only*	✅	181s	239s	-24%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	110s	126s	-13%
	LP64	z3_smt_only*	✅	2s	4s	-50%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	33s	39s	-15%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	34s	38s	-11%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	31s	32s	-3%
	LP64	z3*	✅	3s	3s	+0%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	32s	34s	-6%
	LP64	z3*	✅	5s	2s	+150%
`polyw1_pack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`polyw1_pack_88`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
`polyz_pack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	2s	+100%
`polyz_unpack`	LP64	bitwuzla	✅	5s	9s	-44%
	LP64	z3*	✅	4s	1s	+300%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_c`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	26s	34s	-24%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	16s	17s	-6%
	LP64	z3*	✅	4s	3s	+33%
`power2round`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	4s	-75%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	4s	4s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	14s	16s	-12%
`rej_eta_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	9s	13s	-31%
`rej_uniform`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	9s	9s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	13s	18s	-28%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	5s	2s	+150%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	9s	11s	-18%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3_smt_only*	✅	10s	10s	+0%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	5s	-40%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	2s	-50%
`shake256`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`shake256_absorb`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	3s	+0%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
`shake256_release`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	4s	3s	+33%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	bitwuzla	✅	1278s	1762s	-27%
	LP64	z3*	✅	18s	22s	-18%
`sign_keypair`	LP64	cadical	✅	395s	563s	-30%
	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	cadical	✅	204s	195s	+5%
	LP64	z3_no_bv_extract*	✅	16s	17s	-6%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	31s	40s	-22%
`sign_signature`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	5s	4s	+25%
`sign_signature_extmu`	LP64	cadical	✅	26s	44s	-41%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	149s	196s	-24%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	15s	20s	-25%
	LP64	z3*	✅	6s	2s	+200%
`sign_verify`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	443s	478s	-7%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	39s	44s	-11%
	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	31s	34s	-9%
	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	32s	30s	+7%
	LP64	z3*	✅	3s	3s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	bitwuzla	✅	13s	13s	+0%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk`	LP64	cadical	✅	44s	53s	-17%
	LP64	z3*	✅	6s	3s	+100%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	84s	94s	-11%
	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	151s	170s	-11%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_t0hat`	LP64	cadical	✅	92s	91s	+1%
	LP64	z3*	✅	4s	1s	+300%
`use_hint`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	4s	-50%
`yvec_get_poly`	LP64	bitwuzla	✅	33s	37s	-11%
	LP64	z3*	✅	3s	1s	+200%
`yvec_init`	LP64	bitwuzla	✅	8s	9s	-11%
	LP64	z3*	✅	2s	1s	+100%

oqs-bot · 2026-11-05T09:22:53Z

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

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1300s	1294s	+0.5%
`caddq`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	27s	25s	+8%
`decompose`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`fqmul`	LP64	bitwuzla*	✅	23s	25s	-8%
	LP64	z3_smt_only	✅	21s	20s	+5%
`fqscale`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	3s	2s	+50%
`intt_native_aarch64`	LP64	bitwuzla	✅	22s	22s	+0%
	LP64	z3*	✅	1s	1s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	10s	7s	+43%
	LP64	z3	✅	1s	2s	-50%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	1s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	2s	2s	+0%
`intt_native_x86_64`	LP64	bitwuzla	✅	18s	16s	+12%
	LP64	z3*	✅	2s	2s	+0%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	5s	5s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	9s	6s	+50%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	✅	1s	3s	-67%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`keccak_init`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	3s	-67%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	13s	+0%
	LP64	z3*	✅	13s	12s	+8%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	3s	2s	+50%
`make_hint`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	160s	154s	+4%
`mld_check_pct`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	5s	5s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	34s	34s	+0%
	LP64	z3_no_bv_extract*	✅	4s	4s	+0%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	2s	5s	-60%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	46s	46s	+0%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mld_h`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	64s	65s	-2%
	LP64	z3_smt_only	✅	72s	75s	-4%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	5s	-40%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	12s	+0%
	LP64	z3_no_bv_extract	✅	166s	154s	+8%
`mld_ntt_layer`	LP64	bitwuzla*	✅	25s	23s	+9%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	5s	-80%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	73s	72s	+1%
	LP64	z3*	✅	6s	5s	+20%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	539s	542s	-1%
	LP64	z3*	✅	3s	6s	-50%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	5s	-60%
`mld_sign_finish`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	3s	+0%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	4s	-75%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	17s	+12%
	LP64	z3*	✅	3s	2s	+50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	2s	2s	+0%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	3s	3s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	✅	17s	16s	+6%
	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	182s	178s	+2%
	LP64	z3*	✅	3s	2s	+50%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`pack_sig_h`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`pack_sig_z`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	90s	91s	-1%
	LP64	z3_smt_only*	✅	5s	3s	+67%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	87s	87s	+0%
	LP64	z3_smt_only*	✅	5s	4s	+25%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	21s	19s	+11%
	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	2s	1s	+100%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	1s	3s	-67%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	20s	21s	-5%
	LP64	z3*	✅	1s	2s	-50%
`poly_add`	LP64	cadical	✅	59s	49s	+20%
	LP64	z3*	✅	11s	9s	+22%
`poly_caddq`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	1s	+200%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	17s	+12%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	bitwuzla	✅	108s	106s	+2%
	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	33s	+3%
	LP64	z3*	✅	2s	1s	+100%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	124s	118s	+5%
	LP64	z3*	✅	2s	1s	+100%
`poly_challenge`	LP64	bitwuzla	✅	30s	35s	-14%
	LP64	z3*	✅	14s	12s	+17%
`poly_chknorm`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	8s	+12%
	LP64	z3*	✅	6s	7s	-14%
`poly_chknorm_native`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	8s	7s	+14%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	1s	+300%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	229s	224s	+2%
	LP64	z3*	✅	3s	6s	-50%
`poly_decompose_native`	LP64	cadical	✅	14s	14s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	LP64	cadical	✅	7s	9s	-22%
	LP64	z3*	✅	4s	4s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	157s	152s	+3%
	LP64	z3_smt_only*	✅	4s	5s	-20%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	43s	45s	-4%
	LP64	z3*	✅	1s	3s	-67%
`poly_ntt`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_c`	LP64	bitwuzla	✅	50s	47s	+6%
	LP64	z3_smt_only*	✅	9s	9s	+0%
`poly_ntt_native`	LP64	bitwuzla	✅	26s	25s	+4%
	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	1s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	188s	184s	+2%
	LP64	z3*	✅	37s	37s	+0%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	49s	54s	-9%
	LP64	z3*	✅	3s	1s	+200%
`poly_power2round`	LP64	bitwuzla	✅	238s	266s	-11%
	LP64	z3*	✅	3s	3s	+0%
`poly_reduce`	LP64	bitwuzla	✅	8s	10s	-20%
	LP64	z3*	✅	2s	1s	+100%
`poly_shiftl`	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	bitwuzla	✅	14s	13s	+8%
	LP64	z3*	✅	1s	3s	-67%
`poly_uniform`	LP64	bitwuzla	✅	162s	165s	-2%
	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_4x`	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`poly_uniform_eta`	LP64	bitwuzla	✅	79s	76s	+4%
	LP64	z3*	✅	5s	2s	+150%
`poly_uniform_eta_4x`	LP64	cadical	✅	62s	60s	+3%
	LP64	z3*	✅	11s	7s	+57%
`poly_uniform_gamma1`	LP64	cadical	✅	2s	3s	-33%
	LP64	z3*	✅	1s	1s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	22s	20s	+10%
	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	10s	11s	-9%
	LP64	z3*	✅	4s	4s	+0%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	91s	93s	-2%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	30s	28s	+7%
	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	29s	30s	-3%
	LP64	z3*	✅	3s	2s	+50%
`polyeta_pack`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_unpack`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	8s	9s	-11%
`polyt0_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	1s	+100%
`polyt0_unpack`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	10s	7s	+43%
`polyt1_pack`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
`polyt1_unpack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	2s	+200%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	2s	+50%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	48s	44s	+9%
	LP64	z3_no_bv_extract*	✅	4s	3s	+33%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	1330s	1250s	+6%
	LP64	z3*	✅	106s	102s	+4%
`polyveck_caddq`	LP64	cadical	✅	1235s	1207s	+2%
	LP64	z3*	✅	1s	2s	-50%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	204s	196s	+4%
	LP64	z3*	✅	2s	5s	-60%
`polyveck_invntt_tomont`	LP64	cadical	✅	312s	303s	+3%
	LP64	z3*	✅	6s	3s	+100%
`polyveck_ntt`	LP64	cadical	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyveck_reduce`	LP64	cadical	✅	263s	247s	+6%
	LP64	z3*	✅	2s	2s	+0%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	16s	+19%
	LP64	z3*	✅	3s	1s	+200%
`polyvecl_chknorm`	LP64	cadical	✅	139s	133s	+5%
	LP64	z3*	✅	1s	2s	-50%
`polyvecl_ntt`	LP64	cadical	✅	193s	181s	+7%
	LP64	z3*	✅	4s	4s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	3s	1s	+200%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	4s	3s	+33%
	LP64	z3*	✅	4s	2s	+100%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	44s	46s	-4%
	LP64	z3*	✅	3s	2s	+50%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	46s	48s	-4%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_pack`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
`polyw1_unpack_88`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyz_pack`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`polyz_unpack`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	4s	6s	-33%
`polyz_unpack_native`	LP64	bitwuzla	✅	27s	25s	+8%
	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	13s	+31%
	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	1s	+200%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	3s	+0%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	12s	13s	-8%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	18s	16s	+12%
`rej_uniform`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	8s	9s	-11%
`rej_uniform_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	9s	8s	+12%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	3s	1s	+200%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	10s	9s	+11%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3_smt_only*	✅	9s	7s	+29%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`shake128_release`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`shake256`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	1s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	bitwuzla	✅	24s	24s	+0%
	LP64	z3*	✅	38s	37s	+3%
`sign_keypair`	LP64	cadical	✅	585s	495s	+18%
	LP64	z3*	✅	5s	6s	-17%
`sign_keypair_internal`	LP64	cadical	✅	222s	213s	+4%
	LP64	z3_no_bv_extract*	✅	18s	19s	-5%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	27s	28s	-4%
`sign_signature`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	4s	+0%
`sign_signature_extmu`	LP64	cadical	✅	60s	58s	+3%
	LP64	z3*	✅	3s	1s	+200%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	16s	14s	+14%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	2s	+50%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	20s	21s	-5%
	LP64	z3*	✅	4s	6s	-33%
`sign_verify`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
`sign_verify_extmu`	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	3s	2s	+50%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	183s	193s	-5%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	3s	2s	+50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`unpack_pk_t1`	LP64	bitwuzla	✅	14s	10s	+40%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk`	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3*	✅	2s	5s	-60%
`unpack_sk_t0hat`	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
`use_hint`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	1s	2s	-50%
`yvec_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%

oqs-bot · 2026-11-05T09:41:52Z

CBMC Results (ML-DSA-87)

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	3773s	3488s	+8.2%
`caddq`	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	✅	179s	176s	+2%
`decompose`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	23s	24s	-4%
	LP64	z3_smt_only	✅	20s	18s	+11%
`fqscale`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	bitwuzla	✅	23s	22s	+5%
	LP64	z3*	✅	4s	1s	+300%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	6s	+33%
	LP64	z3	✅	2s	3s	-33%
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	3s	3s	+0%
`intt_native_x86_64`	LP64	bitwuzla	✅	20s	17s	+18%
	LP64	z3*	✅	2s	5s	-60%
`keccak_absorb`	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
	LP64	z3*	✅	7s	6s	+17%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	4s	1s	+300%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
`keccak_finalize`	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
`keccak_init`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	3s	2s	+50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_permute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute_native`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	1s	+100%
`keccakf1600x4_permute`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
`keccakf1600x4_permute_native`	LP64	cvc5_arrays_exp	✅	13s	12s	+8%
	LP64	z3*	✅	14s	11s	+27%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_no_bv_extract	✅	2s	5s	-60%
`make_hint`	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	3s	4s	-25%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	✅	249s	250s	-0%
`mld_check_pct`	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	6s	6s	+0%
`mld_compute_pack_z`	LP64	cadical	✅	82s	81s	+1%
	LP64	z3_no_bv_extract*	✅	4s	7s	-43%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	3s	2s	+50%
	ILP32	z3	✅	4s	1s	+300%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_i64`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	47s	45s	+4%
`mld_ct_sel_int32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	3s	-33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	78s	60s	+30%
	LP64	z3_smt_only	✅	90s	86s	+5%
`mld_keccakf1600_extract_bytes`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	1s	3s	-67%
`mld_keccakf1600_permute_c`	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	4s	3s	+33%
`mld_keccakf1600x4_extract_bytes_c`	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mld_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	1s	+100%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	13s	13s	+0%
	LP64	z3_no_bv_extract	✅	64s	62s	+3%
`mld_ntt_layer`	LP64	bitwuzla*	✅	26s	24s	+8%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
`mld_polymat_expand_entry`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
`mld_prepare_domain_separation_prefix`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
`mld_sample_pack_s1_s2`	LP64	cadical	✅	79s	72s	+10%
	LP64	z3*	✅	8s	7s	+14%
`mld_sample_pack_s1_s2_serial`	LP64	cvc5_mbqi_enum	✅	556s	537s	+4%
	LP64	z3*	✅	4s	5s	-20%
`mld_sign_attempt`	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	4s	-50%
`mld_sign_finish`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
`mld_sign_hook_resume`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_i64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u32`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	1s	+300%
`mld_value_barrier_u8`	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	4s	-50%
`montgomery_reduce`	LP64	cvc5_arrays_exp	✅	3s	5s	-40%
	LP64	z3*	✅	2s	4s	-50%
`ntt_native_aarch64`	LP64	bitwuzla	✅	22s	19s	+16%
	LP64	z3*	✅	5s	2s	+150%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	4s	3s	+33%
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	3s	2s	+50%
`ntt_native_x86_64`	LP64	bitwuzla	✅	16s	17s	-6%
	LP64	z3*	✅	2s	6s	-67%
`nttunpack_native_x86_64`	LP64	bitwuzla	✅	188s	177s	+6%
	LP64	z3*	✅	3s	4s	-25%
`pack_sig_c`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	4s	-75%
`pack_sig_h`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
`pack_sig_z`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	3s	+0%
`pointwise_acc_native_aarch64`	LP64	cadical	✅	94s	91s	+3%
	LP64	z3_smt_only*	✅	5s	4s	+25%
`pointwise_acc_native_x86_64`	LP64	cadical	✅	92s	89s	+3%
	LP64	z3_smt_only*	✅	4s	4s	+0%
`pointwise_native_aarch64`	LP64	bitwuzla	✅	22s	20s	+10%
	LP64	z3*	✅	3s	3s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	5s	2s	+150%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	4s	2s	+100%
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	4s	1s	+300%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	2s	2s	+0%
`pointwise_native_x86_64`	LP64	bitwuzla	✅	21s	21s	+0%
	LP64	z3*	✅	5s	3s	+67%
`poly_add`	LP64	cadical	✅	49s	54s	-9%
	LP64	z3*	✅	11s	9s	+22%
`poly_caddq`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	4s	4s	+0%
`poly_caddq_c`	LP64	bitwuzla	✅	19s	19s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native`	LP64	bitwuzla	✅	110s	102s	+8%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	LP64	cvc5_mbqi_enum	✅	34s	34s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	LP64	bitwuzla	✅	133s	99s	+34%
	LP64	z3*	✅	4s	3s	+33%
`poly_challenge`	LP64	bitwuzla	✅	35s	32s	+9%
	LP64	z3*	✅	10s	14s	-29%
`poly_chknorm`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	bitwuzla	✅	9s	8s	+12%
	LP64	z3*	✅	9s	8s	+12%
`poly_chknorm_native`	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_native_aarch64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
`poly_chknorm_native_x86_64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	4s	-75%
`poly_decompose`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	cadical	✅	10s	6s	+67%
	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_88_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_c`	LP64	cvc5_mbqi_enum	✅	224s	217s	+3%
	LP64	z3*	✅	5s	4s	+25%
`poly_decompose_native`	LP64	cadical	✅	15s	14s	+7%
	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	cadical	✅	11s	10s	+10%
	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	3s	5s	-40%
`poly_invntt_tomont_c`	LP64	bitwuzla	✅	160s	151s	+6%
	LP64	z3_smt_only*	✅	7s	4s	+75%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	44s	41s	+7%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_ntt_c`	LP64	bitwuzla	✅	52s	43s	+21%
	LP64	z3_smt_only*	✅	10s	10s	+0%
`poly_ntt_native`	LP64	bitwuzla	✅	28s	26s	+8%
	LP64	z3*	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`poly_permute_bitrev_to_custom_optional_native`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
`poly_pointwise_montgomery`	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	bitwuzla	✅	189s	178s	+6%
	LP64	z3*	✅	80s	62s	+29%
`poly_pointwise_montgomery_native`	LP64	cvc5_mbqi_enum	✅	55s	56s	-2%
	LP64	z3*	✅	5s	2s	+150%
`poly_power2round`	LP64	bitwuzla	✅	313s	256s	+22%
	LP64	z3*	✅	3s	5s	-40%
`poly_reduce`	LP64	bitwuzla	✅	8s	8s	+0%
	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	bitwuzla	✅	11s	11s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_sub`	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_uniform`	LP64	bitwuzla	✅	176s	173s	+2%
	LP64	z3*	✅	4s	2s	+100%
`poly_uniform_4x`	LP64	cadical	✅	61s	60s	+2%
	LP64	z3*	✅	6s	8s	-25%
`poly_uniform_eta`	LP64	bitwuzla	✅	87s	76s	+14%
	LP64	z3*	✅	5s	3s	+67%
`poly_uniform_eta_4x`	LP64	cadical	✅	71s	61s	+16%
	LP64	z3*	✅	11s	8s	+38%
`poly_uniform_gamma1`	LP64	cadical	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_gamma1_4x`	LP64	cadical	✅	12s	10s	+20%
	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint`	LP64	cvc5_mbqi_enum	✅	24s	22s	+9%
	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint_c`	LP64	cvc5_enum_inst	✅	12s	11s	+9%
	LP64	z3*	✅	4s	2s	+100%
`poly_use_hint_native`	LP64	cvc5_mbqi_enum	✅	95s	95s	+0%
	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	bitwuzla	✅	33s	28s	+18%
	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	2s	2s	+0%
`polyeta_pack`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	1s	+300%
`polyeta_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	7s	10s	-30%
`polyt0_pack`	LP64	bitwuzla	✅	7s	4s	+75%
	LP64	z3*	✅	4s	2s	+100%
`polyt0_unpack`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	8s	8s	+0%
`polyt1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
`polyt1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	5s	3s	+67%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	95s	82s	+16%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	27s	25s	+8%
`polyvec_matrix_pointwise_montgomery_row`	LP64	cadical	✅	593s	582s	+2%
	LP64	z3_no_bv_extract*	✅	4s	1s	+300%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	cadical	✅	758s	758s	+0%
	LP64	z3*	✅	7s	6s	+17%
`polyveck_caddq`	LP64	cadical	✅	1219s	1189s	+3%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_decompose_pack_w1`	LP64	cadical	✅	210s	198s	+6%
	LP64	z3*	✅	5s	4s	+25%
`polyveck_invntt_tomont`	LP64	cadical	✅	312s	308s	+1%
	LP64	z3*	✅	4s	4s	+0%
`polyveck_ntt`	LP64	cadical	✅	1068s	1054s	+1%
	LP64	z3*	✅	3s	5s	-40%
`polyveck_reduce`	LP64	cadical	✅	1s	4s	-75%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta`	LP64	cvc5_mbqi_enum	✅	53s	50s	+6%
	LP64	z3*	✅	3s	2s	+50%
`polyveck_unpack_eta_chknorm`	LP64	cvc5_mbqi_enum	✅	19s	18s	+6%
	LP64	z3*	✅	4s	3s	+33%
`polyvecl_chknorm`	LP64	cadical	✅	141s	155s	-9%
	LP64	z3*	✅	2s	3s	-33%
`polyvecl_ntt`	LP64	cadical	✅	238s	182s	+31%
	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	cvc5_mbqi_enum	✅	14s	13s	+8%
	LP64	z3_smt_only*	✅	2s	1s	+100%
`polyvecl_pointwise_acc_montgomery_c`	LP64	cadical	✅	149s	148s	+1%
	LP64	z3_smt_only*	✅	1185s	1031s	+15%
`polyvecl_pointwise_acc_montgomery_native`	LP64	cvc5_mbqi_enum	✅	180s	175s	+3%
	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	cvc5_mbqi_enum	✅	78s	75s	+4%
	LP64	z3*	✅	2s	5s	-60%
`polyvecl_uniform_gamma1_serial`	LP64	cvc5_mbqi_enum	✅	43s	46s	-7%
	LP64	z3*	✅	3s	4s	-25%
`polyvecl_unpack_eta`	LP64	cvc5_mbqi_enum	✅	50s	47s	+6%
	LP64	z3*	✅	3s	5s	-40%
`polyvecl_unpack_z`	LP64	cvc5_mbqi_enum	✅	49s	47s	+4%
	LP64	z3*	✅	3s	2s	+50%
`polyw1_pack`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	4s	+0%
`polyw1_pack_32`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
`polyw1_pack_88`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
`polyw1_unpack_32`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack_88`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
`polyz_pack`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack`	LP64	bitwuzla	✅	7s	7s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	8s	8s	+0%
`polyz_unpack_native`	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_native_x86_64`	LP64	bitwuzla	✅	17s	13s	+31%
	LP64	z3*	✅	4s	3s	+33%
`power2round`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	5s	1s	+400%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	14s	13s	+8%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	17s	18s	-6%
`rej_uniform`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	8s	8s	+0%
`rej_uniform_c`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	16s	15s	+7%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
`rej_uniform_eta_native_x86_64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3_smt_only*	✅	3s	2s	+50%
`rej_uniform_native`	LP64	bitwuzla*	✅	6s	2s	+200%
	LP64	z3_smt_only	✅	12s	9s	+33%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	z3_smt_only	✅	6s	3s	+100%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3_smt_only*	✅	9s	7s	+29%
`shake128_absorb`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`shake128_release`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`shake256`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	1s	+0%
`shake256_absorb`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	1s	+200%
`shake256_finalize`	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	4s	2s	+100%
`shake256_release`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`shake256_squeeze`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	4s	-50%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	4s	2s	+100%
`sig_unpack_hints`	LP64	bitwuzla	✅	24s	24s	+0%
	LP64	z3*	✅	16s	12s	+33%
`sign_keypair`	LP64	cadical	✅	555s	585s	-5%
	LP64	z3*	✅	7s	5s	+40%
`sign_keypair_internal`	LP64	cadical	✅	215s	214s	+0%
	LP64	z3_no_bv_extract*	✅	26s	28s	-7%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	✅	30s	28s	+7%
`sign_signature`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
`sign_signature_extmu`	LP64	cadical	✅	57s	69s	-17%
	LP64	z3*	✅	5s	3s	+67%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	253s	245s	+3%
`sign_signature_pre_hash_internal`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	1s	+300%
`sign_signature_pre_hash_shake256`	LP64	cadical	✅	24s	23s	+4%
	LP64	z3*	✅	4s	5s	-20%
`sign_verify`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	3s	+67%
`sign_verify_extmu`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	1s	3s	-67%
`sign_verify_internal`	LP64	z3_no_bv_extract*	✅	844s	798s	+6%
`sign_verify_pre_hash_internal`	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
`sign_verify_pre_hash_shake256`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
`sk_s1hat_get_poly`	LP64	bitwuzla	✅	32s	31s	+3%
	LP64	z3*	✅	3s	2s	+50%
`sk_s2hat_get_poly`	LP64	bitwuzla	✅	34s	34s	+0%
	LP64	z3*	✅	1s	2s	-50%
`sk_t0hat_get_poly`	LP64	bitwuzla	✅	37s	32s	+16%
	LP64	z3*	✅	2s	3s	-33%
`sys_check_capability`	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	3s	1s	+200%
`unpack_pk_t1`	LP64	bitwuzla	✅	13s	13s	+0%
	LP64	z3*	✅	2s	1s	+100%
`unpack_sk`	LP64	cadical	✅	74s	63s	+17%
	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	cvc5_mbqi_enum	✅	90s	86s	+5%
	LP64	z3*	✅	3s	4s	-25%
`unpack_sk_s2hat`	LP64	cvc5_mbqi_enum	✅	318s	307s	+4%
	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	cadical	✅	109s	112s	-3%
	LP64	z3*	✅	3s	4s	-25%
`use_hint`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	bitwuzla	✅	36s	40s	-10%
	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	bitwuzla	✅	18s	14s	+29%
	LP64	z3*	✅	1s	4s	-75%

mkannwischer added 3 commits November 5, 2026 15:37

mkannwischer marked this pull request as ready for review November 5, 2026 11:54

mkannwischer requested a review from a team as a code owner November 5, 2026 11:54

mkannwischer added this to the v2.1 milestone Nov 9, 2026

Navigation Menu

Repository navigation

Port abicheck: Use the native build's CPU feature flags - #1532

Port abicheck: Use the native build's CPU feature flags#1532
mkannwischer wants to merge 3 commits into
mainfrom
port-abicheck-cpu-flags

mkannwischer commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mkannwischer commented Nov 5, 2026

Uh oh!

oqs-bot commented Nov 5, 2026

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

Uh oh!

oqs-bot commented Nov 5, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Nov 5, 2026

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

Uh oh!

oqs-bot commented Nov 5, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Nov 5, 2026

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

Uh oh!

oqs-bot commented Nov 5, 2026

CBMC Results (ML-DSA-87)

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants