{"action":"closed","issue":{"url":"https://api.github.com/repos/LeventErkok/sbv/issues/75","labels_url":"https://api.github.com/repos/LeventErkok/sbv/issues/75/labels{/name}","comments_url":"https://api.github.com/repos/LeventErkok/sbv/issues/75/comments","events_url":"https://api.github.com/repos/LeventErkok/sbv/issues/75/events","html_url":"https://github.com/LeventErkok/sbv/issues/75","id":15595643,"number":75,"title":"Arrays with boolean target types","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":[{"url":"https://api.github.com/repos/LeventErkok/sbv/labels/Bug","name":"Bug","color":"ededed"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2013-06-15T19:08:36Z","updated_at":"2015-04-13T03:54:47Z","closed_at":"2015-04-13T03:54:47Z","body":"The QF_BV logic doesn't support arrays with target element of \"Bool\"'s, so we end up with:\r\n\r\n\r\n    Prelude Data.SBV> prove $ \\x -> readArray (x::SArray Word8 Bool) (0::SWord8)\r\n    *** An error occurred.\r\n    ***  Failed to complete the call to z3\r\n    ***  Executable   : \"/usr/local/bin/z3\"\r\n    ***  Options      : -in -smt2\r\n    ***  Exit code    : 1\r\n    ***  Solver output:\r\n    ***  ==============================================================================\r\n    ***  (error \"line 17 column 50: logic supports only arrays from bitvectors to bitvectors\")\r\n    ***  (error \"line 22 column 22: unknown constant array_0\")\r\n    ***  sat\r\n    ***  ==============================================================================\r\n\r\nIt'd be good to recognize this and reject early.\r\n\r\nNote that this is a problem with both the SMT-Lib1 and SMT-Lib2 backends."}}