Distinguish \bottom from stuck states #2451
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…amework/kore into distinguish-bottom-from-stuck-states
ttuegel
suggested changes
Mar 12, 2021
ttuegel
approved these changes
Mar 15, 2021
ana-pantilie
approved these changes
Mar 16, 2021
kore/src/Kore/Step.hs
Outdated
| configs <- lift $ Pattern.simplifyTopConfiguration config | ||
| filteredConfigs <- SMT.Evaluator.filterMultiOr configs | ||
| asum (pure <$> toList filteredConfigs) | ||
| if filteredConfigs == mempty |
There was a problem hiding this comment.
Suggested change
| if filteredConfigs == mempty | |
| if null filteredConfigs |
There was a problem hiding this comment.
Sorry, disregard this comment. I added it before you changed this line, but for some reason the review didn't go through.
goodlyrottenapple
added a commit
that referenced
this pull request
Aug 9, 2023
Another attempt at addressing runtimeverification/evm-semantics#1944. Addresses #3630 (needs a follow-up in booster) This change mimicks what kore-exe in prover mode returns(as introduced by #2451), namely the configuration goes to bottom
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When the last configuration rewrites to \bottom, the backend will report that instead of reporting the last configuration as "stuck".
Fixes #2445.
Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.