{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1957","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1957/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1957/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1957/events","html_url":"https://github.com/Z3Prover/z3/issues/1957","id":382838795,"node_id":"MDU6SXNzdWUzODI4Mzg3OTU=","number":1957,"title":"int.to.str cannot show unsat","user":{"login":"MontyThibault","id":1238401,"node_id":"MDQ6VXNlcjEyMzg0MDE=","avatar_url":"https://avatars1.githubusercontent.com/u/1238401?v=4","gravatar_id":"","url":"https://api.github.com/users/MontyThibault","html_url":"https://github.com/MontyThibault","followers_url":"https://api.github.com/users/MontyThibault/followers","following_url":"https://api.github.com/users/MontyThibault/following{/other_user}","gists_url":"https://api.github.com/users/MontyThibault/gists{/gist_id}","starred_url":"https://api.github.com/users/MontyThibault/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MontyThibault/subscriptions","organizations_url":"https://api.github.com/users/MontyThibault/orgs","repos_url":"https://api.github.com/users/MontyThibault/repos","events_url":"https://api.github.com/users/MontyThibault/events{/privacy}","received_events_url":"https://api.github.com/users/MontyThibault/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-11-20T20:37:29Z","updated_at":"2018-11-20T23:50:49Z","closed_at":null,"author_association":"NONE","body":"This example leads to an infinite hang.\r\n\r\n```\r\n(declare-const n Int)\r\n\r\n(assert (= (int.to.str n) \"asdf\"))\r\n\r\n(check-sat)\r\n```"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/440471049","html_url":"https://github.com/Z3Prover/z3/issues/1957#issuecomment-440471049","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/1957","id":440471049,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0MDQ3MTA0OQ==","user":{"login":"DvonHolten","id":41451972,"node_id":"MDQ6VXNlcjQxNDUxOTcy","avatar_url":"https://avatars3.githubusercontent.com/u/41451972?v=4","gravatar_id":"","url":"https://api.github.com/users/DvonHolten","html_url":"https://github.com/DvonHolten","followers_url":"https://api.github.com/users/DvonHolten/followers","following_url":"https://api.github.com/users/DvonHolten/following{/other_user}","gists_url":"https://api.github.com/users/DvonHolten/gists{/gist_id}","starred_url":"https://api.github.com/users/DvonHolten/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DvonHolten/subscriptions","organizations_url":"https://api.github.com/users/DvonHolten/orgs","repos_url":"https://api.github.com/users/DvonHolten/repos","events_url":"https://api.github.com/users/DvonHolten/events{/privacy}","received_events_url":"https://api.github.com/users/DvonHolten/received_events","type":"User","site_admin":false},"created_at":"2018-11-20T23:50:49Z","updated_at":"2018-11-20T23:50:49Z","author_association":"NONE","body":"is it really 'inifinite' ? or just 'very long' ? it seems, it is busy iterating through all the integers - there are quite a few of them - to find a value, which is converted to a string, equal to \"asdf\". I think, Z3 has no idea about the fact that _no_ converted Int would result in \"asdf\""}}
{"actor":{"display_login":"DvonHolten"}}