-
Notifications
You must be signed in to change notification settings - Fork 13
Open
Description
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)
Metadata
Metadata
Assignees
Labels
No labels