Investigate if optimizing constant generation to avoid allocations improve solver performance

[celinval]

Requested feature: Optimize code generation of constants
Use case: Improve solver performance due to better constant propagation.

We currently generate an allocation when initializing an ADT with more than one non-zst field instead of initializing it from value. While porting Kani to StableMIR, I noticed that CBMC seems to perform better when we don't use an allocation. We should investigate reducing the number of allocations.

For example, for the test cargo-kani/mir-linker, CBMC will not be able to find the loop bounds if we treat all ADTs as allocations.