{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/220","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/220/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/220/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/220/events","html_url":"https://github.com/Z3Prover/z3/issues/220","id":106894997,"number":220,"title":"Possible Bug in fp.sqrt","user":{"login":"kyledewey","id":992190,"avatar_url":"https://avatars.githubusercontent.com/u/992190?v=3","gravatar_id":"","url":"https://api.github.com/users/kyledewey","html_url":"https://github.com/kyledewey","followers_url":"https://api.github.com/users/kyledewey/followers","following_url":"https://api.github.com/users/kyledewey/following{/other_user}","gists_url":"https://api.github.com/users/kyledewey/gists{/gist_id}","starred_url":"https://api.github.com/users/kyledewey/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kyledewey/subscriptions","organizations_url":"https://api.github.com/users/kyledewey/orgs","repos_url":"https://api.github.com/users/kyledewey/repos","events_url":"https://api.github.com/users/kyledewey/events{/privacy}","received_events_url":"https://api.github.com/users/kyledewey/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-09-17T01:26:57Z","updated_at":"2015-09-17T11:14:26Z","closed_at":"2015-09-17T11:14:26Z","body":"On the `unstable` branch, at commit 52df2224e94de0842281899449a58966698450f5, consider the following input:\r\n\r\n```\r\n(set-option :produce-models true)\r\n(set-logic QF_FP)\r\n(declare-fun x0 () Float32)\r\n\r\n; Floating point representation of -2\r\n(assert (= (fp.sqrt RNE (fp #b1 #b10000000 #b00000000000000000000000)) x0))\r\n\r\n(check-sat)\r\n(get-model)\r\n```\r\n\r\nZ3 states that this is `sat`, with a model that `x0` is `(_ -zero 8 24)`.  According to the IEEE standard, the square root of `-2` should be a quiet `NaN`, though this only suggests `NaN` is the correct result.  Looking at [the expected SMT-LIB semantics](http://www.philipp.ruemmer.org/publications/smt-fpa.pdf), I'm actually not sure what's supposed to happen here.  From the standard, assuming `E^-` is 0 (I'm not 100% sure it is here; this is unclear to me) then the second case shouldn't apply, as in this case the exponent is not zero.  The third case would be applicable, except that it bears the constraint that the mantissa must be greater than 0, and in this case the mantissa is zero.  As such, it looks to me like no cases apply, though I could very well be wrong.  Given that everything should be total, if no cases apply, then this is a bug in the standard itself (or I'm confused, which, again, is quite possible).\r\n\r\nIn any event, on a \"similar\" input of `2.5`, Z3 returns `NaN`, which seems to be due to the third case of the standard applying (`m` is greater than 0 in this situation).  For what it's worth, on an input of 2, MathSAT5 reports `NaN`.  If this isn't an issue in either the standard or Z3, I'll go ahead and report it to the MathSAT5 team."}}