#468 caused a performance regression for the ML-DSA-87 CBMC proofs from 8 minutes to 20 minutes.
It's odd because #468 does not modify any code that should be relevant to CBMC proofs.
We should investigate and get the proof performance back to what it was before.