{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/66","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/66/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/66/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/66/events","html_url":"https://github.com/Z3Prover/z3/issues/66","id":72824769,"number":66,"title":"Not sure if it's an error, but this is not working","user":{"login":"Rumata888","id":4798775,"avatar_url":"https://avatars.githubusercontent.com/u/4798775?v=3","gravatar_id":"","url":"https://api.github.com/users/Rumata888","html_url":"https://github.com/Rumata888","followers_url":"https://api.github.com/users/Rumata888/followers","following_url":"https://api.github.com/users/Rumata888/following{/other_user}","gists_url":"https://api.github.com/users/Rumata888/gists{/gist_id}","starred_url":"https://api.github.com/users/Rumata888/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Rumata888/subscriptions","organizations_url":"https://api.github.com/users/Rumata888/orgs","repos_url":"https://api.github.com/users/Rumata888/repos","events_url":"https://api.github.com/users/Rumata888/events{/privacy}","received_events_url":"https://api.github.com/users/Rumata888/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-05-03T15:57:49Z","updated_at":"2015-05-03T15:58:52Z","closed_at":"2015-05-03T15:58:52Z","body":"from symbolic.args import *\r\n@symbolic(a=0xdeaddeaddeaddead,b=beefbeefbeefbeef)\r\n\r\ndef expandKey(a,b):\r\n\ti=0;\r\n\tpasskeyn=[a,b]\r\n\t\r\n\texpandedkey=[]\r\n\twhile i<6:\r\n\t\texpandedkey=expandedkey+passkeyn\r\n\t\ti=i+1\r\n\t\tv1=passkeyn[0]\r\n\t\tv2=passkeyn[1]\r\n\t\tv3=(v1>>0x30)|(((v1>>0x20)&0xffff)<<0x10)|(((v1>>0x10)&0xffff)<<0x20)|((v1&0xffff)<<0x30)\r\n\t\tv4=(v2>>0x30)|(((v2>>0x20)&0xffff)<<0x10)|(((v2>>0x10)&0xffff)<<0x20)|((v2&0xffff)<<0x30)\r\n\t\tv5 = ((v4 & 0xFFFFFF8000000000) >> 39) | ((v3 << 25)&0xffffffffffffffff);\r\n\t\tv6 = ((v3 & 0xFFFFFF8000000000) >> 39) | ((v4 << 25)&0xffffffffffffffff);\r\n\t\tv1=(v5>>0x30)|(((v5>>0x20)&0xffff)<<0x10)|(((v5>>0x10)&0xffff)<<0x20)|(((v4 & 0xFFFFFF8000000000) >> 39)<<0x30)\r\n\t\tv2=(v6>>0x30)|(((v6>>32)&0xffff)<<0x10)|(((v6>>0x10)&0xffff)<<0x20)|(((v3 & 0xFFFFFF8000000000) >> 39)<<0x30)\r\n\t\tpasskeyn=[v1,v2]\r\n\texpandedkey=expandedkey+passkeyn\r\n\tif expandedkey==[16045725885737590445, 13758425323549998831, 7044313620519854103485, 8215411798635391606653, 8245388070021240879798, 3384596836810669685695, 9287860625795901259255, 4527376222128629444341, 4093654381503457390331, 4647353382867023162077, 8665057901351565392853, 8816957627389395711965, 6783497306152038280055, 9291067819851303074799]:\r\n\t\treturn 1\r\n\treturn 2\r\n"}}