{"action":"opened","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/17","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/17/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/17/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/17/events","html_url":"https://github.com/Z3Prover/z3/issues/17","id":65105161,"number":17,"title":"Bug in either FP conversion or addition","user":{"login":"LeventErkok","id":549449,"avatar_url":"https://avatars.githubusercontent.com/u/549449?v=3","gravatar_id":"","url":"https://api.github.com/users/LeventErkok","html_url":"https://github.com/LeventErkok","followers_url":"https://api.github.com/users/LeventErkok/followers","following_url":"https://api.github.com/users/LeventErkok/following{/other_user}","gists_url":"https://api.github.com/users/LeventErkok/gists{/gist_id}","starred_url":"https://api.github.com/users/LeventErkok/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/LeventErkok/subscriptions","organizations_url":"https://api.github.com/users/LeventErkok/orgs","repos_url":"https://api.github.com/users/LeventErkok/repos","events_url":"https://api.github.com/users/LeventErkok/events{/privacy}","received_events_url":"https://api.github.com/users/LeventErkok/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-03-29T23:03:20Z","updated_at":"2015-03-29T23:03:20Z","closed_at":null,"body":"This is on the unstable branch.\r\n\r\nThe following benchmark is essentially asking Z3 to compute the addition of the following two numbers:\r\n\r\n```\r\n   15749125 / 64\r\n   268632143 / 1024\r\n```\r\n\r\nrepresented as a single-precision floating point numbers.\r\n\r\nWith `roundNearestTiesToEven`, these numbers in decimal are:\r\n\r\n```\r\n246080.08\r\n16255.999\r\n```\r\n\r\nSo, addition should produce \r\n\r\n```\r\n262336.06\r\n```\r\n\r\nBut it appears Z3 is producing a value that equals\r\n\r\n```\r\n2.1885552e-38\r\n```\r\n\r\nwhich is nowhere even close. I'm not sure if the bug is in the conversion of the constants, which I believe you recently modified, or in the actual `fp.add` routine.\r\n\r\nHere's the benchmark:\r\n\r\n```\r\n; Automatically generated by SBV. Do not edit.\r\n(set-option :produce-models true)\r\n(set-logic QF_FP)\r\n; --- uninterpreted sorts ---\r\n; --- literal constants ---\r\n(define-fun s_2 () Bool false)\r\n(define-fun s_1 () Bool true)\r\n(define-fun s1 () RoundingMode roundNearestTiesToEven)\r\n(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 15749125 64)))\r\n(define-fun s3 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 16646143 1024)))\r\n; --- skolem constants ---\r\n(declare-fun s0 () (_ FloatingPoint  8 24))\r\n; --- constant tables ---\r\n; --- skolemized tables ---\r\n; --- arrays ---\r\n; --- uninterpreted constants ---\r\n; --- user given axioms ---\r\n; --- formula ---\r\n(assert ; no quantifiers\r\n   (let ((s4 (fp.add s1 s2 s3)))\r\n   (let ((s5 (fp.eq s0 s4)))\r\n   s5)))\r\n(check-sat)\r\n(get-value (s0))\r\n``` \r\n\r\nZ3 responds:\r\n\r\n```\r\nsat\r\n((s0 (fp #b0 #x01 #b11011100101000000000100)))\r\n```\r\n\r\nwhich is the internal representation for `2.1885552E-38`"}}