{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/766","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/766/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/766/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/766/events","html_url":"https://github.com/Z3Prover/z3/issues/766","id":185109769,"number":766,"title":"Sort mismatch at argument #1 for function (declare-fun = (Real Real) Bool)","user":{"login":"cocreature","id":1313584,"avatar_url":"https://avatars2.githubusercontent.com/u/1313584?v=4","gravatar_id":"","url":"https://api.github.com/users/cocreature","html_url":"https://github.com/cocreature","followers_url":"https://api.github.com/users/cocreature/followers","following_url":"https://api.github.com/users/cocreature/following{/other_user}","gists_url":"https://api.github.com/users/cocreature/gists{/gist_id}","starred_url":"https://api.github.com/users/cocreature/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cocreature/subscriptions","organizations_url":"https://api.github.com/users/cocreature/orgs","repos_url":"https://api.github.com/users/cocreature/repos","events_url":"https://api.github.com/users/cocreature/events{/privacy}","received_events_url":"https://api.github.com/users/cocreature/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":{"login":"kenmcmil","id":8010069,"avatar_url":"https://avatars1.githubusercontent.com/u/8010069?v=4","gravatar_id":"","url":"https://api.github.com/users/kenmcmil","html_url":"https://github.com/kenmcmil","followers_url":"https://api.github.com/users/kenmcmil/followers","following_url":"https://api.github.com/users/kenmcmil/following{/other_user}","gists_url":"https://api.github.com/users/kenmcmil/gists{/gist_id}","starred_url":"https://api.github.com/users/kenmcmil/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kenmcmil/subscriptions","organizations_url":"https://api.github.com/users/kenmcmil/orgs","repos_url":"https://api.github.com/users/kenmcmil/repos","events_url":"https://api.github.com/users/kenmcmil/events{/privacy}","received_events_url":"https://api.github.com/users/kenmcmil/received_events","type":"User","site_admin":false},"assignees":[{"login":"kenmcmil","id":8010069,"avatar_url":"https://avatars1.githubusercontent.com/u/8010069?v=4","gravatar_id":"","url":"https://api.github.com/users/kenmcmil","html_url":"https://github.com/kenmcmil","followers_url":"https://api.github.com/users/kenmcmil/followers","following_url":"https://api.github.com/users/kenmcmil/following{/other_user}","gists_url":"https://api.github.com/users/kenmcmil/gists{/gist_id}","starred_url":"https://api.github.com/users/kenmcmil/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kenmcmil/subscriptions","organizations_url":"https://api.github.com/users/kenmcmil/orgs","repos_url":"https://api.github.com/users/kenmcmil/repos","events_url":"https://api.github.com/users/kenmcmil/events{/privacy}","received_events_url":"https://api.github.com/users/kenmcmil/received_events","type":"User","site_admin":false}],"milestone":null,"comments":1,"created_at":"2016-10-25T12:57:00Z","updated_at":"2018-05-25T18:04:25Z","closed_at":"2018-05-25T18:04:25Z","author_association":"CONTRIBUTOR","body":"When running z3 build at commit fefd00aa4980dd7410f2315a6e3033c349f6b266 on the input file shown below, I get the error message:\n\n```\n(error \"query failed: Sort mismatch at argument #1 for function (declare-fun = (Real Real) Bool) supplied sort is Int\")\n```\n\nJudging by the error messages I received for other input files it seems like `duality` doesn’t support mixing reals and integers, so this is probably just a confusing error message rather than an actual bug. This example doesn’t use `=` anywhere. (I removed everything possible from the example so it’s pretty meaningless at this point).\n\n``` smt\n(set-logic HORN)\n(set-option :fixedpoint.engine duality)\n(set-option :int-real-coercions false)\n(declare-var HEAP (Array Int Int))\n(declare-var a Int)\n(declare-var i Int)\n(declare-var n Int)\n(declare-var s Real)\n(declare-rel QUERY ())\n(declare-rel Inv (Int Int Int Real (Array Int Int)))\n(rule\n (=> (not (<= n 0))\n     (Inv 0 a n 0.0 HEAP)))\n(rule\n (=> (and (Inv i a n s HEAP) (>= i n))\n     QUERY))\n(rule\n (=> (Inv i a n s HEAP)\n     (Inv i a n (/ (to_real (select HEAP a)) (to_real n)) HEAP)))\n(query QUERY)\n```\n"}}
{"actor":{"display_login":"NikolajBjorner"}}