{"action":"created","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/113","labels_url":"https://api.github.com/repos/newca12/gapt/issues/113/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/113/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/113/events","html_url":"https://github.com/newca12/gapt/issues/113","id":55588789,"number":113,"title":"Get rid of position occurrences","user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/newca12/gapt/labels/1%20star","name":"1 star","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/bug","name":"bug","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Component-LogicalDataStructures","name":"Component-LogicalDataStructures","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/imported","name":"imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-Medium","name":"Priority-Medium","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":9,"created_at":"2015-01-27T08:24:31Z","updated_at":"2015-01-27T08:25:17Z","closed_at":null,"body":"_From [fra...@gmail.com](https://code.google.com/u/108596877348066494139/) on February 17, 2011 15:27:50_\n\nAn issue came up when using position occurrences with the AndEquivalenceRule1 of SLK. The AndEquivalenceRule1 is written in such a way that it checks whether the auxiliary formula occurs in the antecedent or in the succedent, and changes things accordingly.\r\n\r\nBut the position occurrences only distinguish the place in the antecedent or the succedent, but not antecedent/succedent. Hence the rule was applied incorrectly. In particular, it can be that for two position occurrences p1, p2, we have p1 == p2 but p1.formula != p2.formula. I am rather sure that this is undesirable.\r\n\r\nA test reproducing this issue can be found in SLKTest.scala.\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=113_"},"comment":{"url":"https://api.github.com/repos/newca12/gapt/issues/comments/71608007","html_url":"https://github.com/newca12/gapt/issues/113#issuecomment-71608007","issue_url":"https://api.github.com/repos/newca12/gapt/issues/113","id":71608007,"user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"created_at":"2015-01-27T08:25:17Z","updated_at":"2015-01-27T08:25:17Z","body":"_From [bruno...@gmail.com](https://code.google.com/u/105016684496602932564/) on October 06, 2011 05:51:48_\n\nCvetan: please do something with the commented out code that still uses PointerOccurrence in \"profile.scala\".\n\n**Status:** Fixed  \n"}}