[mkannwischer]

Check ||w0 - cs2||_inf < GAMMA2 - BETA before ||z||_inf < GAMMA1 - BETA, and compute ct0 along with its norm check in a separate loop after the check on z.

Both loops and mld_compute_pack_z stop at the first polynomial that fails their check, so an attempt is cheapest when the check that rejects most often per polynomial runs first.

Thanks to Georg Land for pointing out that this is faster.

[github-actions]

Mac Mini (M1, 2020) benchmarks (opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	46483 cycles	46495 cycles	1.00
ML-DSA-44 sign	126277 cycles	131379 cycles	0.96
ML-DSA-44 verify	47328 cycles	47329 cycles	1.00
ML-DSA-65 keypair	81684 cycles	81688 cycles	1.00
ML-DSA-65 sign	203626 cycles	215251 cycles	0.95
ML-DSA-65 verify	79296 cycles	79300 cycles	1.00
ML-DSA-87 keypair	132436 cycles	132342 cycles	1.00
ML-DSA-87 sign	264823 cycles	277355 cycles	0.95
ML-DSA-87 verify	137040 cycles	137009 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A55 (Snapdragon 888) benchmarks (opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	267076 cycles	271362 cycles	0.98
ML-DSA-44 sign	768789 cycles	821847 cycles	0.94
ML-DSA-44 verify	268922 cycles	275728 cycles	0.98
ML-DSA-65 keypair	462364 cycles	465556 cycles	0.99
ML-DSA-65 sign	1234780 cycles	1335846 cycles	0.92
ML-DSA-65 verify	447107 cycles	454969 cycles	0.98
ML-DSA-87 keypair	788186 cycles	797505 cycles	0.99
ML-DSA-87 sign	1693254 cycles	1842068 cycles	0.92
ML-DSA-87 verify	769006 cycles	772926 cycles	0.99

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Mac Mini (M1, 2020) benchmarks (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	113344 cycles	112827 cycles	1.00
ML-DSA-44 sign	389337 cycles	402496 cycles	0.97
ML-DSA-44 verify	120087 cycles	119365 cycles	1.01
ML-DSA-65 keypair	192979 cycles	193024 cycles	1.00
ML-DSA-65 sign	607732 cycles	651437 cycles	0.93
ML-DSA-65 verify	193079 cycles	192987 cycles	1.00
ML-DSA-87 keypair	318985 cycles	318856 cycles	1.00
ML-DSA-87 sign	786008 cycles	831314 cycles	0.95
ML-DSA-87 verify	325787 cycles	325766 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	43504 cycles	43490 cycles	1.00
ML-DSA-44 sign	125230 cycles	130374 cycles	0.96
ML-DSA-44 verify	45467 cycles	45520 cycles	1.00
ML-DSA-65 keypair	75839 cycles	76087 cycles	1.00
ML-DSA-65 sign	199703 cycles	213837 cycles	0.93
ML-DSA-65 verify	74685 cycles	74906 cycles	1.00
ML-DSA-87 keypair	123539 cycles	123169 cycles	1.00
ML-DSA-87 sign	257464 cycles	271033 cycles	0.95
ML-DSA-87 verify	120914 cycles	120541 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Intel Xeon 4th gen (c7i) (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	92027 cycles	91856 cycles	1.00
ML-DSA-44 sign	335496 cycles	347728 cycles	0.96
ML-DSA-44 verify	99573 cycles	99470 cycles	1.00
ML-DSA-65 keypair	154185 cycles	154288 cycles	1.00
ML-DSA-65 sign	528846 cycles	565330 cycles	0.94
ML-DSA-65 verify	158879 cycles	159320 cycles	1.00
ML-DSA-87 keypair	255300 cycles	255280 cycles	1.00
ML-DSA-87 sign	683414 cycles	724481 cycles	0.94
ML-DSA-87 verify	265647 cycles	263908 cycles	1.01

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

AMD EPYC 4th gen (c7a)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	46966 cycles	47122 cycles	1.00
ML-DSA-44 sign	135193 cycles	139708 cycles	0.97
ML-DSA-44 verify	49509 cycles	49493 cycles	1.00
ML-DSA-65 keypair	82102 cycles	82609 cycles	0.99
ML-DSA-65 sign	215204 cycles	228035 cycles	0.94
ML-DSA-65 verify	82418 cycles	82590 cycles	1.00
ML-DSA-87 keypair	130554 cycles	135639 cycles	0.96
ML-DSA-87 sign	265794 cycles	297917 cycles	0.89
ML-DSA-87 verify	128188 cycles	138079 cycles	0.93

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

AMD EPYC 3rd gen (c6a)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	52000 cycles	51939 cycles	1.00
ML-DSA-44 sign	149041 cycles	156000 cycles	0.96
ML-DSA-44 verify	54150 cycles	54123 cycles	1.00
ML-DSA-65 keypair	90040 cycles	89968 cycles	1.00
ML-DSA-65 sign	238806 cycles	253225 cycles	0.94
ML-DSA-65 verify	90688 cycles	89944 cycles	1.01
ML-DSA-87 keypair	144075 cycles	144818 cycles	0.99
ML-DSA-87 sign	291390 cycles	311705 cycles	0.93
ML-DSA-87 verify	138819 cycles	139540 cycles	0.99

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

AMD EPYC 4th gen (c7a) (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	130153 cycles	118984 cycles	1.09
ML-DSA-44 sign	465144 cycles	457223 cycles	1.02
ML-DSA-44 verify	136543 cycles	131208 cycles	1.04
ML-DSA-65 keypair	201668 cycles	201145 cycles	1.00
ML-DSA-65 sign	690959 cycles	742379 cycles	0.93
ML-DSA-65 verify	210334 cycles	210357 cycles	1.00
ML-DSA-87 keypair	330759 cycles	331120 cycles	1.00
ML-DSA-87 sign	885955 cycles	937547 cycles	0.94
ML-DSA-87 verify	343797 cycles	344646 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'AMD EPYC 4th gen (c7a) (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	130153 cycles	118984 cycles	1.09
ML-DSA-44 verify	136543 cycles	131208 cycles	1.04

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

AMD EPYC 3rd gen (c6a) (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	136700 cycles	133390 cycles	1.02
ML-DSA-44 sign	509354 cycles	520419 cycles	0.98
ML-DSA-44 verify	149320 cycles	147163 cycles	1.01
ML-DSA-65 keypair	226418 cycles	224254 cycles	1.01
ML-DSA-65 sign	791338 cycles	847424 cycles	0.93
ML-DSA-65 verify	236618 cycles	234487 cycles	1.01
ML-DSA-87 keypair	368243 cycles	374067 cycles	0.98
ML-DSA-87 sign	997011 cycles	1077560 cycles	0.93
ML-DSA-87 verify	381585 cycles	387046 cycles	0.99

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Intel Xeon 3rd gen (c6i)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	61814 cycles	61880 cycles	1.00
ML-DSA-44 sign	180420 cycles	188999 cycles	0.95
ML-DSA-44 verify	66341 cycles	66270 cycles	1.00
ML-DSA-65 keypair	111270 cycles	108610 cycles	1.02
ML-DSA-65 sign	293308 cycles	311200 cycles	0.94
ML-DSA-65 verify	109878 cycles	108850 cycles	1.01
ML-DSA-87 keypair	172071 cycles	170415 cycles	1.01
ML-DSA-87 sign	360965 cycles	379059 cycles	0.95
ML-DSA-87 verify	173187 cycles	169838 cycles	1.02

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Intel Xeon 3rd gen (c6i) (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	153928 cycles	154089 cycles	1.00
ML-DSA-44 sign	565915 cycles	588454 cycles	0.96
ML-DSA-44 verify	168942 cycles	168985 cycles	1.00
ML-DSA-65 keypair	261111 cycles	262084 cycles	1.00
ML-DSA-65 sign	892477 cycles	957523 cycles	0.93
ML-DSA-65 verify	271433 cycles	271777 cycles	1.00
ML-DSA-87 keypair	431696 cycles	432435 cycles	1.00
ML-DSA-87 sign	1144218 cycles	1211727 cycles	0.94
ML-DSA-87 verify	446747 cycles	446648 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton5

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	51436 cycles	51545 cycles	1.00
ML-DSA-44 sign	155076 cycles	162250 cycles	0.96
ML-DSA-44 verify	54819 cycles	54707 cycles	1.00
ML-DSA-65 keypair	90196 cycles	90155 cycles	1.00
ML-DSA-65 sign	248768 cycles	266210 cycles	0.93
ML-DSA-65 verify	89976 cycles	89817 cycles	1.00
ML-DSA-87 keypair	145946 cycles	145919 cycles	1.00
ML-DSA-87 sign	316757 cycles	335543 cycles	0.94
ML-DSA-87 verify	144938 cycles	145468 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A55 (Snapdragon 888) benchmarks (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	462444 cycles	465447 cycles	0.99
ML-DSA-44 sign	2045365 cycles	2139526 cycles	0.96
ML-DSA-44 verify	555007 cycles	556637 cycles	1.00
ML-DSA-65 keypair	781227 cycles	784251 cycles	1.00
ML-DSA-65 sign	3197624 cycles	3492484 cycles	0.92
ML-DSA-65 verify	864436 cycles	867152 cycles	1.00
ML-DSA-87 keypair	1261446 cycles	1264532 cycles	1.00
ML-DSA-87 sign	4010388 cycles	4319116 cycles	0.93
ML-DSA-87 verify	1386616 cycles	1392230 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	112180 cycles	112287 cycles	1.00
ML-DSA-44 sign	340501 cycles	354101 cycles	0.96
ML-DSA-44 verify	117258 cycles	117167 cycles	1.00
ML-DSA-65 keypair	194399 cycles	194666 cycles	1.00
ML-DSA-65 sign	544990 cycles	583246 cycles	0.93
ML-DSA-65 verify	193236 cycles	193114 cycles	1.00
ML-DSA-87 keypair	320046 cycles	321100 cycles	1.00
ML-DSA-87 sign	707638 cycles	747925 cycles	0.95
ML-DSA-87 verify	317779 cycles	318764 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton5 (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	100293 cycles	99958 cycles	1.00
ML-DSA-44 sign	355113 cycles	369441 cycles	0.96
ML-DSA-44 verify	110582 cycles	110183 cycles	1.00
ML-DSA-65 keypair	175331 cycles	176088 cycles	1.00
ML-DSA-65 sign	555087 cycles	596658 cycles	0.93
ML-DSA-65 verify	177767 cycles	177613 cycles	1.00
ML-DSA-87 keypair	285187 cycles	286628 cycles	0.99
ML-DSA-87 sign	715875 cycles	758172 cycles	0.94
ML-DSA-87 verify	296824 cycles	295695 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton4

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	67422 cycles	67200 cycles	1.00
ML-DSA-44 sign	190932 cycles	198799 cycles	0.96
ML-DSA-44 verify	70378 cycles	70440 cycles	1.00
ML-DSA-65 keypair	119289 cycles	119573 cycles	1.00
ML-DSA-65 sign	305593 cycles	325662 cycles	0.94
ML-DSA-65 verify	116785 cycles	117090 cycles	1.00
ML-DSA-87 keypair	196705 cycles	196352 cycles	1.00
ML-DSA-87 sign	401801 cycles	420686 cycles	0.96
ML-DSA-87 verify	193245 cycles	192912 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	211730 cycles	212139 cycles	1.00
ML-DSA-44 sign	734098 cycles	760267 cycles	0.97
ML-DSA-44 verify	229532 cycles	229531 cycles	1.00
ML-DSA-65 keypair	375430 cycles	376003 cycles	1.00
ML-DSA-65 sign	1162783 cycles	1245016 cycles	0.93
ML-DSA-65 verify	371803 cycles	371755 cycles	1.00
ML-DSA-87 keypair	601690 cycles	601186 cycles	1.00
ML-DSA-87 sign	1500896 cycles	1583247 cycles	0.95
ML-DSA-87 verify	617436 cycles	616849 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton4 (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	127826 cycles	127783 cycles	1.00
ML-DSA-44 sign	425885 cycles	442225 cycles	0.96
ML-DSA-44 verify	136437 cycles	136517 cycles	1.00
ML-DSA-65 keypair	223200 cycles	223479 cycles	1.00
ML-DSA-65 sign	667955 cycles	714516 cycles	0.93
ML-DSA-65 verify	220944 cycles	220881 cycles	1.00
ML-DSA-87 keypair	365026 cycles	365589 cycles	1.00
ML-DSA-87 sign	910819 cycles	958728 cycles	0.95
ML-DSA-87 verify	371422 cycles	371278 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton3

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	71587 cycles	71487 cycles	1.00
ML-DSA-44 sign	202042 cycles	210224 cycles	0.96
ML-DSA-44 verify	74958 cycles	74917 cycles	1.00
ML-DSA-65 keypair	126032 cycles	126188 cycles	1.00
ML-DSA-65 sign	324680 cycles	344959 cycles	0.94
ML-DSA-65 verify	124159 cycles	124325 cycles	1.00
ML-DSA-87 keypair	206662 cycles	206913 cycles	1.00
ML-DSA-87 sign	423495 cycles	444505 cycles	0.95
ML-DSA-87 verify	204723 cycles	204416 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton3 (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	138343 cycles	138325 cycles	1.00
ML-DSA-44 sign	470222 cycles	488151 cycles	0.96
ML-DSA-44 verify	149475 cycles	149578 cycles	1.00
ML-DSA-65 keypair	242575 cycles	242073 cycles	1.00
ML-DSA-65 sign	739545 cycles	792009 cycles	0.93
ML-DSA-65 verify	242027 cycles	241892 cycles	1.00
ML-DSA-87 keypair	395811 cycles	396711 cycles	1.00
ML-DSA-87 sign	1007776 cycles	1059889 cycles	0.95
ML-DSA-87 verify	404966 cycles	404586 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton2

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	112184 cycles	112244 cycles	1.00
ML-DSA-44 sign	340803 cycles	354631 cycles	0.96
ML-DSA-44 verify	117435 cycles	117405 cycles	1.00
ML-DSA-65 keypair	194508 cycles	194595 cycles	1.00
ML-DSA-65 sign	545448 cycles	583758 cycles	0.93
ML-DSA-65 verify	193594 cycles	193536 cycles	1.00
ML-DSA-87 keypair	320488 cycles	320476 cycles	1.00
ML-DSA-87 sign	708659 cycles	746827 cycles	0.95
ML-DSA-87 verify	318427 cycles	317877 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

Graviton2 (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	211908 cycles	211929 cycles	1.00
ML-DSA-44 sign	735842 cycles	760854 cycles	0.97
ML-DSA-44 verify	229369 cycles	229874 cycles	1.00
ML-DSA-65 keypair	375079 cycles	376701 cycles	1.00
ML-DSA-65 sign	1163391 cycles	1247378 cycles	0.93
ML-DSA-65 verify	371247 cycles	372579 cycles	1.00
ML-DSA-87 keypair	601033 cycles	602349 cycles	1.00
ML-DSA-87 sign	1541924 cycles	1587832 cycles	0.97
ML-DSA-87 verify	616742 cycles	618624 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[oqs-bot]

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

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1373s	1307s	+5.0%
caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	28s	26s	+8%
decompose	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
fqmul	LP64	bitwuzla*	✅	27s	25s	+8%
	LP64	z3_smt_only	✅	21s	18s	+17%
fqscale	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	3s	+0%
intt_native_aarch64	LP64	bitwuzla	✅	25s	19s	+32%
	LP64	z3*	✅	2s	3s	-33%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	7s	+0%
	LP64	z3	✅	2s	2s	+0%
intt_native_rv32im_slowmul	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	6s	8s	-25%
	LP64	z3	✅	2s	5s	-60%
intt_native_x86_64	LP64	bitwuzla	✅	18s	18s	+0%
	LP64	z3*	✅	3s	2s	+50%
keccak_absorb	LP64	cvc5_arrays_exp	✅	3s	6s	-50%
	LP64	z3*	✅	7s	6s	+17%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	10s	8s	+25%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	1s	3s	-67%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	1s	+100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	1s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
keccak_finalize	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
keccak_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
keccak_squeeze	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	3s	2s	+50%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	2s	1s	+100%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute_native	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	4s	3s	+33%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	3s	2s	+50%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	13s	11s	+18%
	LP64	z3*	✅	13s	12s	+8%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_no_bv_extract	✅	1s	3s	-67%
make_hint	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	152s	157s	-3%
mld_check_pct	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	6s	7s	-14%
mld_compute_pack_z	LP64	cadical	✅	39s	37s	+5%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
mld_ct_abs_i32	ILP32	bitwuzla	✅	3s	3s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	4s	-50%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	3s	-33%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	50s	46s	+9%
mld_ct_sel_int32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_h	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
mld_invntt_layer	LP64	bitwuzla*	✅	74s	60s	+23%
	LP64	z3_smt_only	✅	88s	74s	+19%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	5s	3s	+67%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	4s	-75%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	12s	13s	-8%
	LP64	z3_no_bv_extract	✅	216s	183s	+18%
mld_ntt_layer	LP64	bitwuzla*	✅	27s	27s	+0%
	LP64	z3_no_bv_extract	✅	3s	1s	+200%
mld_polymat_expand_entry	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	2s	+100%
mld_sample_pack_s1_s2	LP64	cadical	✅	76s	73s	+4%
	LP64	z3*	✅	5s	6s	-17%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	554s	539s	+3%
	LP64	z3*	✅	4s	4s	+0%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
mld_sign_finish	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
mld_sign_hook_resume	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
mld_value_barrier_i64	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
mld_value_barrier_u32	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	4s	2s	+100%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
ntt_native_aarch64	LP64	bitwuzla	✅	22s	19s	+16%
	LP64	z3*	✅	2s	4s	-50%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	5s	6s	-17%
	LP64	z3	✅	1s	2s	-50%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	6s	6s	+0%
	LP64	z3	✅	4s	1s	+300%
ntt_native_x86_64	LP64	bitwuzla	✅	21s	18s	+17%
	LP64	z3*	✅	2s	3s	-33%
nttunpack_native_x86_64	LP64	bitwuzla	✅	183s	162s	+13%
	LP64	z3*	✅	1s	1s	+0%
pack_sig_c	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
pack_sig_h	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
pack_sig_z	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
pointwise_acc_native_aarch64	LP64	cadical	✅	92s	89s	+3%
	LP64	z3_smt_only*	✅	5s	4s	+25%
pointwise_acc_native_x86_64	LP64	cadical	✅	96s	95s	+1%
	LP64	z3_smt_only*	✅	5s	4s	+25%
pointwise_native_aarch64	LP64	bitwuzla	✅	22s	21s	+5%
	LP64	z3*	✅	2s	1s	+100%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	2s	1s	+100%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	3s	1s	+200%
	LP64	cvc5_mbqi_enum	✅	4s	9s	-56%
	LP64	z3	✅	2s	3s	-33%
pointwise_native_x86_64	LP64	bitwuzla	✅	25s	22s	+14%
	LP64	z3*	✅	3s	3s	+0%
poly_add	LP64	cadical	✅	52s	47s	+11%
	LP64	z3*	✅	10s	10s	+0%
poly_caddq	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
poly_caddq_c	LP64	bitwuzla	✅	22s	19s	+16%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native	LP64	bitwuzla	✅	127s	109s	+17%
	LP64	z3*	✅	3s	1s	+200%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	38s	36s	+6%
	LP64	z3*	✅	3s	4s	-25%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	139s	120s	+16%
	LP64	z3*	✅	2s	1s	+100%
poly_challenge	LP64	bitwuzla	✅	37s	33s	+12%
	LP64	z3*	✅	11s	11s	+0%
poly_chknorm	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
poly_chknorm_c	LP64	bitwuzla	✅	12s	10s	+20%
	LP64	z3*	✅	8s	7s	+14%
poly_chknorm_native	LP64	bitwuzla	✅	5s	7s	-29%
	LP64	z3*	✅	5s	3s	+67%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	2s	+100%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	3s	+0%
poly_decompose	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	8s	7s	+14%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
poly_decompose_c	LP64	cvc5_mbqi_enum	✅	244s	194s	+26%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_native	LP64	cadical	✅	14s	13s	+8%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_native_x86_64	LP64	cadical	✅	11s	11s	+0%
	LP64	z3*	✅	3s	2s	+50%
poly_invntt_tomont	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	1s	1s	+0%
poly_invntt_tomont_c	LP64	bitwuzla	✅	164s	152s	+8%
	LP64	z3_smt_only*	✅	4s	5s	-20%
poly_invntt_tomont_native	LP64	bitwuzla	✅	48s	43s	+12%
	LP64	z3*	✅	4s	2s	+100%
poly_ntt	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_ntt_c	LP64	bitwuzla	✅	58s	43s	+35%
	LP64	z3_smt_only*	✅	10s	10s	+0%
poly_ntt_native	LP64	bitwuzla	✅	29s	25s	+16%
	LP64	z3*	✅	3s	2s	+50%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	4s	2s	+100%
poly_pointwise_montgomery	LP64	bitwuzla	✅	11s	12s	-8%
	LP64	z3*	✅	3s	3s	+0%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	209s	184s	+14%
	LP64	z3*	✅	44s	37s	+19%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	56s	57s	-2%
	LP64	z3*	✅	2s	3s	-33%
poly_power2round	LP64	bitwuzla	✅	336s	253s	+33%
	LP64	z3*	✅	3s	1s	+200%
poly_reduce	LP64	bitwuzla	✅	8s	6s	+33%
	LP64	z3*	✅	2s	2s	+0%
poly_shiftl	LP64	bitwuzla	✅	11s	12s	-8%
	LP64	z3*	✅	2s	3s	-33%
poly_sub	LP64	bitwuzla	✅	15s	13s	+15%
	LP64	z3*	✅	3s	2s	+50%
poly_uniform	LP64	bitwuzla	✅	203s	176s	+15%
	LP64	z3*	✅	2s	4s	-50%
poly_uniform_4x	LP64	cadical	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
poly_uniform_eta	LP64	bitwuzla	✅	85s	76s	+12%
	LP64	z3*	✅	4s	2s	+100%
poly_uniform_eta_4x	LP64	cadical	✅	65s	62s	+5%
	LP64	z3*	✅	10s	7s	+43%
poly_uniform_gamma1	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
poly_uniform_gamma1_4x	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	24s	22s	+9%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	13s	9s	+44%
	LP64	z3*	✅	4s	4s	+0%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	89s	93s	-4%
	LP64	z3*	✅	4s	4s	+0%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	33s	29s	+14%
	LP64	z3*	✅	4s	1s	+300%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	32s	28s	+14%
	LP64	z3*	✅	1s	3s	-67%
polyeta_pack	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	1s	3s	-67%
polyeta_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	11s	8s	+38%
polyt0_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
polyt0_unpack	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	10s	10s	+0%
polyt1_pack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	4s	3s	+33%
polyt1_unpack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	4s	+0%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
polyvec_matrix_expand_serial	LP64	z3*	✅	2s	2s	+0%
polyvec_matrix_pointwise_montgomery_row	LP64	cadical	✅	49s	45s	+9%
	LP64	z3_no_bv_extract*	✅	2s	5s	-60%
polyvec_matrix_pointwise_montgomery_yvec	LP64	cadical	✅	1389s	1272s	+9%
	LP64	z3*	✅	111s	101s	+10%
polyveck_caddq	LP64	cadical	✅	1247s	1199s	+4%
	LP64	z3*	✅	3s	2s	+50%
polyveck_decompose_pack_w1	LP64	cadical	✅	262s	200s	+31%
	LP64	z3*	✅	2s	6s	-67%
polyveck_invntt_tomont	LP64	cadical	✅	330s	309s	+7%
	LP64	z3*	✅	4s	4s	+0%
polyveck_ntt	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	2s	3s	-33%
polyveck_reduce	LP64	cadical	✅	269s	257s	+5%
	LP64	z3*	✅	2s	2s	+0%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	19s	18s	+6%
	LP64	z3*	✅	1s	1s	+0%
polyvecl_chknorm	LP64	cadical	✅	143s	137s	+4%
	LP64	z3*	✅	2s	5s	-60%
polyvecl_ntt	LP64	cadical	✅	197s	187s	+5%
	LP64	z3*	✅	5s	3s	+67%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	4s	3s	+33%
	LP64	z3_smt_only*	✅	2s	3s	-33%
polyvecl_pointwise_acc_montgomery_c	LP64	cadical	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	1s	3s	-67%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	4s	2s	+100%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	51s	49s	+4%
	LP64	z3*	✅	3s	1s	+200%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	48s	46s	+4%
	LP64	z3*	✅	3s	1s	+200%
polyw1_pack	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	2s	+50%
polyw1_pack_32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack_88	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	4s	-75%
polyw1_unpack	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	2s	+50%
polyw1_unpack_32	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	3s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
polyz_pack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
polyz_unpack	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3*	✅	4s	3s	+33%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_c	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	3s	+33%
polyz_unpack_native	LP64	bitwuzla	✅	28s	24s	+17%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	16s	14s	+14%
	LP64	z3*	✅	2s	3s	-33%
power2round	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
reduce32	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
rej_eta	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
rej_eta_c	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3	✅	14s	12s	+17%
rej_eta_native	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	21s	16s	+31%
rej_uniform	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	11s	9s	+22%
rej_uniform_c	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	9s	7s	+29%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	3s	3s	+0%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3_smt_only*	✅	1s	2s	-50%
rej_uniform_native	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	11s	10s	+10%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3_smt_only*	✅	11s	9s	+22%
shake128_absorb	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
shake128_finalize	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake128_init	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
shake128_release	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
shake128_squeeze	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
shake128x4_absorb_once	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	1s	+0%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	2s	-50%
shake256	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
shake256_absorb	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
shake256_finalize	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	3s	2s	+50%
shake256_init	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
shake256_release	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake256_squeeze	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
shake256x4_absorb_once	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
sig_unpack_hints	LP64	bitwuzla	✅	27s	22s	+23%
	LP64	z3*	✅	41s	37s	+11%
sign_keypair	LP64	cadical	✅	650s	533s	+22%
	LP64	z3*	✅	3s	6s	-50%
sign_keypair_internal	LP64	cadical	✅	229s	217s	+6%
	LP64	z3_no_bv_extract*	✅	17s	18s	-6%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	30s	25s	+20%
sign_signature	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_extmu	LP64	cadical	✅	62s	54s	+15%
	LP64	z3*	✅	3s	3s	+0%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	15s	13s	+15%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	2s	+50%
sign_signature_pre_hash_shake256	LP64	cadical	✅	23s	23s	+0%
	LP64	z3*	✅	4s	5s	-20%
sign_verify	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	2s	1s	+100%
sign_verify_extmu	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	4s	-25%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	201s	189s	+6%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	2s	-50%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	6s	-50%
sk_s1hat_get_poly	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
sk_s2hat_get_poly	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
sk_t0hat_get_poly	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
sys_check_capability	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
unpack_pk_t1	LP64	bitwuzla	✅	10s	13s	-23%
	LP64	z3*	✅	1s	3s	-67%
unpack_sk	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk_t0hat	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
use_hint	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
yvec_get_poly	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	4s	-75%
yvec_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%

[oqs-bot]

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

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1288s	1243s	+3.6%
caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	5s	-20%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	31s	31s	+0%
decompose	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
fqmul	LP64	bitwuzla*	✅	25s	25s	+0%
	LP64	z3_smt_only	✅	22s	19s	+16%
fqscale	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	4s	2s	+100%
intt_native_aarch64	LP64	bitwuzla	✅	24s	24s	+0%
	LP64	z3*	✅	2s	1s	+100%
intt_native_rv32im_fastmul	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	8s	7s	+14%
	LP64	z3	✅	3s	4s	-25%
intt_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	3s	3s	+0%
intt_native_x86_64	LP64	bitwuzla	✅	17s	18s	-6%
	LP64	z3*	✅	4s	1s	+300%
keccak_absorb	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	5s	7s	-29%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	cvc5_arrays_exp	✅	9s	8s	+12%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	6s	3s	+100%
	LP64	z3_no_bv_extract	✅	4s	2s	+100%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	3s	+0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	3s	-33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
keccak_finalize	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
keccak_init	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
keccak_squeeze	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
keccakf1600_permute	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
keccakf1600_permute_native	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	1s	+200%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	12s	14s	-14%
	LP64	z3*	✅	14s	12s	+17%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
make_hint	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	159s	114s	+39%
mld_check_pct	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	3s	4s	-25%
mld_compute_pack_z	LP64	cadical	✅	35s	39s	-10%
	LP64	z3_no_bv_extract*	✅	3s	4s	-25%
mld_ct_abs_i32	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+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	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	2s	2s	+0%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	47s	51s	-8%
mld_ct_sel_int32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
mld_h	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
mld_invntt_layer	LP64	bitwuzla*	✅	67s	72s	-7%
	LP64	z3_smt_only	✅	78s	83s	-6%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	4s	4s	+0%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	12s	14s	-14%
	LP64	z3_no_bv_extract	✅	193s	213s	-9%
mld_ntt_layer	LP64	bitwuzla*	✅	26s	29s	-10%
	LP64	z3_no_bv_extract	✅	4s	3s	+33%
mld_polymat_expand_entry	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
mld_sample_pack_s1_s2	LP64	cadical	✅	53s	46s	+15%
	LP64	z3*	✅	3s	4s	-25%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	229s	237s	-3%
	LP64	z3*	✅	2s	2s	+0%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	1s	1s	+0%
mld_sign_finish	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
mld_sign_hook_resume	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	3s	+33%
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	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
ntt_native_aarch64	LP64	bitwuzla	✅	22s	20s	+10%
	LP64	z3*	✅	2s	2s	+0%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	5s	6s	-17%
	LP64	z3	✅	1s	2s	-50%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	6s	6s	+0%
	LP64	z3	✅	2s	2s	+0%
ntt_native_x86_64	LP64	bitwuzla	✅	20s	22s	-9%
	LP64	z3*	✅	2s	3s	-33%
nttunpack_native_x86_64	LP64	bitwuzla	✅	173s	208s	-17%
	LP64	z3*	✅	2s	2s	+0%
pack_sig_c	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
pack_sig_h	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3_no_bv_extract*	✅	1s	1s	+0%
pack_sig_z	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
pointwise_acc_native_aarch64	LP64	cadical	✅	80s	81s	-1%
	LP64	z3_smt_only*	✅	2s	3s	-33%
pointwise_acc_native_x86_64	LP64	cadical	✅	77s	80s	-4%
	LP64	z3_smt_only*	✅	5s	2s	+150%
pointwise_native_aarch64	LP64	bitwuzla	✅	21s	23s	-9%
	LP64	z3*	✅	4s	3s	+33%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	2s	3s	-33%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	9s	+0%
	LP64	z3	✅	3s	3s	+0%
pointwise_native_x86_64	LP64	bitwuzla	✅	23s	24s	-4%
	LP64	z3*	✅	3s	3s	+0%
poly_add	LP64	cadical	✅	49s	50s	-2%
	LP64	z3*	✅	10s	13s	-23%
poly_caddq	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
poly_caddq_c	LP64	bitwuzla	✅	18s	19s	-5%
	LP64	z3*	✅	3s	4s	-25%
poly_caddq_native	LP64	bitwuzla	✅	114s	123s	-7%
	LP64	z3*	✅	1s	3s	-67%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	35s	37s	-5%
	LP64	z3*	✅	5s	2s	+150%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	126s	136s	-7%
	LP64	z3*	✅	2s	2s	+0%
poly_challenge	LP64	bitwuzla	✅	24s	25s	-4%
	LP64	z3*	✅	11s	13s	-15%
poly_chknorm	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
poly_chknorm_c	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	7s	8s	-12%
poly_chknorm_native	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	3s	2s	+50%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	9s	8s	+12%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_c	LP64	cvc5_mbqi_enum	✅	241s	258s	-7%
	LP64	z3*	✅	1s	3s	-67%
poly_decompose_native	LP64	cadical	✅	13s	13s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_native_x86_64	LP64	cadical	✅	9s	8s	+12%
	LP64	z3*	✅	2s	1s	+100%
poly_invntt_tomont	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	1s	+0%
poly_invntt_tomont_c	LP64	bitwuzla	✅	158s	172s	-8%
	LP64	z3_smt_only*	✅	4s	4s	+0%
poly_invntt_tomont_native	LP64	bitwuzla	✅	44s	53s	-17%
	LP64	z3*	✅	2s	3s	-33%
poly_ntt	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	4s	2s	+100%
poly_ntt_c	LP64	bitwuzla	✅	50s	53s	-6%
	LP64	z3_smt_only*	✅	10s	10s	+0%
poly_ntt_native	LP64	bitwuzla	✅	26s	29s	-10%
	LP64	z3*	✅	1s	2s	-50%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
poly_pointwise_montgomery	LP64	bitwuzla	✅	10s	10s	+0%
	LP64	z3*	✅	1s	2s	-50%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	197s	203s	-3%
	LP64	z3*	✅	38s	39s	-3%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	53s	56s	-5%
	LP64	z3*	✅	3s	1s	+200%
poly_power2round	LP64	bitwuzla	✅	315s	308s	+2%
	LP64	z3*	✅	1s	2s	-50%
poly_reduce	LP64	bitwuzla	✅	9s	8s	+12%
	LP64	z3*	✅	3s	3s	+0%
poly_shiftl	LP64	bitwuzla	✅	14s	14s	+0%
	LP64	z3*	✅	3s	2s	+50%
poly_sub	LP64	bitwuzla	✅	15s	15s	+0%
	LP64	z3*	✅	3s	4s	-25%
poly_uniform	LP64	bitwuzla	✅	185s	168s	+10%
	LP64	z3*	✅	4s	1s	+300%
poly_uniform_4x	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_eta	LP64	bitwuzla	✅	57s	57s	+0%
	LP64	z3*	✅	3s	4s	-25%
poly_uniform_eta_4x	LP64	cadical	✅	57s	55s	+4%
	LP64	z3*	✅	8s	9s	-11%
poly_uniform_gamma1	LP64	cadical	✅	2s	4s	-50%
	LP64	z3*	✅	1s	1s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	22s	23s	-4%
	LP64	z3*	✅	3s	3s	+0%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	13s	12s	+8%
	LP64	z3*	✅	4s	5s	-20%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	86s	84s	+2%
	LP64	z3*	✅	2s	4s	-50%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	30s	29s	+3%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	27s	31s	-13%
	LP64	z3*	✅	2s	2s	+0%
polyeta_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	1s	+0%
polyeta_unpack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
polyt0_pack	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
polyt0_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	8s	7s	+14%
polyt1_pack	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
polyt1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	5s	-20%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
polyvec_matrix_expand_serial	LP64	z3*	✅	2s	1s	+100%
polyvec_matrix_pointwise_montgomery_row	LP64	cadical	✅	48s	42s	+14%
	LP64	z3_no_bv_extract*	✅	4s	6s	-33%
polyvec_matrix_pointwise_montgomery_yvec	LP64	cadical	✅	770s	799s	-4%
	LP64	z3*	✅	90s	83s	+8%
polyveck_caddq	LP64	cadical	✅	219s	225s	-3%
	LP64	z3*	✅	2s	3s	-33%
polyveck_decompose_pack_w1	LP64	cadical	✅	175s	181s	-3%
	LP64	z3*	✅	15s	16s	-6%
polyveck_invntt_tomont	LP64	cadical	✅	191s	195s	-2%
	LP64	z3*	✅	3s	4s	-25%
polyveck_ntt	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
polyveck_reduce	LP64	cadical	✅	176s	215s	-18%
	LP64	z3*	✅	3s	2s	+50%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	18s	20s	-10%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_chknorm	LP64	cadical	✅	68s	73s	-7%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_ntt	LP64	cadical	✅	193s	162s	+19%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	2s	3s	-33%
polyvecl_pointwise_acc_montgomery_c	LP64	cadical	✅	4s	2s	+100%
	LP64	z3_smt_only*	✅	2s	3s	-33%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	1s	2s	-50%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	35s	31s	+13%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	33s	34s	-3%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
polyw1_pack_32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_pack_88	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
polyw1_unpack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	1s	2s	-50%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyw1_unpack_88	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
polyz_pack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyz_unpack	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	1s	+300%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_c	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	4s	-50%
polyz_unpack_native	LP64	bitwuzla	✅	27s	25s	+8%
	LP64	z3*	✅	3s	1s	+200%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	15s	17s	-12%
	LP64	z3*	✅	2s	2s	+0%
power2round	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
reduce32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
rej_eta	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	4s	3s	+33%
rej_eta_c	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	16s	15s	+7%
rej_eta_native	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	10s	11s	-9%
rej_uniform	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	9s	12s	-25%
rej_uniform_c	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	8s	10s	-20%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	4s	3s	+33%
rej_uniform_native	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3_smt_only	✅	8s	10s	-20%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	6s	2s	+200%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3_smt_only*	✅	9s	8s	+12%
shake128_absorb	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
shake128_finalize	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
shake128_init	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
shake128_release	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
shake128_squeeze	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
shake128x4_absorb_once	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
shake256	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake256_absorb	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	3s	-67%
shake256_finalize	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	4s	-75%
shake256_init	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
shake256_release	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
shake256_squeeze	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	2s	-50%
shake256x4_absorb_once	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	5s	3s	+67%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	1s	2s	-50%
sig_unpack_hints	LP64	bitwuzla	✅	1357s	1503s	-10%
	LP64	z3*	✅	18s	19s	-5%
sign_keypair	LP64	cadical	✅	435s	508s	-14%
	LP64	z3*	✅	4s	4s	+0%
sign_keypair_internal	LP64	cadical	✅	178s	184s	-3%
	LP64	z3_no_bv_extract*	✅	15s	16s	-6%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	25s	27s	-7%
sign_signature	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
sign_signature_extmu	LP64	cadical	✅	27s	30s	-10%
	LP64	z3*	✅	2s	3s	-33%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	12s	12s	+0%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	5s	-60%
sign_signature_pre_hash_shake256	LP64	cadical	✅	14s	18s	-22%
	LP64	z3*	✅	5s	4s	+25%
sign_verify	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	3s	+33%
sign_verify_extmu	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	195s	205s	-5%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	2s	3s	-33%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
sk_s1hat_get_poly	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
sk_s2hat_get_poly	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
sk_t0hat_get_poly	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	2s	+100%
sys_check_capability	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
unpack_pk_t1	LP64	bitwuzla	✅	12s	12s	+0%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk_t0hat	LP64	cadical	✅	3s	1s	+200%
	LP64	z3*	✅	3s	3s	+0%
use_hint	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
yvec_get_poly	LP64	bitwuzla	✅	8s	7s	+14%
	LP64	z3*	✅	2s	3s	-33%
yvec_init	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	2s	+50%

[oqs-bot]

CBMC Results (ML-DSA-44)

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1727s	1605s	+7.6%
caddq	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	65s	64s	+2%
decompose	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	2s	+0%
fqmul	LP64	bitwuzla*	✅	23s	22s	+5%
	LP64	z3_smt_only	✅	21s	19s	+11%
fqscale	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	1s	+200%
intt_native_aarch64	LP64	bitwuzla	✅	23s	20s	+15%
	LP64	z3*	✅	3s	2s	+50%
intt_native_rv32im_fastmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	3s	2s	+50%
intt_native_rv32im_slowmul	ILP32	z3*	✅	2s	2s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	2s	4s	-50%
intt_native_x86_64	LP64	bitwuzla	✅	18s	15s	+20%
	LP64	z3*	✅	2s	3s	-33%
keccak_absorb	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	7s	7s	+0%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	4s	6s	-33%
	LP64	cvc5_arrays_exp	✅	8s	8s	+0%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	4s	1s	+300%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	1s	+100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
keccak_finalize	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	1s	1s	+0%
keccak_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
keccak_squeeze	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	4s	3s	+33%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
keccakf1600_permute	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute_native	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	1s	+100%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	2s	+0%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	1s	+100%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	13s	12s	+8%
	LP64	z3*	✅	12s	13s	-8%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
make_hint	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	3s	-33%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	249s	200s	+25%
mld_check_pct	LP64	bitwuzla	✅	5s	8s	-38%
	LP64	z3*	✅	8s	3s	+167%
mld_compute_pack_z	LP64	cadical	✅	77s	65s	+18%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
mld_ct_abs_i32	ILP32	bitwuzla	✅	2s	1s	+100%
	ILP32	cvc5_arrays_exp	✅	3s	3s	+0%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	1s	+0%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	4s	-50%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	3s	4s	-25%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	48s	44s	+9%
mld_ct_sel_int32	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
mld_h	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	2s	+100%
mld_invntt_layer	LP64	bitwuzla*	✅	65s	64s	+2%
	LP64	z3_smt_only	✅	92s	86s	+7%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	4s	2s	+100%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	4s	3s	+33%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	5s	-40%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	11s	12s	-8%
	LP64	z3_no_bv_extract	✅	69s	61s	+13%
mld_ntt_layer	LP64	bitwuzla*	✅	25s	24s	+4%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
mld_polymat_expand_entry	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
mld_sample_pack_s1_s2	LP64	cadical	✅	28s	27s	+4%
	LP64	z3*	✅	1s	2s	-50%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	92s	89s	+3%
	LP64	z3*	✅	5s	4s	+25%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
mld_sign_finish	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
mld_sign_hook_resume	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_value_barrier_u32	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
ntt_native_aarch64	LP64	bitwuzla	✅	20s	17s	+18%
	LP64	z3*	✅	3s	3s	+0%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	6s	6s	+0%
	LP64	z3	✅	4s	2s	+100%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	8s	5s	+60%
	LP64	z3	✅	1s	3s	-67%
ntt_native_x86_64	LP64	bitwuzla	✅	20s	18s	+11%
	LP64	z3*	✅	3s	5s	-40%
nttunpack_native_x86_64	LP64	bitwuzla	✅	169s	177s	-5%
	LP64	z3*	✅	3s	2s	+50%
pack_sig_c	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	1s	+200%
pack_sig_h	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
pack_sig_z	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	2s	+100%
pointwise_acc_native_aarch64	LP64	cadical	✅	58s	57s	+2%
	LP64	z3_smt_only*	✅	6s	4s	+50%
pointwise_acc_native_x86_64	LP64	cadical	✅	70s	55s	+27%
	LP64	z3_smt_only*	✅	3s	4s	-25%
pointwise_native_aarch64	LP64	bitwuzla	✅	24s	20s	+20%
	LP64	z3*	✅	2s	2s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	10s	-10%
	LP64	z3	✅	3s	1s	+200%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	1s	2s	-50%
pointwise_native_x86_64	LP64	bitwuzla	✅	26s	22s	+18%
	LP64	z3*	✅	2s	3s	-33%
poly_add	LP64	cadical	✅	50s	51s	-2%
	LP64	z3*	✅	10s	9s	+11%
poly_caddq	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	1s	+100%
poly_caddq_c	LP64	bitwuzla	✅	20s	16s	+25%
	LP64	z3*	✅	2s	3s	-33%
poly_caddq_native	LP64	bitwuzla	✅	117s	106s	+10%
	LP64	z3*	✅	2s	3s	-33%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	35s	33s	+6%
	LP64	z3*	✅	1s	3s	-67%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	133s	115s	+16%
	LP64	z3*	✅	5s	3s	+67%
poly_challenge	LP64	bitwuzla	✅	27s	24s	+12%
	LP64	z3*	✅	13s	13s	+0%
poly_chknorm	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
poly_chknorm_c	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	6s	8s	-25%
poly_chknorm_native	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	1s	1s	+0%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	1s	+100%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	3s	+0%
poly_decompose	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	1s	3s	-67%
poly_decompose_32_native_aarch64	LP64	cadical	✅	1s	3s	-67%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_c	LP64	cvc5_mbqi_enum	✅	234s	171s	+37%
	LP64	z3*	✅	3s	3s	+0%
poly_decompose_native	LP64	cadical	✅	18s	15s	+20%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose_native_x86_64	LP64	cadical	✅	12s	10s	+20%
	LP64	z3*	✅	3s	1s	+200%
poly_invntt_tomont	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	2s	4s	-50%
poly_invntt_tomont_c	LP64	bitwuzla	✅	165s	154s	+7%
	LP64	z3_smt_only*	✅	3s	5s	-40%
poly_invntt_tomont_native	LP64	bitwuzla	✅	46s	45s	+2%
	LP64	z3*	✅	2s	1s	+100%
poly_ntt	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	2s	+50%
poly_ntt_c	LP64	bitwuzla	✅	55s	49s	+12%
	LP64	z3_smt_only*	✅	10s	10s	+0%
poly_ntt_native	LP64	bitwuzla	✅	28s	25s	+12%
	LP64	z3*	✅	2s	2s	+0%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	2s	-50%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	3s	3s	+0%
poly_pointwise_montgomery	LP64	bitwuzla	✅	9s	7s	+29%
	LP64	z3*	✅	3s	2s	+50%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	202s	182s	+11%
	LP64	z3*	✅	65s	62s	+5%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	54s	57s	-5%
	LP64	z3*	✅	3s	2s	+50%
poly_power2round	LP64	bitwuzla	✅	311s	241s	+29%
	LP64	z3*	✅	3s	2s	+50%
poly_reduce	LP64	bitwuzla	✅	8s	8s	+0%
	LP64	z3*	✅	4s	2s	+100%
poly_shiftl	LP64	bitwuzla	✅	13s	10s	+30%
	LP64	z3*	✅	2s	2s	+0%
poly_sub	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	1s	1s	+0%
poly_uniform	LP64	bitwuzla	✅	193s	175s	+10%
	LP64	z3*	✅	3s	3s	+0%
poly_uniform_4x	LP64	cadical	✅	61s	59s	+3%
	LP64	z3*	✅	7s	8s	-12%
poly_uniform_eta	LP64	bitwuzla	✅	74s	76s	-3%
	LP64	z3*	✅	2s	3s	-33%
poly_uniform_eta_4x	LP64	cadical	✅	65s	59s	+10%
	LP64	z3*	✅	11s	8s	+38%
poly_uniform_gamma1	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	11s	12s	-8%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	24s	23s	+4%
	LP64	z3*	✅	2s	1s	+100%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	12s	13s	-8%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	96s	92s	+4%
	LP64	z3*	✅	5s	4s	+25%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	32s	35s	-9%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	34s	34s	+0%
	LP64	z3*	✅	2s	4s	-50%
polyeta_pack	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	1s	+100%
polyeta_unpack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	8s	8s	+0%
polyt0_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	4s	-50%
polyt0_unpack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	9s	7s	+29%
polyt1_pack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
polyt1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	14s	10s	+40%
polyvec_matrix_expand_serial	LP64	z3*	✅	5s	5s	+0%
polyvec_matrix_pointwise_montgomery_row	LP64	cadical	✅	104s	98s	+6%
	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
polyvec_matrix_pointwise_montgomery_yvec	LP64	cadical	✅	239s	234s	+2%
	LP64	z3*	✅	6s	4s	+50%
polyveck_caddq	LP64	cadical	✅	104s	100s	+4%
	LP64	z3*	✅	2s	2s	+0%
polyveck_decompose_pack_w1	LP64	cadical	✅	125s	105s	+19%
	LP64	z3*	✅	3s	4s	-25%
polyveck_invntt_tomont	LP64	cadical	✅	141s	149s	-5%
	LP64	z3*	✅	2s	3s	-33%
polyveck_ntt	LP64	cadical	✅	117s	113s	+4%
	LP64	z3*	✅	4s	4s	+0%
polyveck_reduce	LP64	cadical	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	26s	26s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	17s	16s	+6%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_chknorm	LP64	cadical	✅	53s	50s	+6%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_ntt	LP64	cadical	✅	118s	133s	-11%
	LP64	z3*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	5s	6s	-17%
	LP64	z3_smt_only*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery_c	LP64	cadical	✅	92s	88s	+5%
	LP64	z3_smt_only*	✅	102s	94s	+9%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	165s	160s	+3%
	LP64	z3_smt_only*	✅	3s	2s	+50%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	40s	38s	+5%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	38s	42s	-10%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	33s	30s	+10%
	LP64	z3*	✅	1s	4s	-75%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	27s	24s	+12%
	LP64	z3*	✅	4s	2s	+100%
polyw1_pack	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
polyw1_pack_32	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
polyw1_pack_88	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
polyw1_unpack	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	2s	+50%
polyw1_unpack_32	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	3s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	5s	-40%
polyz_pack	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyz_unpack	LP64	bitwuzla	✅	7s	8s	-12%
	LP64	z3*	✅	4s	2s	+100%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
polyz_unpack_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	3s	+33%
polyz_unpack_native	LP64	bitwuzla	✅	26s	23s	+13%
	LP64	z3*	✅	4s	1s	+300%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	17s	14s	+21%
	LP64	z3*	✅	3s	1s	+200%
power2round	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	1s	2s	-50%
reduce32	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
rej_eta	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3_smt_only	✅	1s	3s	-67%
rej_eta_c	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	15s	13s	+15%
rej_eta_native	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	18s	15s	+20%
rej_uniform	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	9s	8s	+12%
rej_uniform_c	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	14s	12s	+17%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	4s	3s	+33%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3_smt_only*	✅	3s	1s	+200%
rej_uniform_native	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3_smt_only	✅	10s	8s	+25%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3_smt_only	✅	2s	4s	-50%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3_smt_only*	✅	9s	11s	-18%
shake128_absorb	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
shake128_finalize	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
shake128_init	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	4s	-50%
shake128_release	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	1s	+300%
shake128_squeeze	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
shake128x4_absorb_once	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	2s	2s	+0%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
shake256	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	2s	+0%
shake256_absorb	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
shake256_finalize	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
shake256_init	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
shake256_release	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%
shake256_squeeze	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	3s	1s	+200%
shake256x4_absorb_once	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	1s	3s	-67%
sig_unpack_hints	LP64	bitwuzla	✅	56s	50s	+12%
	LP64	z3*	✅	37s	33s	+12%
sign_keypair	LP64	cadical	✅	49s	56s	-12%
	LP64	z3*	✅	5s	5s	+0%
sign_keypair_internal	LP64	cadical	✅	150s	146s	+3%
	LP64	z3_no_bv_extract*	✅	7s	8s	-12%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	32s	34s	-6%
sign_signature	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
sign_signature_extmu	LP64	cadical	✅	24s	18s	+33%
	LP64	z3*	✅	3s	3s	+0%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	107s	95s	+13%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_pre_hash_shake256	LP64	cadical	✅	16s	14s	+14%
	LP64	z3*	✅	6s	7s	-14%
sign_verify	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	2s	+50%
sign_verify_extmu	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	324s	296s	+9%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	2s	+100%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	4s	2s	+100%
sk_s1hat_get_poly	LP64	bitwuzla	✅	30s	31s	-3%
	LP64	z3*	✅	2s	1s	+100%
sk_s2hat_get_poly	LP64	bitwuzla	✅	31s	29s	+7%
	LP64	z3*	✅	2s	2s	+0%
sk_t0hat_get_poly	LP64	bitwuzla	✅	32s	29s	+10%
	LP64	z3*	✅	2s	4s	-50%
sys_check_capability	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
unpack_pk_t1	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk	LP64	cadical	✅	32s	37s	-14%
	LP64	z3*	✅	2s	3s	-33%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	258s	248s	+4%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	255s	249s	+2%
	LP64	z3*	✅	2s	5s	-60%
unpack_sk_t0hat	LP64	cadical	✅	40s	36s	+11%
	LP64	z3*	✅	2s	1s	+100%
use_hint	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	3s	-67%
yvec_get_poly	LP64	bitwuzla	✅	33s	34s	-3%
	LP64	z3*	✅	2s	1s	+100%
yvec_init	LP64	bitwuzla	✅	39s	41s	-5%
	LP64	z3*	✅	1s	3s	-67%

[oqs-bot]

CBMC Results (ML-DSA-65)

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	2143s	2519s	-14.9%
caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	128s	156s	-18%
decompose	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	3s	1s	+200%
fqmul	LP64	bitwuzla*	✅	23s	30s	-23%
	LP64	z3_smt_only	✅	18s	22s	-18%
fqscale	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
intt_native_aarch64	LP64	bitwuzla	✅	23s	28s	-18%
	LP64	z3*	✅	1s	3s	-67%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	4s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	3s	3s	+0%
intt_native_rv32im_slowmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	2s	2s	+0%
intt_native_x86_64	LP64	bitwuzla	✅	18s	20s	-10%
	LP64	z3*	✅	1s	2s	-50%
keccak_absorb	LP64	cvc5_arrays_exp	✅	4s	4s	+0%
	LP64	z3*	✅	7s	9s	-22%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	5s	6s	-17%
	LP64	cvc5_arrays_exp	✅	7s	11s	-36%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	2s	3s	-33%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	1s	+100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3_smt_only	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	3s	1s	+200%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
keccak_finalize	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
keccak_init	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
keccak_squeeze	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	1s	+100%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	5s	3s	+67%
	LP64	z3	✅	4s	2s	+100%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
keccakf1600_permute_native	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	1s	+200%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	2s	+50%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	1s	+100%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	16s	11s	+45%
	LP64	z3*	✅	12s	12s	+0%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
make_hint	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	5s	1s	+400%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	270s	254s	+6%
mld_check_pct	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	6s	10s	-40%
mld_compute_pack_z	LP64	cadical	✅	70s	76s	-8%
	LP64	z3_no_bv_extract*	✅	3s	6s	-50%
mld_ct_abs_i32	ILP32	bitwuzla	✅	2s	2s	+0%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	4s	-50%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	5s	1s	+400%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_smt_only	✅	1s	1s	+0%
mld_ct_memcmp	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	45s	61s	-26%
mld_ct_sel_int32	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	3s	+0%
mld_h	LP64	bitwuzla	✅	4s	6s	-33%
	LP64	z3*	✅	3s	3s	+0%
mld_invntt_layer	LP64	bitwuzla*	✅	63s	88s	-28%
	LP64	z3_smt_only	✅	87s	111s	-22%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	6s	2s	+200%
	LP64	z3*	✅	4s	6s	-33%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	13s	17s	-24%
	LP64	z3_no_bv_extract	✅	65s	89s	-27%
mld_ntt_layer	LP64	bitwuzla*	✅	24s	34s	-29%
	LP64	z3_no_bv_extract	✅	5s	3s	+67%
mld_polymat_expand_entry	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	1s	+300%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
mld_sample_pack_s1_s2	LP64	cadical	✅	45s	50s	-10%
	LP64	z3*	✅	4s	6s	-33%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	229s	252s	-9%
	LP64	z3*	✅	6s	3s	+100%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
mld_sign_finish	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_sign_hook_resume	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	3s	+33%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
mld_value_barrier_u32	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	5s	-80%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
ntt_native_aarch64	LP64	bitwuzla	✅	19s	24s	-21%
	LP64	z3*	✅	2s	4s	-50%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	7s	8s	-12%
	LP64	z3	✅	2s	2s	+0%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	6s	7s	-14%
	LP64	z3	✅	4s	2s	+100%
ntt_native_x86_64	LP64	bitwuzla	✅	20s	22s	-9%
	LP64	z3*	✅	2s	2s	+0%
nttunpack_native_x86_64	LP64	bitwuzla	✅	186s	252s	-26%
	LP64	z3*	✅	2s	5s	-60%
pack_sig_c	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
pack_sig_h	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3_no_bv_extract*	✅	3s	3s	+0%
pack_sig_z	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
pointwise_acc_native_aarch64	LP64	cadical	✅	76s	84s	-10%
	LP64	z3_smt_only*	✅	5s	3s	+67%
pointwise_acc_native_x86_64	LP64	cadical	✅	89s	88s	+1%
	LP64	z3_smt_only*	✅	4s	4s	+0%
pointwise_native_aarch64	LP64	bitwuzla	✅	21s	27s	-22%
	LP64	z3*	✅	3s	3s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	2s	2s	+0%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	4s	1s	+300%
	LP64	cvc5_mbqi_enum	✅	3s	9s	-67%
	LP64	z3	✅	5s	2s	+150%
pointwise_native_x86_64	LP64	bitwuzla	✅	22s	25s	-12%
	LP64	z3*	✅	3s	2s	+50%
poly_add	LP64	cadical	✅	52s	56s	-7%
	LP64	z3*	✅	12s	15s	-20%
poly_caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_c	LP64	bitwuzla	✅	17s	24s	-29%
	LP64	z3*	✅	4s	3s	+33%
poly_caddq_native	LP64	bitwuzla	✅	113s	150s	-25%
	LP64	z3*	✅	4s	2s	+100%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	33s	39s	-15%
	LP64	z3*	✅	1s	1s	+0%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	122s	145s	-16%
	LP64	z3*	✅	2s	4s	-50%
poly_challenge	LP64	bitwuzla	✅	22s	29s	-24%
	LP64	z3*	✅	11s	13s	-15%
poly_chknorm	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_c	LP64	bitwuzla	✅	8s	9s	-11%
	LP64	z3*	✅	10s	8s	+25%
poly_chknorm_native	LP64	bitwuzla	✅	6s	7s	-14%
	LP64	z3*	✅	2s	3s	-33%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	2s	+100%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
poly_decompose	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	4s	-50%
poly_decompose_32_native_aarch64	LP64	cadical	✅	10s	8s	+25%
	LP64	z3*	✅	1s	3s	-67%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	5s	-60%
poly_decompose_c	LP64	cvc5_mbqi_enum	✅	228s	254s	-10%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_native	LP64	cadical	✅	13s	14s	-7%
	LP64	z3*	✅	3s	2s	+50%
poly_decompose_native_x86_64	LP64	cadical	✅	10s	10s	+0%
	LP64	z3*	✅	5s	4s	+25%
poly_invntt_tomont	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	2s	4s	-50%
poly_invntt_tomont_c	LP64	bitwuzla	✅	151s	213s	-29%
	LP64	z3_smt_only*	✅	5s	5s	+0%
poly_invntt_tomont_native	LP64	bitwuzla	✅	49s	58s	-16%
	LP64	z3*	✅	2s	4s	-50%
poly_ntt	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	2s	2s	+0%
poly_ntt_c	LP64	bitwuzla	✅	46s	68s	-32%
	LP64	z3_smt_only*	✅	9s	11s	-18%
poly_ntt_native	LP64	bitwuzla	✅	28s	35s	-20%
	LP64	z3*	✅	3s	3s	+0%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	4s	3s	+33%
poly_pointwise_montgomery	LP64	bitwuzla	✅	11s	13s	-15%
	LP64	z3*	✅	2s	3s	-33%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	188s	231s	-19%
	LP64	z3*	✅	65s	83s	-22%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	55s	59s	-7%
	LP64	z3*	✅	3s	4s	-25%
poly_power2round	LP64	bitwuzla	✅	276s	366s	-25%
	LP64	z3*	✅	3s	3s	+0%
poly_reduce	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	4s	1s	+300%
poly_shiftl	LP64	bitwuzla	✅	12s	13s	-8%
	LP64	z3*	✅	2s	1s	+100%
poly_sub	LP64	bitwuzla	✅	13s	17s	-24%
	LP64	z3*	✅	4s	4s	+0%
poly_uniform	LP64	bitwuzla	✅	157s	238s	-34%
	LP64	z3*	✅	1s	5s	-80%
poly_uniform_4x	LP64	cadical	✅	72s	67s	+7%
	LP64	z3*	✅	8s	9s	-11%
poly_uniform_eta	LP64	bitwuzla	✅	51s	65s	-22%
	LP64	z3*	✅	2s	3s	-33%
poly_uniform_eta_4x	LP64	cadical	✅	57s	58s	-2%
	LP64	z3*	✅	7s	11s	-36%
poly_uniform_gamma1	LP64	cadical	✅	3s	6s	-50%
	LP64	z3*	✅	3s	4s	-25%
poly_uniform_gamma1_4x	LP64	cadical	✅	11s	14s	-21%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	23s	26s	-12%
	LP64	z3*	✅	3s	1s	+200%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	14s	16s	-12%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	85s	77s	+10%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	31s	39s	-21%
	LP64	z3*	✅	1s	2s	-50%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	28s	37s	-24%
	LP64	z3*	✅	3s	3s	+0%
polyeta_pack	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	5s	2s	+150%
polyeta_unpack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	6s	4s	+50%
polyt0_pack	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	4s	2s	+100%
polyt0_unpack	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	8s	9s	-11%
polyt1_pack	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
polyt1_unpack	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	5s	2s	+150%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	59s	72s	-18%
polyvec_matrix_expand_serial	LP64	z3*	✅	11s	12s	-8%
polyvec_matrix_pointwise_montgomery_row	LP64	cadical	✅	246s	262s	-6%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
polyvec_matrix_pointwise_montgomery_yvec	LP64	cadical	✅	414s	443s	-7%
	LP64	z3*	✅	5s	5s	+0%
polyveck_caddq	LP64	cadical	✅	213s	297s	-28%
	LP64	z3*	✅	4s	4s	+0%
polyveck_decompose_pack_w1	LP64	cadical	✅	174s	189s	-8%
	LP64	z3*	✅	7s	7s	+0%
polyveck_invntt_tomont	LP64	cadical	✅	188s	210s	-10%
	LP64	z3*	✅	4s	4s	+0%
polyveck_ntt	LP64	cadical	✅	195s	211s	-8%
	LP64	z3*	✅	1s	7s	-86%
polyveck_reduce	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	2s	5s	-60%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	45s	46s	-2%
	LP64	z3*	✅	3s	3s	+0%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	22s	18s	+22%
	LP64	z3*	✅	2s	4s	-50%
polyvecl_chknorm	LP64	cadical	✅	69s	80s	-14%
	LP64	z3*	✅	4s	4s	+0%
polyvecl_ntt	LP64	cadical	✅	162s	178s	-9%
	LP64	z3*	✅	3s	3s	+0%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3_smt_only*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery_c	LP64	cadical	✅	114s	127s	-10%
	LP64	z3_smt_only*	✅	214s	274s	-22%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	118s	119s	-1%
	LP64	z3_smt_only*	✅	3s	4s	-25%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	35s	41s	-15%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	33s	38s	-13%
	LP64	z3*	✅	2s	1s	+100%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	36s	38s	-5%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	33s	34s	-3%
	LP64	z3*	✅	3s	2s	+50%
polyw1_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
polyw1_pack_32	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	2s	-50%
polyw1_pack_88	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
polyw1_unpack	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack_32	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	5s	2s	+150%
polyz_pack	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	1s	+0%
polyz_unpack	LP64	bitwuzla	✅	7s	8s	-12%
	LP64	z3*	✅	3s	2s	+50%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_c	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	4s	+0%
polyz_unpack_native	LP64	bitwuzla	✅	27s	33s	-18%
	LP64	z3*	✅	2s	1s	+100%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	16s	24s	-33%
	LP64	z3*	✅	3s	3s	+0%
power2round	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
reduce32	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	3s	+33%
rej_eta	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	5s	-40%
rej_eta_c	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	13s	21s	-38%
rej_eta_native	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	9s	13s	-31%
rej_uniform	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	9s	11s	-18%
rej_uniform_c	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	13s	18s	-28%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	3s	3s	+0%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3_smt_only*	✅	4s	2s	+100%
rej_uniform_native	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3_smt_only	✅	10s	12s	-17%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	5s	6s	-17%
	LP64	z3_smt_only*	✅	8s	12s	-33%
shake128_absorb	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	1s	+200%
shake128_finalize	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
shake128_init	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
shake128_release	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
shake128_squeeze	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
shake128x4_absorb_once	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
shake256	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
shake256_absorb	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
shake256_finalize	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
shake256_init	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	3s	4s	-25%
shake256_release	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	3s	-67%
shake256_squeeze	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	1s	+100%
shake256x4_absorb_once	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	1s	+300%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
sig_unpack_hints	LP64	bitwuzla	✅	1319s	1791s	-26%
	LP64	z3*	✅	20s	25s	-20%
sign_keypair	LP64	cadical	✅	452s	571s	-21%
	LP64	z3*	✅	4s	5s	-20%
sign_keypair_internal	LP64	cadical	✅	203s	196s	+4%
	LP64	z3_no_bv_extract*	✅	18s	20s	-10%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	37s	42s	-12%
sign_signature	LP64	bitwuzla	✅	6s	2s	+200%
	LP64	z3*	✅	2s	4s	-50%
sign_signature_extmu	LP64	cadical	✅	27s	44s	-39%
	LP64	z3*	✅	3s	3s	+0%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	162s	206s	-21%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	4s	4s	+0%
sign_signature_pre_hash_shake256	LP64	cadical	✅	18s	18s	+0%
	LP64	z3*	✅	6s	5s	+20%
sign_verify	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	4s	-25%
sign_verify_extmu	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	429s	548s	-22%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	3s	+0%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	2s	+0%
sk_s1hat_get_poly	LP64	bitwuzla	✅	37s	47s	-21%
	LP64	z3*	✅	1s	4s	-75%
sk_s2hat_get_poly	LP64	bitwuzla	✅	29s	34s	-15%
	LP64	z3*	✅	2s	2s	+0%
sk_t0hat_get_poly	LP64	bitwuzla	✅	29s	34s	-15%
	LP64	z3*	✅	4s	2s	+100%
sys_check_capability	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
unpack_pk_t1	LP64	bitwuzla	✅	12s	15s	-20%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk	LP64	cadical	✅	48s	54s	-11%
	LP64	z3*	✅	1s	2s	-50%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	84s	97s	-13%
	LP64	z3*	✅	2s	3s	-33%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	157s	172s	-9%
	LP64	z3*	✅	1s	5s	-80%
unpack_sk_t0hat	LP64	cadical	✅	83s	92s	-10%
	LP64	z3*	✅	1s	1s	+0%
use_hint	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
yvec_get_poly	LP64	bitwuzla	✅	32s	38s	-16%
	LP64	z3*	✅	4s	2s	+100%
yvec_init	LP64	bitwuzla	✅	9s	10s	-10%
	LP64	z3*	✅	2s	2s	+0%

[oqs-bot]

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
sign_keypair	LP64	cadical	⚠️	792s	515s	+54%

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	4154s	3521s	+18.0%
caddq	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	196s	180s	+9%
decompose	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	3s	4s	-25%
fqmul	LP64	bitwuzla*	✅	24s	24s	+0%
	LP64	z3_smt_only	✅	21s	21s	+0%
fqscale	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
intt_native_aarch64	LP64	bitwuzla	✅	25s	24s	+4%
	LP64	z3*	✅	3s	4s	-25%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	1s	2s	-50%
intt_native_rv32im_slowmul	ILP32	z3*	✅	4s	2s	+100%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	1s	2s	-50%
intt_native_x86_64	LP64	bitwuzla	✅	21s	16s	+31%
	LP64	z3*	✅	1s	4s	-75%
keccak_absorb	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	7s	5s	+40%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	4s	6s	-33%
	LP64	cvc5_arrays_exp	✅	9s	9s	+0%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	1s	+100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	2s	3s	-33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
keccak_finalize	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
keccak_init	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
keccak_squeeze	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	1s	1s	+0%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	1s	+0%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
keccakf1600_permute	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute_native	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	2s	3s	-33%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	4s	-50%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	4s	-25%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	14s	15s	-7%
	LP64	z3*	✅	12s	14s	-14%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
keccakf1600x4_xor_bytes_native	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_no_bv_extract	✅	2s	1s	+100%
make_hint	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	310s	263s	+18%
mld_check_pct	LP64	bitwuzla	✅	5s	7s	-29%
	LP64	z3*	✅	5s	7s	-29%
mld_compute_pack_z	LP64	cadical	✅	87s	84s	+4%
	LP64	z3_no_bv_extract*	✅	4s	7s	-43%
mld_ct_abs_i32	ILP32	bitwuzla	✅	3s	1s	+200%
	ILP32	cvc5_arrays_exp	✅	2s	4s	-50%
	ILP32	z3	✅	1s	4s	-75%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	1s	+100%
mld_ct_memcmp	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_no_bv_extract	✅	49s	47s	+4%
mld_ct_sel_int32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
mld_h	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	3s	-33%
mld_invntt_layer	LP64	bitwuzla*	✅	76s	64s	+19%
	LP64	z3_smt_only	✅	104s	85s	+22%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	4s	5s	-20%
	LP64	z3*	✅	5s	6s	-17%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	16s	14s	+14%
	LP64	z3_no_bv_extract	✅	69s	57s	+21%
mld_ntt_layer	LP64	bitwuzla*	✅	26s	24s	+8%
	LP64	z3_no_bv_extract	✅	3s	3s	+0%
mld_polymat_expand_entry	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	3s	3s	+0%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
mld_sample_pack_s1_s2	LP64	cadical	✅	80s	71s	+13%
	LP64	z3*	✅	5s	5s	+0%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	562s	541s	+4%
	LP64	z3*	✅	5s	4s	+25%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
mld_sign_finish	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	4s	-25%
mld_sign_hook_resume	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	4s	-25%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	1s	3s	-67%
mld_value_barrier_u32	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	3s	-33%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	3s	4s	-25%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	3s	4s	-25%
	LP64	z3*	✅	3s	1s	+200%
ntt_native_aarch64	LP64	bitwuzla	✅	22s	21s	+5%
	LP64	z3*	✅	2s	4s	-50%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	4s	4s	+0%
	LP64	cvc5_mbqi_enum	✅	7s	6s	+17%
	LP64	z3	✅	4s	2s	+100%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	1s	2s	-50%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	1s	2s	-50%
ntt_native_x86_64	LP64	bitwuzla	✅	18s	19s	-5%
	LP64	z3*	✅	1s	5s	-80%
nttunpack_native_x86_64	LP64	bitwuzla	✅	207s	173s	+20%
	LP64	z3*	✅	2s	3s	-33%
pack_sig_c	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
pack_sig_h	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
pack_sig_z	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	1s	1s	+0%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	4s	5s	-20%
pointwise_acc_native_aarch64	LP64	cadical	✅	95s	87s	+9%
	LP64	z3_smt_only*	✅	6s	6s	+0%
pointwise_acc_native_x86_64	LP64	cadical	✅	94s	87s	+8%
	LP64	z3_smt_only*	✅	4s	5s	-20%
pointwise_native_aarch64	LP64	bitwuzla	✅	24s	20s	+20%
	LP64	z3*	✅	5s	3s	+67%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	9s	7s	+29%
	LP64	z3	✅	1s	1s	+0%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	5s	3s	+67%
	LP64	cvc5_mbqi_enum	✅	11s	8s	+38%
	LP64	z3	✅	1s	3s	-67%
pointwise_native_x86_64	LP64	bitwuzla	✅	25s	22s	+14%
	LP64	z3*	✅	3s	1s	+200%
poly_add	LP64	cadical	✅	50s	46s	+9%
	LP64	z3*	✅	10s	11s	-9%
poly_caddq	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
poly_caddq_c	LP64	bitwuzla	✅	21s	18s	+17%
	LP64	z3*	✅	4s	4s	+0%
poly_caddq_native	LP64	bitwuzla	✅	127s	106s	+20%
	LP64	z3*	✅	3s	4s	-25%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	34s	34s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	134s	110s	+22%
	LP64	z3*	✅	1s	3s	-67%
poly_challenge	LP64	bitwuzla	✅	38s	33s	+15%
	LP64	z3*	✅	12s	12s	+0%
poly_chknorm	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_c	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	9s	8s	+12%
poly_chknorm_native	LP64	bitwuzla	✅	7s	7s	+0%
	LP64	z3*	✅	3s	2s	+50%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	3s	-67%
poly_decompose	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	4s	2s	+100%
poly_decompose_32_native_aarch64	LP64	cadical	✅	8s	9s	-11%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
poly_decompose_c	LP64	cvc5_mbqi_enum	✅	225s	227s	-1%
	LP64	z3*	✅	4s	4s	+0%
poly_decompose_native	LP64	cadical	✅	13s	13s	+0%
	LP64	z3*	✅	2s	6s	-67%
poly_decompose_native_x86_64	LP64	cadical	✅	9s	10s	-10%
	LP64	z3*	✅	2s	2s	+0%
poly_invntt_tomont	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	1s	4s	-75%
poly_invntt_tomont_c	LP64	bitwuzla	✅	182s	151s	+21%
	LP64	z3_smt_only*	✅	4s	5s	-20%
poly_invntt_tomont_native	LP64	bitwuzla	✅	53s	41s	+29%
	LP64	z3*	✅	2s	2s	+0%
poly_ntt	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
poly_ntt_c	LP64	bitwuzla	✅	53s	49s	+8%
	LP64	z3_smt_only*	✅	10s	10s	+0%
poly_ntt_native	LP64	bitwuzla	✅	31s	23s	+35%
	LP64	z3*	✅	4s	1s	+300%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	3s	-33%
poly_pointwise_montgomery	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	4s	3s	+33%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	197s	186s	+6%
	LP64	z3*	✅	68s	61s	+11%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	55s	52s	+6%
	LP64	z3*	✅	4s	2s	+100%
poly_power2round	LP64	bitwuzla	✅	355s	263s	+35%
	LP64	z3*	✅	3s	5s	-40%
poly_reduce	LP64	bitwuzla	✅	8s	6s	+33%
	LP64	z3*	✅	3s	2s	+50%
poly_shiftl	LP64	bitwuzla	✅	11s	15s	-27%
	LP64	z3*	✅	2s	2s	+0%
poly_sub	LP64	bitwuzla	✅	16s	14s	+14%
	LP64	z3*	✅	3s	2s	+50%
poly_uniform	LP64	bitwuzla	✅	195s	177s	+10%
	LP64	z3*	✅	3s	3s	+0%
poly_uniform_4x	LP64	cadical	✅	66s	59s	+12%
	LP64	z3*	✅	7s	9s	-22%
poly_uniform_eta	LP64	bitwuzla	✅	92s	76s	+21%
	LP64	z3*	✅	2s	3s	-33%
poly_uniform_eta_4x	LP64	cadical	✅	64s	62s	+3%
	LP64	z3*	✅	11s	8s	+38%
poly_uniform_gamma1	LP64	cadical	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	10s	11s	-9%
	LP64	z3*	✅	3s	6s	-50%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	24s	22s	+9%
	LP64	z3*	✅	1s	2s	-50%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	14s	11s	+27%
	LP64	z3*	✅	2s	4s	-50%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	87s	90s	-3%
	LP64	z3*	✅	2s	1s	+100%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	30s	29s	+3%
	LP64	z3*	✅	2s	2s	+0%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	34s	28s	+21%
	LP64	z3*	✅	2s	2s	+0%
polyeta_pack	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	1s	3s	-67%
polyeta_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	8s	8s	+0%
polyt0_pack	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	2s	3s	-33%
polyt0_unpack	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	9s	9s	+0%
polyt1_pack	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
polyt1_unpack	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	5s	-20%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	102s	81s	+26%
polyvec_matrix_expand_serial	LP64	z3*	✅	27s	28s	-4%
polyvec_matrix_pointwise_montgomery_row	LP64	cadical	✅	601s	582s	+3%
	LP64	z3_no_bv_extract*	✅	1s	2s	-50%
polyvec_matrix_pointwise_montgomery_yvec	LP64	cadical	✅	795s	756s	+5%
	LP64	z3*	✅	6s	6s	+0%
polyveck_caddq	LP64	cadical	✅	1259s	1195s	+5%
	LP64	z3*	✅	2s	4s	-50%
polyveck_decompose_pack_w1	LP64	cadical	✅	215s	199s	+8%
	LP64	z3*	✅	3s	4s	-25%
polyveck_invntt_tomont	LP64	cadical	✅	339s	305s	+11%
	LP64	z3*	✅	2s	2s	+0%
polyveck_ntt	LP64	cadical	✅	1099s	1100s	-0%
	LP64	z3*	✅	2s	2s	+0%
polyveck_reduce	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	56s	55s	+2%
	LP64	z3*	✅	1s	2s	-50%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	17s	18s	-6%
	LP64	z3*	✅	3s	3s	+0%
polyvecl_chknorm	LP64	cadical	✅	145s	135s	+7%
	LP64	z3*	✅	6s	6s	+0%
polyvecl_ntt	LP64	cadical	✅	203s	182s	+12%
	LP64	z3*	✅	5s	3s	+67%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	13s	15s	-13%
	LP64	z3_smt_only*	✅	4s	2s	+100%
polyvecl_pointwise_acc_montgomery_c	LP64	cadical	✅	161s	155s	+4%
	LP64	z3_smt_only*	✅	1356s	1021s	+33%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	182s	172s	+6%
	LP64	z3_smt_only*	✅	3s	3s	+0%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	83s	78s	+6%
	LP64	z3*	✅	5s	3s	+67%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	49s	46s	+7%
	LP64	z3*	✅	2s	3s	-33%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	49s	44s	+11%
	LP64	z3*	✅	2s	1s	+100%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	48s	46s	+4%
	LP64	z3*	✅	2s	4s	-50%
polyw1_pack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyw1_pack_32	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
polyw1_pack_88	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	1s	+200%
polyw1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack_88	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
polyz_pack	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	4s	-50%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_c	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	12s	9s	+33%
polyz_unpack_native	LP64	bitwuzla	✅	29s	22s	+32%
	LP64	z3*	✅	2s	2s	+0%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	17s	16s	+6%
	LP64	z3*	✅	3s	4s	-25%
power2round	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	4s	3s	+33%
reduce32	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	1s	3s	-67%
rej_eta	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3_smt_only	✅	5s	3s	+67%
rej_eta_c	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	15s	16s	-6%
rej_eta_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	20s	15s	+33%
rej_uniform	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	10s	9s	+11%
rej_uniform_c	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	13s	13s	+0%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	2s	3s	-33%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3_smt_only*	✅	3s	2s	+50%
rej_uniform_native	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3_smt_only	✅	11s	11s	+0%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3_smt_only	✅	2s	3s	-33%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3_smt_only*	✅	9s	10s	-10%
shake128_absorb	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	3s	+33%
shake128_finalize	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
shake128_init	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
shake128_release	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
shake128_squeeze	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
shake128x4_absorb_once	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	3s	2s	+50%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	1s	+200%
shake256	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
shake256_absorb	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
shake256_finalize	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
shake256_init	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
shake256_release	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
shake256_squeeze	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	3s	-33%
shake256x4_absorb_once	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	3s	1s	+200%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
sig_unpack_hints	LP64	bitwuzla	✅	29s	22s	+32%
	LP64	z3*	✅	14s	14s	+0%
sign_keypair	LP64	cadical	⚠️	792s	515s	+54%
	LP64	z3*	✅	5s	4s	+25%
sign_keypair_internal	LP64	cadical	✅	232s	214s	+8%
	LP64	z3_no_bv_extract*	✅	27s	25s	+8%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	31s	28s	+11%
sign_signature	LP64	bitwuzla	✅	6s	4s	+50%
	LP64	z3*	✅	4s	3s	+33%
sign_signature_extmu	LP64	cadical	✅	61s	50s	+22%
	LP64	z3*	✅	4s	4s	+0%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	334s	242s	+38%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	4s	2s	+100%
sign_signature_pre_hash_shake256	LP64	cadical	✅	28s	22s	+27%
	LP64	z3*	✅	4s	5s	-20%
sign_verify	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	3s	+0%
sign_verify_extmu	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	3s	+0%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	916s	798s	+15%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	5s	-20%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	6s	-50%
sk_s1hat_get_poly	LP64	bitwuzla	✅	34s	31s	+10%
	LP64	z3*	✅	2s	2s	+0%
sk_s2hat_get_poly	LP64	bitwuzla	✅	40s	32s	+25%
	LP64	z3*	✅	2s	4s	-50%
sk_t0hat_get_poly	LP64	bitwuzla	✅	35s	33s	+6%
	LP64	z3*	✅	1s	2s	-50%
sys_check_capability	LP64	cvc5_arrays_exp	✅	4s	6s	-33%
	LP64	z3*	✅	2s	3s	-33%
unpack_pk_t1	LP64	bitwuzla	✅	12s	11s	+9%
	LP64	z3*	✅	4s	2s	+100%
unpack_sk	LP64	cadical	✅	71s	64s	+11%
	LP64	z3*	✅	1s	4s	-75%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	91s	87s	+5%
	LP64	z3*	✅	3s	2s	+50%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	322s	299s	+8%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk_t0hat	LP64	cadical	✅	117s	115s	+2%
	LP64	z3*	✅	4s	4s	+0%
use_hint	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
yvec_get_poly	LP64	bitwuzla	✅	38s	35s	+9%
	LP64	z3*	✅	2s	2s	+0%
yvec_init	LP64	bitwuzla	✅	17s	16s	+6%
	LP64	z3*	✅	2s	2s	+0%

[oqs-bot]

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

* default.

Full Results (433 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
**TOTAL**	-	-	✅	1551s	1389s	+11.7%
caddq	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
compute_pack_t0_t1	LP64	z3_no_bv_extract*	✅	32s	27s	+19%
decompose	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	1s	+100%
fqmul	LP64	bitwuzla*	✅	27s	25s	+8%
	LP64	z3_smt_only	✅	20s	18s	+11%
fqscale	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	1s	+0%
intt_native_aarch64	LP64	bitwuzla	✅	22s	23s	-4%
	LP64	z3*	✅	4s	3s	+33%
intt_native_rv32im_fastmul	ILP32	z3*	✅	2s	3s	-33%
	LP64	cvc5_mbqi_enum	✅	9s	8s	+12%
	LP64	z3	✅	3s	1s	+200%
intt_native_rv32im_slowmul	ILP32	z3*	✅	3s	2s	+50%
	LP64	cvc5_mbqi_enum	✅	8s	9s	-11%
	LP64	z3	✅	3s	2s	+50%
intt_native_x86_64	LP64	bitwuzla	✅	23s	19s	+21%
	LP64	z3*	✅	2s	4s	-50%
keccak_absorb	LP64	cvc5_arrays_exp	✅	3s	3s	+0%
	LP64	z3*	✅	7s	6s	+17%
keccak_absorb_once_x4	LP64	bitwuzla*	✅	6s	4s	+50%
	LP64	cvc5_arrays_exp	✅	14s	10s	+40%
keccak_f1600_x1_native_aarch64	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_no_bv_extract	✅	1s	1s	+0%
keccak_f1600_x1_native_aarch64_v84a	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
keccak_f1600_x4_native_aarch64_v84a	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	2s	-50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3_smt_only	✅	2s	2s	+0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	1s	2s	-50%
keccak_f1600_x4_native_avx2	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
keccak_finalize	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	3s	1s	+200%
keccak_init	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	2s	+100%
keccak_squeeze	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
keccak_squeezeblocks_x4	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	3s	2s	+50%
keccakf1600_extract_bytes (big endian)	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3*	✅	2s	2s	+0%
keccakf1600_permute	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
keccakf1600_permute_native	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
keccakf1600_xor_bytes	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
keccakf1600_xor_bytes (big endian)	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3_smt_only	✅	3s	2s	+50%
keccakf1600x4_extract_bytes	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	2s	+0%
keccakf1600x4_extract_bytes_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	1s	+100%
keccakf1600x4_permute	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	1s	1s	+0%
keccakf1600x4_permute_native	LP64	cvc5_arrays_exp	✅	14s	11s	+27%
	LP64	z3*	✅	12s	12s	+0%
keccakf1600x4_xor_bytes	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
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*	✅	3s	2s	+50%
mld_attempt_signature_generation	LP64	z3_no_bv_extract*	✅	170s	141s	+21%
mld_check_pct	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	6s	5s	+20%
mld_compute_pack_z	LP64	cadical	✅	40s	38s	+5%
	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
mld_ct_abs_i32	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	3s	3s	+0%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_cmask_neg_i32	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
mld_ct_cmask_nonzero_u32	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
mld_ct_cmask_nonzero_u8	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
mld_ct_get_optblocker_i64	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	1s	+0%
mld_ct_get_optblocker_u32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	1s	+100%
mld_ct_get_optblocker_u8	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	✅	1s	2s	-50%
mld_ct_memcmp	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3_no_bv_extract	✅	46s	53s	-13%
mld_ct_sel_int32	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_h	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
mld_invntt_layer	LP64	bitwuzla*	✅	89s	76s	+17%
	LP64	z3_smt_only	✅	80s	82s	-2%
mld_keccakf1600_extract_bytes	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
mld_keccakf1600_permute_c	LP64	cvc5_arrays_exp	✅	5s	4s	+25%
	LP64	z3*	✅	6s	3s	+100%
mld_keccakf1600x4_extract_bytes_c	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	1s	3s	-67%
mld_keccakf1600x4_xor_bytes_c	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
mld_ntt_butterfly_block	LP64	bitwuzla*	✅	15s	14s	+7%
	LP64	z3_no_bv_extract	✅	244s	206s	+18%
mld_ntt_layer	LP64	bitwuzla*	✅	25s	29s	-14%
	LP64	z3_no_bv_extract	✅	2s	2s	+0%
mld_polymat_expand_entry	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
mld_prepare_domain_separation_prefix	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	4s	2s	+100%
mld_sample_pack_s1_s2	LP64	cadical	✅	33s	29s	+14%
	LP64	z3*	✅	2s	3s	-33%
mld_sample_pack_s1_s2_serial	LP64	cvc5_mbqi_enum	✅	93s	90s	+3%
	LP64	z3*	✅	2s	2s	+0%
mld_sign_attempt	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	4s	1s	+300%
mld_sign_finish	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	1s	+200%
mld_sign_hook_resume	LP64	bitwuzla	✅	5s	2s	+150%
	LP64	z3*	✅	2s	2s	+0%
mld_value_barrier_i64	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
mld_value_barrier_u32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
mld_value_barrier_u8	LP64	cvc5_arrays_exp	✅	3s	2s	+50%
	LP64	z3*	✅	3s	3s	+0%
montgomery_reduce	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
ntt_native_aarch64	LP64	bitwuzla	✅	21s	22s	-5%
	LP64	z3*	✅	1s	2s	-50%
ntt_native_rv32im_fastmul	ILP32	z3*	✅	1s	3s	-67%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	1s	3s	-67%
ntt_native_rv32im_slowmul	ILP32	z3*	✅	3s	4s	-25%
	LP64	cvc5_mbqi_enum	✅	7s	9s	-22%
	LP64	z3	✅	2s	2s	+0%
ntt_native_x86_64	LP64	bitwuzla	✅	18s	21s	-14%
	LP64	z3*	✅	4s	2s	+100%
nttunpack_native_x86_64	LP64	bitwuzla	✅	217s	175s	+24%
	LP64	z3*	✅	4s	2s	+100%
pack_sig_c	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
pack_sig_h	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
pack_sig_z	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
pack_sk_rho_key_tr	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	4s	-50%
pointwise_acc_native_aarch64	LP64	cadical	✅	59s	58s	+2%
	LP64	z3_smt_only*	✅	4s	5s	-20%
pointwise_acc_native_x86_64	LP64	cadical	✅	58s	59s	-2%
	LP64	z3_smt_only*	✅	6s	5s	+20%
pointwise_native_aarch64	LP64	bitwuzla	✅	24s	23s	+4%
	LP64	z3*	✅	3s	3s	+0%
pointwise_native_rv32im_fastmul	ILP32	z3*	✅	4s	3s	+33%
	LP64	cvc5_mbqi_enum	✅	8s	10s	-20%
	LP64	z3	✅	2s	3s	-33%
pointwise_native_rv32im_slowmul	ILP32	z3*	✅	2s	1s	+100%
	LP64	cvc5_mbqi_enum	✅	8s	8s	+0%
	LP64	z3	✅	4s	3s	+33%
pointwise_native_x86_64	LP64	bitwuzla	✅	28s	23s	+22%
	LP64	z3*	✅	2s	2s	+0%
poly_add	LP64	cadical	✅	54s	50s	+8%
	LP64	z3*	✅	11s	11s	+0%
poly_caddq	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_c	LP64	bitwuzla	✅	19s	19s	+0%
	LP64	z3*	✅	4s	2s	+100%
poly_caddq_native	LP64	bitwuzla	✅	142s	128s	+11%
	LP64	z3*	✅	2s	2s	+0%
poly_caddq_native_aarch64	LP64	cvc5_mbqi_enum	✅	35s	34s	+3%
	LP64	z3*	✅	3s	3s	+0%
poly_caddq_native_x86_64	LP64	bitwuzla	✅	161s	142s	+13%
	LP64	z3*	✅	1s	1s	+0%
poly_challenge	LP64	bitwuzla	✅	26s	27s	-4%
	LP64	z3*	✅	14s	12s	+17%
poly_chknorm	LP64	bitwuzla	✅	3s	5s	-40%
	LP64	z3*	✅	2s	2s	+0%
poly_chknorm_c	LP64	bitwuzla	✅	12s	9s	+33%
	LP64	z3*	✅	8s	7s	+14%
poly_chknorm_native	LP64	bitwuzla	✅	8s	9s	-11%
	LP64	z3*	✅	3s	3s	+0%
poly_chknorm_native_aarch64	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
poly_chknorm_native_x86_64	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	3s	+0%
poly_decompose	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	4s	1s	+300%
poly_decompose_32_native_aarch64	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	1s	2s	-50%
poly_decompose_88_native_aarch64	LP64	bitwuzla	✅	6s	6s	+0%
	LP64	z3*	✅	4s	4s	+0%
poly_decompose_c	LP64	cvc5_mbqi_enum	✅	228s	250s	-9%
	LP64	z3*	✅	4s	5s	-20%
poly_decompose_native	LP64	cadical	✅	14s	17s	-18%
	LP64	z3*	✅	3s	3s	+0%
poly_decompose_native_x86_64	LP64	cadical	✅	9s	11s	-18%
	LP64	z3*	✅	3s	2s	+50%
poly_invntt_tomont	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	2s	1s	+100%
poly_invntt_tomont_c	LP64	bitwuzla	✅	202s	176s	+15%
	LP64	z3_smt_only*	✅	5s	5s	+0%
poly_invntt_tomont_native	LP64	bitwuzla	✅	62s	49s	+27%
	LP64	z3*	✅	2s	2s	+0%
poly_ntt	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	3s	1s	+200%
poly_ntt_c	LP64	bitwuzla	✅	57s	56s	+2%
	LP64	z3_smt_only*	✅	9s	9s	+0%
poly_ntt_native	LP64	bitwuzla	✅	26s	29s	-10%
	LP64	z3*	✅	5s	4s	+25%
poly_permute_bitrev_to_custom_optional	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	2s	-50%
poly_permute_bitrev_to_custom_optional_native	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	3s	2s	+50%
poly_pointwise_montgomery	LP64	bitwuzla	✅	10s	12s	-17%
	LP64	z3*	✅	2s	4s	-50%
poly_pointwise_montgomery_c	LP64	bitwuzla	✅	237s	214s	+11%
	LP64	z3*	✅	52s	44s	+18%
poly_pointwise_montgomery_native	LP64	cvc5_mbqi_enum	✅	56s	54s	+4%
	LP64	z3*	✅	3s	4s	-25%
poly_power2round	LP64	bitwuzla	✅	324s	314s	+3%
	LP64	z3*	✅	2s	1s	+100%
poly_reduce	LP64	bitwuzla	✅	9s	7s	+29%
	LP64	z3*	✅	3s	3s	+0%
poly_shiftl	LP64	bitwuzla	✅	16s	12s	+33%
	LP64	z3*	✅	3s	2s	+50%
poly_sub	LP64	bitwuzla	✅	16s	19s	-16%
	LP64	z3*	✅	4s	2s	+100%
poly_uniform	LP64	bitwuzla	✅	229s	187s	+22%
	LP64	z3*	✅	3s	2s	+50%
poly_uniform_4x	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	4s	2s	+100%
poly_uniform_eta	LP64	bitwuzla	✅	93s	92s	+1%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_eta_4x	LP64	cadical	✅	65s	63s	+3%
	LP64	z3*	✅	11s	8s	+38%
poly_uniform_gamma1	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
poly_uniform_gamma1_4x	LP64	cadical	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
poly_use_hint	LP64	cvc5_mbqi_enum	✅	25s	25s	+0%
	LP64	z3*	✅	4s	2s	+100%
poly_use_hint_c	LP64	cvc5_enum_inst	✅	13s	12s	+8%
	LP64	z3*	✅	4s	3s	+33%
poly_use_hint_native	LP64	cvc5_mbqi_enum	✅	86s	87s	-1%
	LP64	z3*	✅	2s	3s	-33%
poly_use_hint_native_aarch64	LP64	bitwuzla	✅	34s	36s	-6%
	LP64	z3*	✅	3s	5s	-40%
poly_use_hint_native_x86_64	LP64	bitwuzla	✅	45s	35s	+29%
	LP64	z3*	✅	2s	3s	-33%
polyeta_pack	LP64	bitwuzla	✅	7s	5s	+40%
	LP64	z3*	✅	4s	2s	+100%
polyeta_unpack	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	12s	9s	+33%
polyt0_pack	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	2s	2s	+0%
polyt0_unpack	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	9s	9s	+0%
polyt1_pack	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	3s	+33%
polyt1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	6s	4s	+50%
polyvec_matrix_expand	LP64	z3_no_bv_extract*	✅	2s	1s	+100%
polyvec_matrix_expand_serial	LP64	z3*	✅	3s	1s	+200%
polyvec_matrix_pointwise_montgomery_row	LP64	cadical	✅	41s	41s	+0%
	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
polyvec_matrix_pointwise_montgomery_yvec	LP64	cadical	✅	580s	489s	+19%
	LP64	z3*	✅	185s	156s	+19%
polyveck_caddq	LP64	cadical	✅	113s	106s	+7%
	LP64	z3*	✅	2s	2s	+0%
polyveck_decompose_pack_w1	LP64	cadical	✅	108s	110s	-2%
	LP64	z3*	✅	2s	3s	-33%
polyveck_invntt_tomont	LP64	cadical	✅	143s	175s	-18%
	LP64	z3*	✅	1s	2s	-50%
polyveck_ntt	LP64	cadical	✅	3s	4s	-25%
	LP64	z3*	✅	2s	3s	-33%
polyveck_reduce	LP64	cadical	✅	129s	123s	+5%
	LP64	z3*	✅	2s	2s	+0%
polyveck_unpack_eta	LP64	cvc5_mbqi_enum	✅	2s	4s	-50%
	LP64	z3*	✅	2s	3s	-33%
polyveck_unpack_eta_chknorm	LP64	cvc5_mbqi_enum	✅	17s	16s	+6%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_chknorm	LP64	cadical	✅	53s	56s	-5%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_ntt	LP64	cadical	✅	129s	119s	+8%
	LP64	z3*	✅	4s	2s	+100%
polyvecl_pointwise_acc_montgomery	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
	LP64	z3_smt_only*	✅	2s	2s	+0%
polyvecl_pointwise_acc_montgomery_c	LP64	cadical	✅	2s	2s	+0%
	LP64	z3_smt_only*	✅	3s	1s	+200%
polyvecl_pointwise_acc_montgomery_native	LP64	cvc5_mbqi_enum	✅	3s	4s	-25%
	LP64	z3_smt_only*	✅	3s	4s	-25%
polyvecl_uniform_gamma1	LP64	cvc5_mbqi_enum	✅	2s	2s	+0%
	LP64	z3*	✅	1s	4s	-75%
polyvecl_uniform_gamma1_serial	LP64	cvc5_mbqi_enum	✅	2s	3s	-33%
	LP64	z3*	✅	3s	1s	+200%
polyvecl_unpack_eta	LP64	cvc5_mbqi_enum	✅	34s	33s	+3%
	LP64	z3*	✅	3s	2s	+50%
polyvecl_unpack_z	LP64	cvc5_mbqi_enum	✅	27s	27s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyw1_pack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	3s	+0%
polyw1_pack_32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	3s	-67%
polyw1_pack_88	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	2s	+50%
polyw1_unpack	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
polyw1_unpack_32	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	3s	-33%
polyw1_unpack_88	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	4s	4s	+0%
polyz_pack	LP64	bitwuzla	✅	6s	3s	+100%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack	LP64	bitwuzla	✅	10s	6s	+67%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_17_native_aarch64	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	2s	+50%
polyz_unpack_19_native_aarch64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	3s	-33%
polyz_unpack_c	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	5s	6s	-17%
polyz_unpack_native	LP64	bitwuzla	✅	25s	27s	-7%
	LP64	z3*	✅	1s	3s	-67%
polyz_unpack_native_x86_64	LP64	bitwuzla	✅	17s	16s	+6%
	LP64	z3*	✅	2s	2s	+0%
power2round	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	3s	+0%
reduce32	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
rej_eta	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	3s	2s	+50%
rej_eta_c	LP64	bitwuzla*	✅	6s	3s	+100%
	LP64	z3	✅	12s	14s	-14%
rej_eta_native	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	✅	22s	20s	+10%
rej_uniform	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	10s	13s	-23%
rej_uniform_c	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	12s	10s	+20%
rej_uniform_eta_native_aarch64	LP64	bitwuzla*	✅	1s	4s	-75%
	LP64	z3_smt_only	✅	4s	4s	+0%
rej_uniform_eta_native_x86_64	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3_smt_only*	✅	3s	3s	+0%
rej_uniform_native	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3_smt_only	✅	11s	10s	+10%
rej_uniform_native_aarch64	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3_smt_only	✅	3s	3s	+0%
rej_uniform_native_x86_64	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3_smt_only*	✅	13s	10s	+30%
shake128_absorb	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	3s	-33%
shake128_finalize	LP64	cvc5_arrays_exp	✅	4s	1s	+300%
	LP64	z3*	✅	1s	2s	-50%
shake128_init	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	1s	+200%
shake128_release	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	3s	-67%
shake128_squeeze	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
shake128x4_absorb_once	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	✅	2s	3s	-33%
shake128x4_squeezeblocks	LP64	bitwuzla*	✅	5s	1s	+400%
	LP64	z3	✅	4s	2s	+100%
shake256	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
shake256_absorb	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
shake256_finalize	LP64	cvc5_arrays_exp	✅	4s	2s	+100%
	LP64	z3*	✅	4s	1s	+300%
shake256_init	LP64	cvc5_arrays_exp	✅	3s	1s	+200%
	LP64	z3*	✅	2s	2s	+0%
shake256_release	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	2s	+50%
shake256_squeeze	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	2s	+0%
shake256x4_absorb_once	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	2s	+0%
shake256x4_squeezeblocks	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3_smt_only	✅	2s	1s	+100%
sig_unpack_hints	LP64	bitwuzla	✅	59s	60s	-2%
	LP64	z3*	✅	24s	26s	-8%
sign_keypair	LP64	cadical	✅	49s	51s	-4%
	LP64	z3*	✅	4s	4s	+0%
sign_keypair_internal	LP64	cadical	✅	161s	154s	+5%
	LP64	z3_no_bv_extract*	✅	15s	15s	+0%
sign_pk_from_sk	LP64	z3_no_bv_extract*	✅	28s	34s	-18%
sign_signature	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	5s	3s	+67%
sign_signature_extmu	LP64	cadical	✅	24s	21s	+14%
	LP64	z3*	✅	1s	3s	-67%
sign_signature_internal	LP64	z3_no_bv_extract*	✅	13s	11s	+18%
sign_signature_pre_hash_internal	LP64	bitwuzla	✅	7s	3s	+133%
	LP64	z3*	✅	3s	3s	+0%
sign_signature_pre_hash_shake256	LP64	cadical	✅	14s	12s	+17%
	LP64	z3*	✅	6s	3s	+100%
sign_verify	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	2s	2s	+0%
sign_verify_extmu	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	6s	3s	+100%
sign_verify_internal	LP64	z3_no_bv_extract*	✅	240s	218s	+10%
sign_verify_pre_hash_internal	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
sign_verify_pre_hash_shake256	LP64	bitwuzla	✅	4s	4s	+0%
	LP64	z3*	✅	5s	3s	+67%
sk_s1hat_get_poly	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	2s	2s	+0%
sk_s2hat_get_poly	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	1s	+100%
sk_t0hat_get_poly	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	1s	+0%
sys_check_capability	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	2s	+0%
unpack_pk_t1	LP64	bitwuzla	✅	13s	12s	+8%
	LP64	z3*	✅	1s	1s	+0%
unpack_sk	LP64	cadical	✅	4s	3s	+33%
	LP64	z3*	✅	3s	1s	+200%
unpack_sk_s1hat	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	2s	2s	+0%
unpack_sk_s2hat	LP64	cvc5_mbqi_enum	✅	1s	1s	+0%
	LP64	z3*	✅	4s	3s	+33%
unpack_sk_t0hat	LP64	cadical	✅	1s	2s	-50%
	LP64	z3*	✅	2s	1s	+100%
use_hint	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
yvec_get_poly	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
yvec_init	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%

[github-actions]

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	2129870 cycles	2129863 cycles	1.00
ML-DSA-44 sign	16453128 cycles	17791740 cycles	0.92
ML-DSA-44 verify	2398876 cycles	2398890 cycles	1.00
ML-DSA-65 keypair	3731142 cycles	3731150 cycles	1.00
ML-DSA-65 sign	13926258 cycles	15034565 cycles	0.93
ML-DSA-65 verify	4012792 cycles	4012806 cycles	1.00
ML-DSA-87 keypair	6483505 cycles	6483258 cycles	1.00
ML-DSA-87 sign	23689890 cycles	25052782 cycles	0.95
ML-DSA-87 verify	6865468 cycles	6865084 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	2328440 cycles	2328425 cycles	1.00
ML-DSA-44 sign	16453121 cycles	17791719 cycles	0.92
ML-DSA-44 verify	2398868 cycles	2398854 cycles	1.00
ML-DSA-65 keypair	4025151 cycles	4025137 cycles	1.00
ML-DSA-65 sign	13926279 cycles	15034565 cycles	0.93
ML-DSA-65 verify	4012806 cycles	4012799 cycles	1.00
ML-DSA-87 keypair	6864901 cycles	6864894 cycles	1.00
ML-DSA-87 sign	23684886 cycles	25049136 cycles	0.95
ML-DSA-87 verify	6864419 cycles	6864405 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	216636 cycles	219078 cycles	0.99
ML-DSA-44 sign	575604 cycles	603963 cycles	0.95
ML-DSA-44 verify	217827 cycles	217691 cycles	1.00
ML-DSA-65 keypair	383224 cycles	384101 cycles	1.00
ML-DSA-65 sign	943082 cycles	994891 cycles	0.95
ML-DSA-65 verify	368499 cycles	372051 cycles	0.99
ML-DSA-87 keypair	639519 cycles	645476 cycles	0.99
ML-DSA-87 sign	1266823 cycles	1330055 cycles	0.95
ML-DSA-87 verify	621041 cycles	629238 cycles	0.99

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	301525 cycles	297514 cycles	1.01
ML-DSA-44 sign	1092324 cycles	1130782 cycles	0.97
ML-DSA-44 verify	332434 cycles	330092 cycles	1.01
ML-DSA-65 keypair	547265 cycles	544902 cycles	1.00
ML-DSA-65 sign	1720491 cycles	1850869 cycles	0.93
ML-DSA-65 verify	530876 cycles	528082 cycles	1.01
ML-DSA-87 keypair	854708 cycles	848422 cycles	1.01
ML-DSA-87 sign	2241005 cycles	2353835 cycles	0.95
ML-DSA-87 verify	882179 cycles	881818 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[github-actions]

SpacemiT K1 8 (Banana Pi F3) benchmarks (no-opt)

Details

Benchmark suite	Current: 6840735	Previous: 929b149	Ratio
ML-DSA-44 keypair	759381 cycles	757723 cycles	1.00
ML-DSA-44 sign	3011050 cycles	3138207 cycles	0.96
ML-DSA-44 verify	858873 cycles	856800 cycles	1.00
ML-DSA-65 keypair	1288355 cycles	1288667 cycles	1.00
ML-DSA-65 sign	4731285 cycles	5093210 cycles	0.93
ML-DSA-65 verify	1367624 cycles	1367550 cycles	1.00
ML-DSA-87 keypair	2105568 cycles	2110630 cycles	1.00
ML-DSA-87 sign	5995343 cycles	6351787 cycles	0.94
ML-DSA-87 verify	2220607 cycles	2226957 cycles	1.00

This comment was automatically generated by workflow using github-action-benchmark.

[hanno-becker]

@mkannwischer This looks like an impressive improvement. What's the status here? Are you planning further work / cleanup, or should this be reviewed?

[mkannwischer]

@mkannwischer This looks like an impressive improvement. What's the status here? Are you planning further work / cleanup, or should this be reviewed?

Ready for review and I think we should make this change.