Simplification rule with `symbolic` attribute applied on concrete input

The issue is reported by @lucasmt pn Slack, see the thread. I'm quoting the message here:

This is really weird, I tried adding the normalization rule suggested for *Int:

rule A *Int B => B *Int A [concrete(A), symbolic(B), simplification(40)]

But now there's something odd happening when calling the freshUInt cheatcode. The ensures clause should be introducing the constraint ?WORD <Int 2 ^Int (8 *Int #asWord(ARGS)). But when calling kevm.freshUInt(32), it looks like this constraint is getting simplified to ?WORD <Int #powByteLen(32), which then causes the tool to crash. But this shouldn't be happening because the rule that introduces #powByteLen should only apply when the size is symbolic:

rule 2 ^Int (SIZE *Int 8) => #powByteLen(SIZE) [symbolic(SIZE), simplification]

Is it possible the the backend is ignoring the symbolic attribute?

Start by reproducing the kevm.freshUInt(32) case from the issue and inspect the two quoted simplification rules, especially their symbolic and concrete attributes. Done means concrete SIZE input is not rewritten by the symbolic rule and the resulting constraint no longer causes the tool to crash.