Skip to content

CBMC: Add a second solver for 2 slow proofs - #1496

Draft
mkannwischer wants to merge 2 commits into
mainfrom
cbmc-slow-second-solvers
Draft

CBMC: Add a second solver for 2 slow proofs#1496
mkannwischer wants to merge 2 commits into
mainfrom
cbmc-slow-second-solvers

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@oqs-bot

oqs-bot commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

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

@oqs-bot

oqs-bot commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

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

@oqs-bot

oqs-bot commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

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

@oqs-bot

oqs-bot commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

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

@mkannwischer
CBMC: Add CaDiCaL SAT profile
3554de7 
Add a cadical solver profile that uses CBMC's propositional backend
with CaDiCaL instead of an SMT solver.

Use it as a second solver for 10 proofs that discharge in about 150s
or less locally for ML-DSA-87, for which the SMT alternatives
timed out, returned unknown or were too slow.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
CBMC: Add a second solver for 2 slow proofs
8242234 
Add cvc5_mbqi_enum as a second solver for poly_decompose_c and cadical
as a second solver for sign_keypair_internal.

These are quite slow: locally for ML-DSA-87, poly_decompose_c takes
about 370s with cvc5_mbqi_enum and sign_keypair_internal about 385s
with cadical. No faster non-Z3 option was found for them.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
mkannwischer force-pushed the cbmc-slow-second-solvers branch from c4f91f2 to 8242234 Compare October 26, 2026 05:21

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mkannwischer @oqs-bot