{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1846","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1846/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1846/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1846/events","html_url":"https://github.com/Z3Prover/z3/issues/1846","id":364044750,"node_id":"MDU6SXNzdWUzNjQwNDQ3NTA=","number":1846,"title":"How to properly do an integer to string conversion?","user":{"login":"bj2015","id":23193107,"node_id":"MDQ6VXNlcjIzMTkzMTA3","avatar_url":"https://avatars0.githubusercontent.com/u/23193107?v=4","gravatar_id":"","url":"https://api.github.com/users/bj2015","html_url":"https://github.com/bj2015","followers_url":"https://api.github.com/users/bj2015/followers","following_url":"https://api.github.com/users/bj2015/following{/other_user}","gists_url":"https://api.github.com/users/bj2015/gists{/gist_id}","starred_url":"https://api.github.com/users/bj2015/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bj2015/subscriptions","organizations_url":"https://api.github.com/users/bj2015/orgs","repos_url":"https://api.github.com/users/bj2015/repos","events_url":"https://api.github.com/users/bj2015/events{/privacy}","received_events_url":"https://api.github.com/users/bj2015/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-09-26T13:59:17Z","updated_at":"2018-09-26T15:04:56Z","closed_at":null,"author_association":"NONE","body":"I use Z3's String type and often convert integers to insert them into strings.\r\n\r\nHowever, both built-in functions `str.from-int` and `int.to.str` do not support negative integers. So I built the following user-defined function to remove this restriction:\r\n\r\n```\r\n(define-fun intToStr ((i Int)) String (ite (> i 0) (int.to.str i) (str.++ \"-\" (int.to.str (- 0 i)))))\r\n```\r\n\r\nWhile this seems to work, I noticed that Z3 returns \"unknown\" even on completely trivial problems like\r\n\r\n```\r\n(set-option :produce-unsat-cores true)\r\n\r\n(define-fun intToStr ((i Int)) String (ite (> i 0) (int.to.str i) (str.++ \"-\" (int.to.str (- 0 i)))))\r\n\r\n(declare-const t Int)\r\n(declare-const s String)\r\n\r\n(assert (! (= t 42) :named a))\r\n(assert (= s (intToStr t)))\r\n\r\n(check-sat)\r\n```\r\n\r\nHence my question is:\r\nAm I doing something wrong here? Is there a better way to convert integers into strings? maybe even one that does not cause Z3 headaches?\r\n\r\nWould it be possible to simply support negative numbers in int.to.str so that the above routine becomes unneccessary?"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/424750666","html_url":"https://github.com/Z3Prover/z3/issues/1846#issuecomment-424750666","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/1846","id":424750666,"node_id":"MDEyOklzc3VlQ29tbWVudDQyNDc1MDY2Ng==","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-09-26T15:04:56Z","updated_at":"2018-09-26T15:04:56Z","author_association":"NONE","body":"your example works in rise4fun (version 4.5.1) . do you have another one ?"}}
{"actor":{"display_login":"DvonHolten"}}