Expression not simplified in all contexts

[denis-bogdanas]

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

[ehildenb]

Same as this problem, I think: #2785

[ana-pantilie]

It's not the same problem as ^, the test is being run on CI.

Needs to be reproduced.