Update to Boogie 2.9.5 #165
Open
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
|
@Dargones I am checking on the corral regression error. It seems non-trivial -- the query made by corral to z3 seems right, but somehow z3 simply times out. I'll have to look at the query and flags more closely. I'm also struggling to run old corral (from main branch). Are you able to run it? If so, I can try to get that set up also and do a diff. |
|
I have pushed a fix. that at least fixes some of the bugs. I haven't run the full regressions. |
|
Thank you @akashlal! The two tests still time out, it seems - will look more into this! I did not have any trouble setting up corral from the main branch (I am on Linux, I think the only two requirements are dotnet6 and z3 4.8.8) |
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.
This is a draft of changes necessary to make Corral work with Boogie 2.9.5. The main challenge in updating to this version is addressing this commit, which changes the way unique AST node identifiers work in Boogie.
I have been able to make most regression tests pass but there are two that now timeout (this, and this) and the av-regressions fails seemingly because it does not produce debugging output. @akashlal, would you have any suggestions as to what might be the issue? I must be missing case where the mapping between Absy nodes and IDs is important but so far was not able to identify the problem.
A small change is required to Boogie itself, so I currently add a special "corral" branch of Boogie as a submodule. The goal is to keep updating the branch and corral in sync until the updates could be merged into main.