Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prune #Bottom states when branching #3650

Merged
merged 3 commits into from
Sep 7, 2023
Merged

Conversation

goodlyrottenapple
Copy link
Contributor

Fix for change introduced by #3637, wherein branching could contain bottom states which were not being pruned. (see runtimeverification/pyk#634 (comment))

@goodlyrottenapple goodlyrottenapple marked this pull request as ready for review September 6, 2023 17:39
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code change LGTM.
Re-ran the integration test in CI 🤞

@@ -11,7 +11,6 @@ constraints: any.Cabal ==3.6.3.0,
aeson -cffi +ordered-keymap,
any.aeson-pretty ==0.8.9,
aeson-pretty -lib-only,
any.alex ==3.2.7.4,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Curious, why would you like to remove those dependencies?
Maybe we should adapt the scripts that check or re-freeze if we need to remove them.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have already removed these from the booster. they should not be fixed because the nix version of cabal comes with a different version of alex and happy and cant figure out a build plan using these

@jberthold
Copy link
Member

Re-ran the integration test in CI 🤞

That did not work, though... kore-exec gets killed (error 137) in a search command

krun --haskell-backend-command kore-exec --definition ./test-kompiled --search-final 2.test \
    --output-file 2.test.out --output /tmp/nix-shell.NiDd7o/.krun-2023-09-06-23-59-15-7rLPGoxTwy/result.kore  \
    --searchType FINAL --search 

@goodlyrottenapple goodlyrottenapple merged commit 0d98bc9 into master Sep 7, 2023
8 of 9 checks passed
@goodlyrottenapple goodlyrottenapple deleted the sam/vacuous-bottom-fix branch September 7, 2023 09:35
@PetarMax
Copy link
Contributor

PetarMax commented Sep 8, 2023

@goodlyrottenapple @geo2a I've also addressed this issue by pruning the #Bottom branches in pyk right now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants