{"action":"created","issue":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/7","labels_url":"https://api.github.com/repos/boogie-org/boogie/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/boogie-org/boogie/issues/7/comments","events_url":"https://api.github.com/repos/boogie-org/boogie/issues/7/events","html_url":"https://github.com/boogie-org/boogie/issues/7","id":69735795,"number":7,"title":"Boogie allows identifiers to start with . and @, which SMTLIB does not","user":{"login":"zvonimir","id":1040926,"avatar_url":"https://avatars.githubusercontent.com/u/1040926?v=3","gravatar_id":"","url":"https://api.github.com/users/zvonimir","html_url":"https://github.com/zvonimir","followers_url":"https://api.github.com/users/zvonimir/followers","following_url":"https://api.github.com/users/zvonimir/following{/other_user}","gists_url":"https://api.github.com/users/zvonimir/gists{/gist_id}","starred_url":"https://api.github.com/users/zvonimir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zvonimir/subscriptions","organizations_url":"https://api.github.com/users/zvonimir/orgs","repos_url":"https://api.github.com/users/zvonimir/repos","events_url":"https://api.github.com/users/zvonimir/events{/privacy}","received_events_url":"https://api.github.com/users/zvonimir/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":11,"created_at":"2015-04-21T03:44:49Z","updated_at":"2015-04-24T17:34:49Z","closed_at":null,"body":"The following legal Boogie program (based on its current language spec):\r\n```\r\nprocedure foo() {\r\n  var .x:int;\r\n  assert .x == 0;\r\n}\r\n```\r\ncauses Boogie to throw an exception when used with CVC4:\r\n```\r\nboogie test.bpl /proverOpt:SOLVER=cvc4\r\n```\r\n\r\nHere is the exception excerpt:\r\n```\r\nProver error: (error \"Parse Error: <stdin>:11.15: cannot declare or define symbol `.x'; symbols starting with . and @ are reserved in SMT-LIB\r\n```"},"comment":{"url":"https://api.github.com/repos/boogie-org/boogie/issues/comments/96008361","html_url":"https://github.com/boogie-org/boogie/issues/7#issuecomment-96008361","issue_url":"https://api.github.com/repos/boogie-org/boogie/issues/7","id":96008361,"user":{"login":"delcypher","id":511795,"avatar_url":"https://avatars.githubusercontent.com/u/511795?v=3","gravatar_id":"","url":"https://api.github.com/users/delcypher","html_url":"https://github.com/delcypher","followers_url":"https://api.github.com/users/delcypher/followers","following_url":"https://api.github.com/users/delcypher/following{/other_user}","gists_url":"https://api.github.com/users/delcypher/gists{/gist_id}","starred_url":"https://api.github.com/users/delcypher/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/delcypher/subscriptions","organizations_url":"https://api.github.com/users/delcypher/orgs","repos_url":"https://api.github.com/users/delcypher/repos","events_url":"https://api.github.com/users/delcypher/events{/privacy}","received_events_url":"https://api.github.com/users/delcypher/received_events","type":"User","site_admin":false},"created_at":"2015-04-24T17:34:49Z","updated_at":"2015-04-24T17:34:49Z","body":"The [mailing list post is here](http://www.cs.nyu.edu/pipermail/smt-lib/2015/000878.html)"}}