How to create constant non-deterministic array?

[hflsmax]

Sorry if this is not the right place to ask questions.

I need to create an array with non-deterministic value. I understand that I can use an uninitialized local variable. But I also want to make the array constant(meaning array.id()==ID_constant inside cbmc) so I can benefit from the performance gain during bit-blasting.

How I can make an array with non-deterministic value while being of type ID_constant?

[tautschnig]

With apologies for the very late response. We do not currently have a concept of symbolic constants, hence constant propagation would not be performed on this. If #3619 were to be merged, this situation would change.

That said, would you have an example to share where you'd expect benefit from constant-propagating symbolic constants?

[tautschnig]

@hflsmax We'd need more input to progress this issue. Please feel free to re-open when you have additional information.