-
Notifications
You must be signed in to change notification settings - Fork 29
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
Update to Boogie 2.9.5 #165
base: master
Are you sure you want to change the base?
Conversation
@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) |
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.