{"action":"closed","issue":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/40","repository_url":"https://api.github.com/repos/boogie-org/boogie","labels_url":"https://api.github.com/repos/boogie-org/boogie/issues/40/labels{/name}","comments_url":"https://api.github.com/repos/boogie-org/boogie/issues/40/comments","events_url":"https://api.github.com/repos/boogie-org/boogie/issues/40/events","html_url":"https://github.com/boogie-org/boogie/issues/40","id":165845769,"number":40,"title":"/trace output is less helpful than it could be due to buffering","user":{"login":"0xabu","id":13037682,"avatar_url":"https://avatars2.githubusercontent.com/u/13037682?v=3","gravatar_id":"","url":"https://api.github.com/users/0xabu","html_url":"https://github.com/0xabu","followers_url":"https://api.github.com/users/0xabu/followers","following_url":"https://api.github.com/users/0xabu/following{/other_user}","gists_url":"https://api.github.com/users/0xabu/gists{/gist_id}","starred_url":"https://api.github.com/users/0xabu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/0xabu/subscriptions","organizations_url":"https://api.github.com/users/0xabu/orgs","repos_url":"https://api.github.com/users/0xabu/repos","events_url":"https://api.github.com/users/0xabu/events{/privacy}","received_events_url":"https://api.github.com/users/0xabu/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-07-15T18:08:16Z","updated_at":"2017-06-22T22:01:08Z","closed_at":"2017-06-22T22:01:08Z","body":"Just a minor nitpick. When running Boogie with /trace, it produces output such as:\n\n```\nVerifying CheckWellformed$$_.foo ...\n  [0.716 s, 2 proof obligations]  verified\n\nVerifying Impl$$_.foo ...\n  [187.421 s, 225 proof obligations]  verified\n```\n\nHowever, the line for \"Verifying\" only appears in the console window at the same time that the second line with the result information is printed, so you're never sure what Boogie is currently attempting to verify. I assume this could be fixed by adding an `fflush()`-equivalent between the two print statements.\n\nThis issue also applies to Dafny as Microsoft/dafny#10\n"}}
{"actor":{"display_login":"0xabu"}}