{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/215","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/215/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/215/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/215/events","html_url":"https://github.com/Z3Prover/z3/issues/215","id":105664723,"number":215,"title":"Assertion Violation Involving Floating Point Multiplication","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":[{"url":"https://api.github.com/repos/Z3Prover/z3/labels/bug","name":"bug","color":"fc2929"}],"state":"open","locked":false,"assignee":{"login":"wintersteiger","id":10155819,"avatar_url":"https://avatars.githubusercontent.com/u/10155819?v=3","gravatar_id":"","url":"https://api.github.com/users/wintersteiger","html_url":"https://github.com/wintersteiger","followers_url":"https://api.github.com/users/wintersteiger/followers","following_url":"https://api.github.com/users/wintersteiger/following{/other_user}","gists_url":"https://api.github.com/users/wintersteiger/gists{/gist_id}","starred_url":"https://api.github.com/users/wintersteiger/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wintersteiger/subscriptions","organizations_url":"https://api.github.com/users/wintersteiger/orgs","repos_url":"https://api.github.com/users/wintersteiger/repos","events_url":"https://api.github.com/users/wintersteiger/events{/privacy}","received_events_url":"https://api.github.com/users/wintersteiger/received_events","type":"User","site_admin":false},"milestone":null,"comments":3,"created_at":"2015-09-09T19:11:23Z","updated_at":"2015-09-09T20:22:45Z","closed_at":null,"body":"On the `unstable` branch at commit 44105b7aeb8ec6e85dfba23321eaa6838695d1f3, if I run Z3 with no command-line options on the following input:\r\n\r\n```\r\n(set-logic QF_FP)\r\n(simplify (fp.mul RNE (fp #b1 #b110 #b1) (fp #b0 #b100 #b0)))\r\n```\r\n\r\n...then Z3 crashes with the following output:\r\n\r\n```\r\nASSERTION VIOLATION\r\nFile: ../src/util/mpf.cpp\r\nLine: 1736\r\nTINY || (m_mpz_manager.ge(o.significand, p_sig))\r\n```"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/139035479","html_url":"https://github.com/Z3Prover/z3/issues/215#issuecomment-139035479","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/215","id":139035479,"user":{"login":"wintersteiger","id":10155819,"avatar_url":"https://avatars.githubusercontent.com/u/10155819?v=3","gravatar_id":"","url":"https://api.github.com/users/wintersteiger","html_url":"https://github.com/wintersteiger","followers_url":"https://api.github.com/users/wintersteiger/followers","following_url":"https://api.github.com/users/wintersteiger/following{/other_user}","gists_url":"https://api.github.com/users/wintersteiger/gists{/gist_id}","starred_url":"https://api.github.com/users/wintersteiger/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/wintersteiger/subscriptions","organizations_url":"https://api.github.com/users/wintersteiger/orgs","repos_url":"https://api.github.com/users/wintersteiger/repos","events_url":"https://api.github.com/users/wintersteiger/events{/privacy}","received_events_url":"https://api.github.com/users/wintersteiger/received_events","type":"User","site_admin":false},"created_at":"2015-09-09T20:22:45Z","updated_at":"2015-09-09T20:22:45Z","body":"Yes, that is correct, this is a Z3 limitation, mainly because it's untested and it's not been needed so far. Most operators would still work, but there may be a few cases for which input normalization is impossible, as far as I remember. "}}