{"action":"created","issue":{"url":"https://api.github.com/repos/0vercl0k/z3-playground/issues/2","labels_url":"https://api.github.com/repos/0vercl0k/z3-playground/issues/2/labels{/name}","comments_url":"https://api.github.com/repos/0vercl0k/z3-playground/issues/2/comments","events_url":"https://api.github.com/repos/0vercl0k/z3-playground/issues/2/events","html_url":"https://github.com/0vercl0k/z3-playground/issues/2","id":54978098,"number":2,"title":"Hi! may I have a question?","user":{"login":"hdarwin","id":4065436,"avatar_url":"https://avatars.githubusercontent.com/u/4065436?v=3","gravatar_id":"","url":"https://api.github.com/users/hdarwin","html_url":"https://github.com/hdarwin","followers_url":"https://api.github.com/users/hdarwin/followers","following_url":"https://api.github.com/users/hdarwin/following{/other_user}","gists_url":"https://api.github.com/users/hdarwin/gists{/gist_id}","starred_url":"https://api.github.com/users/hdarwin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/hdarwin/subscriptions","organizations_url":"https://api.github.com/users/hdarwin/orgs","repos_url":"https://api.github.com/users/hdarwin/repos","events_url":"https://api.github.com/users/hdarwin/events{/privacy}","received_events_url":"https://api.github.com/users/hdarwin/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-01-21T05:02:34Z","updated_at":"2015-01-21T10:51:28Z","closed_at":"2015-01-21T10:51:01Z","body":"can you give hint me why case2 doesn't work??\r\n\r\n\r\n\r\nroot@ubuntu:/root# cat test.py\r\n#!/usr/bin/env python\r\nfrom z3 import *\r\n#CASE1\r\nkey = BitVec(\"tag\", 32)\r\nsolve(RotateRight(key, 7) == 0x9a000000)\r\n\r\n#CASE2\r\ntag = BitVec(\"tag\", 32)\r\nkey = BitVecVal(0, 32)\r\nkey = key + tag\r\nRotateRight(key, 7)\r\nsolve(key == 0x9a000000, tag == 77)\r\nroot@ubuntu:/root# ./test.py \r\n[tag = 77]\r\nno solution"},"comment":{"url":"https://api.github.com/repos/0vercl0k/z3-playground/issues/comments/70818006","html_url":"https://github.com/0vercl0k/z3-playground/issues/2#issuecomment-70818006","issue_url":"https://api.github.com/repos/0vercl0k/z3-playground/issues/2","id":70818006,"user":{"login":"0vercl0k","id":1476421,"avatar_url":"https://avatars.githubusercontent.com/u/1476421?v=3","gravatar_id":"","url":"https://api.github.com/users/0vercl0k","html_url":"https://github.com/0vercl0k","followers_url":"https://api.github.com/users/0vercl0k/followers","following_url":"https://api.github.com/users/0vercl0k/following{/other_user}","gists_url":"https://api.github.com/users/0vercl0k/gists{/gist_id}","starred_url":"https://api.github.com/users/0vercl0k/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/0vercl0k/subscriptions","organizations_url":"https://api.github.com/users/0vercl0k/orgs","repos_url":"https://api.github.com/users/0vercl0k/repos","events_url":"https://api.github.com/users/0vercl0k/events{/privacy}","received_events_url":"https://api.github.com/users/0vercl0k/received_events","type":"User","site_admin":false},"created_at":"2015-01-21T10:51:28Z","updated_at":"2015-01-21T10:51:28Z","body":"No worries :-)\r\n\r\n2015-01-21 10:51 GMT+00:00 hdarwin <notifications@github.com>:\r\n\r\n> ahha! thanks a lot! and thanks for your secday presetation! [image: :+1:]\r\n>\r\n> —\r\n> Reply to this email directly or view it on GitHub\r\n> <https://github.com/0vercl0k/z3-playground/issues/2#issuecomment-70817946>\r\n> .\r\n>"}}