{"action":"created","issue":{"url":"https://api.github.com/repos/kframework/evm-semantics/issues/192","repository_url":"https://api.github.com/repos/kframework/evm-semantics","labels_url":"https://api.github.com/repos/kframework/evm-semantics/issues/192/labels{/name}","comments_url":"https://api.github.com/repos/kframework/evm-semantics/issues/192/comments","events_url":"https://api.github.com/repos/kframework/evm-semantics/issues/192/events","html_url":"https://github.com/kframework/evm-semantics/issues/192","id":314823859,"number":192,"title":"error \"line 25 column 394: Sorts K and NullStackOp are incompatible\"","user":{"login":"MrChico","id":8930559,"avatar_url":"https://avatars0.githubusercontent.com/u/8930559?v=4","gravatar_id":"","url":"https://api.github.com/users/MrChico","html_url":"https://github.com/MrChico","followers_url":"https://api.github.com/users/MrChico/followers","following_url":"https://api.github.com/users/MrChico/following{/other_user}","gists_url":"https://api.github.com/users/MrChico/gists{/gist_id}","starred_url":"https://api.github.com/users/MrChico/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MrChico/subscriptions","organizations_url":"https://api.github.com/users/MrChico/orgs","repos_url":"https://api.github.com/users/MrChico/repos","events_url":"https://api.github.com/users/MrChico/events{/privacy}","received_events_url":"https://api.github.com/users/MrChico/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2018-04-16T21:25:36Z","updated_at":"2018-04-25T22:42:49Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"We are trying to make the following circularity claim: https://github.com/dapphub/verified-smart-contracts/blob/dappsys/dappsys/exp-naive-circ-spec.k\r\nbut are given the following error\r\n<img width=\"764\" alt=\"screen shot 2018-04-16 at 15 19 07\" src=\"https://user-images.githubusercontent.com/8930559/38836115-52bca1ee-418a-11e8-9c41-71adc5ea9341.png\">\r\nDoes this error stem from something wrong in our spec? It looks like an error that has to do with the internal workings of K..."},"comment":{"url":"https://api.github.com/repos/kframework/evm-semantics/issues/comments/384456803","html_url":"https://github.com/kframework/evm-semantics/issues/192#issuecomment-384456803","issue_url":"https://api.github.com/repos/kframework/evm-semantics/issues/192","id":384456803,"user":{"login":"ehildenb","id":12721972,"avatar_url":"https://avatars0.githubusercontent.com/u/12721972?v=4","gravatar_id":"","url":"https://api.github.com/users/ehildenb","html_url":"https://github.com/ehildenb","followers_url":"https://api.github.com/users/ehildenb/followers","following_url":"https://api.github.com/users/ehildenb/following{/other_user}","gists_url":"https://api.github.com/users/ehildenb/gists{/gist_id}","starred_url":"https://api.github.com/users/ehildenb/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ehildenb/subscriptions","organizations_url":"https://api.github.com/users/ehildenb/orgs","repos_url":"https://api.github.com/users/ehildenb/repos","events_url":"https://api.github.com/users/ehildenb/events{/privacy}","received_events_url":"https://api.github.com/users/ehildenb/received_events","type":"User","site_admin":false},"created_at":"2018-04-25T22:42:48Z","updated_at":"2018-04-25T22:42:48Z","author_association":"COLLABORATOR","body":"@MrChico I'm trying some other optimizations on another branch (just local for now), but I'm running into a (potentially) similar issue. Can you try changing `<program> ... DEST |-> OP ... </program>` to `<program> ... DEST |-> OP:OpCode ... </program>` for both the `JUMP` and `JUMPI` cases of your semantics of `#badJumpDest?` and see if it changes the behavior on this example?"}}
{"actor":{"display_login":"ehildenb"}}