{"action":"created","issue":{"url":"https://api.github.com/repos/Microsoft/dafny/issues/229","repository_url":"https://api.github.com/repos/Microsoft/dafny","labels_url":"https://api.github.com/repos/Microsoft/dafny/issues/229/labels{/name}","comments_url":"https://api.github.com/repos/Microsoft/dafny/issues/229/comments","events_url":"https://api.github.com/repos/Microsoft/dafny/issues/229/events","html_url":"https://github.com/Microsoft/dafny/issues/229","id":422384330,"node_id":"MDU6SXNzdWU0MjIzODQzMzA=","number":229,"title":"How do I profile my way out of unbounded timeouts?","user":{"login":"jonhnet","id":1816420,"node_id":"MDQ6VXNlcjE4MTY0MjA=","avatar_url":"https://avatars3.githubusercontent.com/u/1816420?v=4","gravatar_id":"","url":"https://api.github.com/users/jonhnet","html_url":"https://github.com/jonhnet","followers_url":"https://api.github.com/users/jonhnet/followers","following_url":"https://api.github.com/users/jonhnet/following{/other_user}","gists_url":"https://api.github.com/users/jonhnet/gists{/gist_id}","starred_url":"https://api.github.com/users/jonhnet/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonhnet/subscriptions","organizations_url":"https://api.github.com/users/jonhnet/orgs","repos_url":"https://api.github.com/users/jonhnet/repos","events_url":"https://api.github.com/users/jonhnet/events{/privacy}","received_events_url":"https://api.github.com/users/jonhnet/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2019-03-18T19:01:54Z","updated_at":"2019-03-18T20:42:48Z","closed_at":null,"author_association":"NONE","body":"Say I write some (purely functional) Dafny, and try to verify it. Things are going great. I'm using my superstitions (opaque recursion, exists and comprehensions) to ward off timeouts. Then suddenly I descend into timeout hell: Dafny will spend unbounded time trying to verify a lemma.\r\n\r\nNo problem, I say! I'll just axiom-profiler that thing, and figure out which sheep entrail I arranged incorrectly! Except that I can't make an axiom profiler work, either. I'm looking for advice, either at the high level (\"don't try to diagnose timeouts this way; that's so 2015\") or the low level (\"use a different profiler\" or \"ah, you're passing the wrong flag to z3; that's why the profiler doesn't work.\")\r\n\r\nThis is a significant blocking issue for my use of Dafny (and my encouraging others to use it), as I am unable to even offer expert help to unblock a \"timeout-infected\" Dafny module.\r\n\r\n\r\nDetails:\r\n\r\nI have attached an example file that hangs Dafny.\r\nHere is how I tried to diagnose it. I'm using a Linux build here, but I have also tried this process on Windows with no success.\r\n\r\n1. Capture a Boogie file with Dafny 2.2.0.10923.\r\n```dafny /timeLimit:2 /print:test.bpl raftInvariants.dfy```\r\n2. Capture a z3 log with Boogie 2.3.0.61016 and Z3 \"version 4.8.5 - 64 bit\", git commit 17adecff6802dad7f381dce3a74a1c96acc8dedb of Feb 25.\r\n```mono ~/dafny-base/boogie/Binaries/Boogie.exe /z3exe:/home/jonh/axiom-profiler/z3/build/z3 /proc:'Impl$$_5_raftInvariants.__default.ElectionSafetyInduction' /timeLimit:8 /z3opt:TRACE=true /z3opt:PROOF=true test.bpl```\r\nZ3 is built from ```git clone https://github.com/Nils-Becker/z3.git```, as advised by the Axiom Profiler page.\r\n3. Run the viper axiom profiler ```hg clone https://bitbucket.org/viperproject/axiom-profiler```, hg changeset 357:f0f7be18b655 of Feb 22 2019.\r\n```mono ~/axiom-profiler/axiom-profiler/bin/Release/AxiomProfiler.exe /l:z3.log```\r\n\r\nWith this particular run, the failure mode is that the axiom profiler draws a Processing... progress bar, closes it, and then spins many minutes; it never opens the profiler page. (With other runs, I have seen a \"Stack empty\" exception, and then a profiler page. When I have gotten a profiler page, it was with the Stack Empty exception; the result has been unhelpful: the worst offending term had 16 instantiations. I suspect the exception meant the profiler dropped all the important bits?)\r\n\r\n[raftTimesOutExample.zip](https://github.com/Microsoft/dafny/files/2979750/raftTimesOutExample.zip)\r\n"},"comment":{"url":"https://api.github.com/repos/Microsoft/dafny/issues/comments/474092758","html_url":"https://github.com/Microsoft/dafny/issues/229#issuecomment-474092758","issue_url":"https://api.github.com/repos/Microsoft/dafny/issues/229","id":474092758,"node_id":"MDEyOklzc3VlQ29tbWVudDQ3NDA5Mjc1OA==","user":{"login":"jonhnet","id":1816420,"node_id":"MDQ6VXNlcjE4MTY0MjA=","avatar_url":"https://avatars3.githubusercontent.com/u/1816420?v=4","gravatar_id":"","url":"https://api.github.com/users/jonhnet","html_url":"https://github.com/jonhnet","followers_url":"https://api.github.com/users/jonhnet/followers","following_url":"https://api.github.com/users/jonhnet/following{/other_user}","gists_url":"https://api.github.com/users/jonhnet/gists{/gist_id}","starred_url":"https://api.github.com/users/jonhnet/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonhnet/subscriptions","organizations_url":"https://api.github.com/users/jonhnet/orgs","repos_url":"https://api.github.com/users/jonhnet/repos","events_url":"https://api.github.com/users/jonhnet/events{/privacy}","received_events_url":"https://api.github.com/users/jonhnet/received_events","type":"User","site_admin":false},"created_at":"2019-03-18T20:42:48Z","updated_at":"2019-03-18T20:42:48Z","author_association":"NONE","body":"Oh, my windows run only saw costs of ~40k, which didn't seem glaringly suspicious. (/c:2 gave the Stack Empty exception, and had *very* low costs.)"}}
{"actor":{"display_login":"jonhnet"}}