{"action":"opened","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/78","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/78/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/78/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/78/events","html_url":"https://github.com/Z3Prover/z3/issues/78","id":74213219,"number":78,"title":"Cannot easily cast Bool to Int in Z3py","user":{"login":"dbueno","id":24254,"avatar_url":"https://avatars.githubusercontent.com/u/24254?v=3","gravatar_id":"","url":"https://api.github.com/users/dbueno","html_url":"https://github.com/dbueno","followers_url":"https://api.github.com/users/dbueno/followers","following_url":"https://api.github.com/users/dbueno/following{/other_user}","gists_url":"https://api.github.com/users/dbueno/gists{/gist_id}","starred_url":"https://api.github.com/users/dbueno/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dbueno/subscriptions","organizations_url":"https://api.github.com/users/dbueno/orgs","repos_url":"https://api.github.com/users/dbueno/repos","events_url":"https://api.github.com/users/dbueno/events{/privacy}","received_events_url":"https://api.github.com/users/dbueno/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-05-08T03:26:40Z","updated_at":"2015-05-08T03:26:40Z","closed_at":null,"body":"It should be easy to cast a bool to an int (just make True -> 1 and False -> 0). But it doesn't work because BoolRef.is_int() isn't implemented. Here's the example.\r\n\r\n```\r\nIn [1]: from z3 import *\r\nIn [2]: IntSort().cast(BoolVal(True))\r\n---------------------------------------------------------------------------\r\nAttributeError                            Traceback (most recent call last)\r\n<ipython-input-2-71a42de2b38a> in <module>()\r\n----> 1 IntSort().cast(BoolVal(True))\r\n\r\n/Users/me/sw/inst/z3/build/z3.pyc in cast(self, val)\r\n   1899             if self.eq(val_s):\r\n   1900                 return val\r\n-> 1901             if val_s.is_int() and self.is_real():\r\n   1902                 return ToReal(val)\r\n   1903             if __debug__:\r\n\r\nAttributeError: BoolSortRef instance has no attribute 'is_int'\r\n```"}}