{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1754","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1754/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1754/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1754/events","html_url":"https://github.com/Z3Prover/z3/issues/1754","id":341192547,"node_id":"MDU6SXNzdWUzNDExOTI1NDc=","number":1754,"title":"Bit-vector regression","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},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":11,"created_at":"2018-07-14T00:20:50Z","updated_at":"2018-09-06T04:48:08Z","closed_at":null,"author_association":"NONE","body":"The following query took about 13 seconds on my Mac, using z3 built about a week ago, correctly answering `unsat`. A fresh build of z3 seem to go on it forever:\r\n\r\n```\r\n(set-option :produce-models true)\r\n(set-logic ALL)\r\n(declare-fun s0 () Int)\r\n(define-fun s2 () Bool (<= 0 s0))\r\n(define-fun s4 () Bool (< s0 256))\r\n(define-fun s5 () Bool (and s2 s4))\r\n(define-fun s6 () Bool (not s5))\r\n(define-fun s7 () (_ BitVec 8) (let ((__a (mod s0 256))) (let ((__a0 (ite (= (mod __a 2) 0) #b0 #b1)) (__a1 (ite (= (mod (div __a 2) 2) 0) #b0 #b1)) (__a2 (ite (= (mod (div __a 4) 2) 0) #b0 #b1)) (__a3 (ite (= (mod (div __a 8) 2) 0) #b0 #b1)) (__a4 (ite (= (mod (div __a 16) 2) 0) #b0 #b1)) (__a5 (ite (= (mod (div __a 32) 2) 0) #b0 #b1)) (__a6 (ite (= (mod (div __a 64) 2) 0) #b0 #b1)) (__a7 (ite (= (mod (div __a 128) 2) 0) #b0 #b1))) (concat __a7 (concat __a6 (concat __a5 (concat __a4 (concat __a3 (concat __a2 (concat __a1 __a0))))))))))\r\n(define-fun s8 () Int (+ (ite (= ((_ extract 0 0) s7) #b1) 1 0) (ite (= ((_ extract 1 1) s7) #b1) 2 0) (ite (= ((_ extract 2 2) s7) #b1) 4 0) (ite (= ((_ extract 3 3) s7) #b1) 8 0) (ite (= ((_ extract 4 4) s7) #b1) 16 0) (ite (= ((_ extract 5 5) s7) #b1) 32 0) (ite (= ((_ extract 6 6) s7) #b1) 64 0) (ite (= ((_ extract 7 7) s7) #b1) 128 0)))\r\n(define-fun s9 () Bool (= s0 s8))\r\n(define-fun s10 () Bool (or s6 s9))\r\n(assert (not s10))\r\n(check-sat)\r\n```\r\n\r\nI'm pretty sure this got broken in the last few days; based on Travis CI output.\r\n\r\nThe benchmark is essentially proving that any integer between @0@ and @255@ can be converted to an 8-bit vector and back using the obvious translation. (Repeated division to obtain the bits, and then add the powers per each blasted one bit.)"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/418963445","html_url":"https://github.com/Z3Prover/z3/issues/1754#issuecomment-418963445","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/1754","id":418963445,"node_id":"MDEyOklzc3VlQ29tbWVudDQxODk2MzQ0NQ==","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-09-06T04:48:08Z","updated_at":"2018-09-06T04:48:08Z","author_association":"NONE","body":"@levnach @NikolajBjorner \r\n\r\nIn case it helps: I'd be happy to run my test-suite on it, if you make the change and put it on a branch."}}
{"actor":{"display_login":"LeventErkok"}}