{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/91","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/91/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/91/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/91/events","html_url":"https://github.com/Z3Prover/z3/issues/91","id":76957714,"number":91,"title":"fp.rem (-0) (0.5) should be -0, but Z3 produces +0","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":"closed","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":4,"created_at":"2015-05-16T06:15:16Z","updated_at":"2015-05-20T00:16:38Z","closed_at":"2015-05-19T17:58:34Z","body":"Happy to provide an SMTLib benchmark if that'd help; but the subject says it all. The semantics of fp.rem is such that the output should follow the sign of the first argument, but Z3 is violating that in this particular case. Note that this is similar to (but not the same as) #80 at it pertains to the smt-lib semantics of fp.rem (and the corresponding C function fmodf.)"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/103703047","html_url":"https://github.com/Z3Prover/z3/issues/91#issuecomment-103703047","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/91","id":103703047,"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},"created_at":"2015-05-20T00:16:38Z","updated_at":"2015-05-20T00:16:38Z","body":"Fantastic, it works as expected now. I belive #80 is the only remaining one on fp.rem semantics that I have a gripe with. Did you get a chance to look at that one?"}}