{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/432","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/432/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/432/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/432/events","html_url":"https://github.com/Z3Prover/z3/issues/432","id":131503165,"number":432,"title":"Weird behaviour of \"+\" operation over BitVectors","user":{"login":"dennis714","id":2044088,"avatar_url":"https://avatars.githubusercontent.com/u/2044088?v=3","gravatar_id":"","url":"https://api.github.com/users/dennis714","html_url":"https://github.com/dennis714","followers_url":"https://api.github.com/users/dennis714/followers","following_url":"https://api.github.com/users/dennis714/following{/other_user}","gists_url":"https://api.github.com/users/dennis714/gists{/gist_id}","starred_url":"https://api.github.com/users/dennis714/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dennis714/subscriptions","organizations_url":"https://api.github.com/users/dennis714/orgs","repos_url":"https://api.github.com/users/dennis714/repos","events_url":"https://api.github.com/users/dennis714/events{/privacy}","received_events_url":"https://api.github.com/users/dennis714/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-02-04T23:16:06Z","updated_at":"2016-02-05T08:07:20Z","closed_at":"2016-02-05T08:07:19Z","body":"Not sure if I hit a bug in Z3 or Z3Py (4.4.2) or I just miss something.\r\nHere is a working example.\r\nI coded Sudoku problem as an example.\r\nHow would I detect if all 9 numbers in row are unique?\r\nYes, there is \"Distinct\", but before I got to know about it, I made this equation:\r\n\r\n`1<<cell1 | 1<<cell2 ... | 1<<cell9 == 0b1111111110 (binary)`\r\n\r\nSo if 9 input cells has 9 unique numbers, the result of this expression should be\r\n0b1111111110 (all cells has numbers in rage of 1..9, hence the last zero bit).\r\n\r\nSo far so good, I've encoded this and it works very well: http://pastebin.com/arFLmbeb\r\nNow what is weird is that if I replace OR operation with PLUS...\r\n\r\n`1<<cell1 + 1<<cell2 ... + 1<<cell9 == 0b1111111110 (binary)`\r\n\r\n... it doesn't works, although, mathematically, everything should work: http://pastebin.com/AtAwk3tx\r\n\r\nDo I miss something? Should I use some specific tactic?\r\n\r\nThanks in advance!"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/180244238","html_url":"https://github.com/Z3Prover/z3/issues/432#issuecomment-180244238","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/432","id":180244238,"user":{"login":"NikolajBjorner","id":3085284,"avatar_url":"https://avatars.githubusercontent.com/u/3085284?v=3","gravatar_id":"","url":"https://api.github.com/users/NikolajBjorner","html_url":"https://github.com/NikolajBjorner","followers_url":"https://api.github.com/users/NikolajBjorner/followers","following_url":"https://api.github.com/users/NikolajBjorner/following{/other_user}","gists_url":"https://api.github.com/users/NikolajBjorner/gists{/gist_id}","starred_url":"https://api.github.com/users/NikolajBjorner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/NikolajBjorner/subscriptions","organizations_url":"https://api.github.com/users/NikolajBjorner/orgs","repos_url":"https://api.github.com/users/NikolajBjorner/repos","events_url":"https://api.github.com/users/NikolajBjorner/events{/privacy}","received_events_url":"https://api.github.com/users/NikolajBjorner/received_events","type":"User","site_admin":false},"created_at":"2016-02-05T08:07:19Z","updated_at":"2016-02-05T08:07:19Z","body":"The precedence of + is higher than <<, which is higher than |. \r\nSee https://docs.python.org/2/reference/expressions.html\r\nSo add parentheses around 1<<cell_i expressions and your script will give the same results.\r\nYou already have parentheses around the first two groups of shift expressions, but the last one would require parentheses before you get an answer (the constraints are unsat if you change | to + without the parentheses).\r\n"}}