Expression not simplified in all contexts

With the attached files, you can reach the state that illustrates the issue with command:

kore-repl definition.kore --module VERIFICATION --prove spec.kore --spec-module VAT-SLIP-PASS-ROUGH-SPEC

The files s0.k and s0.kore contain the initial state. There are 2 nested hashedLocation expressions there that should be simplified but they don't. They should be simplified by the rule in definition.kore line 17552 (original source code hashed-locations.md line 63).
For the inner hashedLocation, rule above has some range requirements for variable VarILK. It satisfies the requirements in s0.kore on lines 1972 and 2165.

Note that during simplification process the same expression is generated twice in the configuration. In one place it gets stuck in hashedLocation state, in another one it is properly simplified into:

keccak ( #buf ( 32 , USR:Int ) ++ #buf ( 32 , keccak ( #buf ( 32 , ILK:Int ) ++ b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x04" ) ) )

So it is simplified in one place but not another. This is not high priority, but is required to pass some failing proofs in KEVM and KSummarizer.

Please let me know if you need any help.
haskell-bug-report.zip

Start by running the kore-repl command from the issue with the attached definition.kore, s0.k.kore, and spec.kore files. Inspect definition.kore line 17552 and hashed-locations.md line 63, then compare the two generated configuration occurrences. Done means both nested hashedLocation expressions simplify consistently and the affected KEVM or KSummarizer proofs pass.