{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1674","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1674/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1674/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1674/events","html_url":"https://github.com/Z3Prover/z3/issues/1674","id":330864687,"node_id":"MDU6SXNzdWUzMzA4NjQ2ODc=","number":1674,"title":"fp.max is no longer defined in latest version of z3","user":{"login":"migimunz","id":766913,"node_id":"MDQ6VXNlcjc2NjkxMw==","avatar_url":"https://avatars1.githubusercontent.com/u/766913?v=4","gravatar_id":"","url":"https://api.github.com/users/migimunz","html_url":"https://github.com/migimunz","followers_url":"https://api.github.com/users/migimunz/followers","following_url":"https://api.github.com/users/migimunz/following{/other_user}","gists_url":"https://api.github.com/users/migimunz/gists{/gist_id}","starred_url":"https://api.github.com/users/migimunz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/migimunz/subscriptions","organizations_url":"https://api.github.com/users/migimunz/orgs","repos_url":"https://api.github.com/users/migimunz/repos","events_url":"https://api.github.com/users/migimunz/events{/privacy}","received_events_url":"https://api.github.com/users/migimunz/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-06-09T08:04:51Z","updated_at":"2018-06-13T01:51:27Z","closed_at":"2018-06-11T08:12:45Z","author_association":"NONE","body":"Hi,\r\n\r\nfp.max no longer seems to be defined, and z3 interprets it as an unspecified uninterpreted function. The following program:\r\n\r\n```\r\n(set-logic QF_FP)\r\n(declare-fun a ()(_ FloatingPoint 4 12))\r\n(assert (fp.eq (fp.max a a) (fp.max a a)))\r\n(check-sat)\r\n(get-model)\r\n```\r\nshould just produce a model for a. However, the version from master produces the following model:\r\n\r\n```\r\n(model \r\n  (define-fun a () (_ FloatingPoint 4 12)\r\n    (_ +zero 4 12))\r\n  (define-fun fp.max ((x!0 (_ FloatingPoint 4 12)) (x!1 (_ FloatingPoint 4 12))) (_ FloatingPoint\r\n     4\r\n     12)\r\n    (_ +zero 4 12))\r\n)\r\n```\r\n"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/396787993","html_url":"https://github.com/Z3Prover/z3/issues/1674#issuecomment-396787993","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/1674","id":396787993,"node_id":"MDEyOklzc3VlQ29tbWVudDM5Njc4Nzk5Mw==","user":{"login":"LeventErkok","id":549449,"node_id":"MDQ6VXNlcjU0OTQ0OQ==","avatar_url":"https://avatars0.githubusercontent.com/u/549449?v=4","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},"created_at":"2018-06-13T01:51:27Z","updated_at":"2018-06-13T01:51:27Z","author_association":"NONE","body":"@wintersteiger \r\n\r\nI thought the parameter `hi_fp_unspecified` can be used to control the behavior of this, but a few experiments suggest that is not the case: \r\n\r\nhttps://github.com/Z3Prover/z3/blob/e8f4dd76c21b52460b6bd95487183aea88749ce0/src/ast/fpa/fpa2bv_rewriter_params.pyg#L4\r\n\r\nIs this not the intended use case for this parameter?"}}
{"actor":{"display_login":"LeventErkok"}}