We shoudn't be returning a Step here, because that indicates taking a rewrite step of depth 1. We should instead be returning an abstraction.
That makes me think, we could maybe integrate this into abstract_node, it's used here by the exploration: https://github.com/runtimeverification/k/blob/547e2cc337d08ba19820a3c22956091c0a9aebf8/pyk/src/pyk/kcfg/explore.py#L227. And KEVM's node abstractor is here: https://github.com/runtimeverification/evm-semantics/blob/b40fd7b09fd79dcb3fa13fc6d8f9a02451e8a475/kevm-pyk/src/kevm_pyk/kevm.py#L125.
So that could look for the correct pattern, and remove the appropriate constraints.
Originally posted by @ehildenb in #899 (comment)
Originally posted by @ehildenb in #899 (comment)