Skip to content

Update to Boogie 2.15.9#441

Merged
gauravpartha merged 9 commits into
masterfrom
boogie_dotnet6
Dec 22, 2022
Merged

Update to Boogie 2.15.9#441
gauravpartha merged 9 commits into
masterfrom
boogie_dotnet6

Conversation

@gauravpartha

Copy link
Copy Markdown
Contributor

No description provided.

@gauravpartha

Copy link
Copy Markdown
Contributor Author

Locally on my machine, the tests run around 15% slower in total using the updated Boogie version. It would be nice to use the new /normalizeNames:1 Boogie option (generates names in the SMT file in a way that is more robust to changes in the Boogie program). However, on my machine, the verifying test https://github.com/viperproject/silver/blob/master/src/test/resources/all/issues/silicon/0483a.vpr then goes from around 45 seconds to 6 minutes. So, we decided to not use the /normalizeNames:1 option for now. It is not clear why the verification time changes by so much for this file if one uses /normalizeNames:1; it would make sense to investigate this at some point.

@gauravpartha gauravpartha marked this pull request as ready for review December 22, 2022 08:39
@gauravpartha gauravpartha merged commit d6c9c74 into master Dec 22, 2022
@gauravpartha gauravpartha deleted the boogie_dotnet6 branch February 21, 2023 10:43
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.

1 participant