{"action":"closed","issue":{"url":"https://api.github.com/repos/Microsoft/dafny/issues/1","repository_url":"https://api.github.com/repos/Microsoft/dafny","labels_url":"https://api.github.com/repos/Microsoft/dafny/issues/1/labels{/name}","comments_url":"https://api.github.com/repos/Microsoft/dafny/issues/1/comments","events_url":"https://api.github.com/repos/Microsoft/dafny/issues/1/events","html_url":"https://github.com/Microsoft/dafny/issues/1","id":161814605,"number":1,"title":"Dafny crash in Translator.FuelSetting.GetFunctionFuel","user":{"login":"jaylorch","id":14809591,"avatar_url":"https://avatars.githubusercontent.com/u/14809591?v=3","gravatar_id":"","url":"https://api.github.com/users/jaylorch","html_url":"https://github.com/jaylorch","followers_url":"https://api.github.com/users/jaylorch/followers","following_url":"https://api.github.com/users/jaylorch/following{/other_user}","gists_url":"https://api.github.com/users/jaylorch/gists{/gist_id}","starred_url":"https://api.github.com/users/jaylorch/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaylorch/subscriptions","organizations_url":"https://api.github.com/users/jaylorch/orgs","repos_url":"https://api.github.com/users/jaylorch/repos","events_url":"https://api.github.com/users/jaylorch/events{/privacy}","received_events_url":"https://api.github.com/users/jaylorch/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":{"login":"qunyanm","id":15744202,"avatar_url":"https://avatars.githubusercontent.com/u/15744202?v=3","gravatar_id":"","url":"https://api.github.com/users/qunyanm","html_url":"https://github.com/qunyanm","followers_url":"https://api.github.com/users/qunyanm/followers","following_url":"https://api.github.com/users/qunyanm/following{/other_user}","gists_url":"https://api.github.com/users/qunyanm/gists{/gist_id}","starred_url":"https://api.github.com/users/qunyanm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qunyanm/subscriptions","organizations_url":"https://api.github.com/users/qunyanm/orgs","repos_url":"https://api.github.com/users/qunyanm/repos","events_url":"https://api.github.com/users/qunyanm/events{/privacy}","received_events_url":"https://api.github.com/users/qunyanm/received_events","type":"User","site_admin":false},"assignees":[{"login":"qunyanm","id":15744202,"avatar_url":"https://avatars.githubusercontent.com/u/15744202?v=3","gravatar_id":"","url":"https://api.github.com/users/qunyanm","html_url":"https://github.com/qunyanm","followers_url":"https://api.github.com/users/qunyanm/followers","following_url":"https://api.github.com/users/qunyanm/following{/other_user}","gists_url":"https://api.github.com/users/qunyanm/gists{/gist_id}","starred_url":"https://api.github.com/users/qunyanm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/qunyanm/subscriptions","organizations_url":"https://api.github.com/users/qunyanm/orgs","repos_url":"https://api.github.com/users/qunyanm/repos","events_url":"https://api.github.com/users/qunyanm/events{/privacy}","received_events_url":"https://api.github.com/users/qunyanm/received_events","type":"User","site_admin":false}],"milestone":null,"comments":1,"created_at":"2016-06-23T00:15:06Z","updated_at":"2016-06-24T03:20:45Z","closed_at":"2016-06-24T03:20:45Z","body":"Dafny crashes in Translator.FuelSetting.GetFunctionFuel when verifying the code below:\r\n\r\n```\r\ndatatype T = T(n:int)\r\n\r\nfunction ToInt(t:T) : int\r\n    ensures ToInt(t) == int(t.n);\r\n{\r\n    int(t.n)\r\n}\r\n\r\nmethod Test()\r\n{\r\n    assert exists p:int :: exists t:T :: ToInt(t) > 0;\r\n}\r\n```"}}
{"actor":{"display_login":"qunyanm"}}