{"action":"created","issue":{"url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/25","repository_url":"https://api.github.com/repos/sohah/VeritestingTransformations","labels_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/25/labels{/name}","comments_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/25/comments","events_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/25/events","html_url":"https://github.com/sohah/VeritestingTransformations/issues/25","id":374477004,"node_id":"MDU6SXNzdWUzNzQ0NzcwMDQ=","number":25,"title":"We think that PC should be unsat in SPF, but actually SPF concludes it is SAT.","user":{"login":"sohah","id":10510966,"node_id":"MDQ6VXNlcjEwNTEwOTY2","avatar_url":"https://avatars2.githubusercontent.com/u/10510966?v=4","gravatar_id":"","url":"https://api.github.com/users/sohah","html_url":"https://github.com/sohah","followers_url":"https://api.github.com/users/sohah/followers","following_url":"https://api.github.com/users/sohah/following{/other_user}","gists_url":"https://api.github.com/users/sohah/gists{/gist_id}","starred_url":"https://api.github.com/users/sohah/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sohah/subscriptions","organizations_url":"https://api.github.com/users/sohah/orgs","repos_url":"https://api.github.com/users/sohah/repos","events_url":"https://api.github.com/users/sohah/events{/privacy}","received_events_url":"https://api.github.com/users/sohah/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"vaibhavbsharma","id":5904279,"node_id":"MDQ6VXNlcjU5MDQyNzk=","avatar_url":"https://avatars1.githubusercontent.com/u/5904279?v=4","gravatar_id":"","url":"https://api.github.com/users/vaibhavbsharma","html_url":"https://github.com/vaibhavbsharma","followers_url":"https://api.github.com/users/vaibhavbsharma/followers","following_url":"https://api.github.com/users/vaibhavbsharma/following{/other_user}","gists_url":"https://api.github.com/users/vaibhavbsharma/gists{/gist_id}","starred_url":"https://api.github.com/users/vaibhavbsharma/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vaibhavbsharma/subscriptions","organizations_url":"https://api.github.com/users/vaibhavbsharma/orgs","repos_url":"https://api.github.com/users/vaibhavbsharma/repos","events_url":"https://api.github.com/users/vaibhavbsharma/events{/privacy}","received_events_url":"https://api.github.com/users/vaibhavbsharma/received_events","type":"User","site_admin":false},"assignees":[{"login":"vaibhavbsharma","id":5904279,"node_id":"MDQ6VXNlcjU5MDQyNzk=","avatar_url":"https://avatars1.githubusercontent.com/u/5904279?v=4","gravatar_id":"","url":"https://api.github.com/users/vaibhavbsharma","html_url":"https://github.com/vaibhavbsharma","followers_url":"https://api.github.com/users/vaibhavbsharma/followers","following_url":"https://api.github.com/users/vaibhavbsharma/following{/other_user}","gists_url":"https://api.github.com/users/vaibhavbsharma/gists{/gist_id}","starred_url":"https://api.github.com/users/vaibhavbsharma/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vaibhavbsharma/subscriptions","organizations_url":"https://api.github.com/users/vaibhavbsharma/orgs","repos_url":"https://api.github.com/users/vaibhavbsharma/repos","events_url":"https://api.github.com/users/vaibhavbsharma/events{/privacy}","received_events_url":"https://api.github.com/users/vaibhavbsharma/received_events","type":"User","site_admin":false},{"login":"sohah","id":10510966,"node_id":"MDQ6VXNlcjEwNTEwOTY2","avatar_url":"https://avatars2.githubusercontent.com/u/10510966?v=4","gravatar_id":"","url":"https://api.github.com/users/sohah","html_url":"https://github.com/sohah","followers_url":"https://api.github.com/users/sohah/followers","following_url":"https://api.github.com/users/sohah/following{/other_user}","gists_url":"https://api.github.com/users/sohah/gists{/gist_id}","starred_url":"https://api.github.com/users/sohah/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sohah/subscriptions","organizations_url":"https://api.github.com/users/sohah/orgs","repos_url":"https://api.github.com/users/sohah/repos","events_url":"https://api.github.com/users/sohah/events{/privacy}","received_events_url":"https://api.github.com/users/sohah/received_events","type":"User","site_admin":false}],"milestone":null,"comments":0,"created_at":"2018-10-26T17:27:18Z","updated_at":"2018-10-27T16:48:55Z","closed_at":null,"author_association":"OWNER","body":"We are having an issue, it initially happened in replace_5 benchmark, but I narrowed it down to a small example. It basically happens when we are running in SPFCases mode and on the veritesting choice. This problems only manifest for arrays, fields and locals are fine if we run the same example. \r\n\r\nWhat happens is that in the veritesting path, we check if the solver thinks it is SAT and the solver says no, however if we ignore the checking for solver SAT in the listener and let SPF figure it out on its own, SPF is able to finish the path, no problem.\r\n\r\nThe example is below and the jpf file is [here](https://github.com/sohah/VeritestingTransformations/blob/e1922edcf5d3c41f2045e5c6d1c950c49456b7fb/src/examples/ObjectCreationTC9.jpf).\r\n\r\n`public int createObjectTC9(boolean x, boolean y) {\r\n        int[] b = {0,1};\r\n\r\n        if (x) {\r\n            b[0] = 3 + b[0];\r\n        } else {\r\n            b[0] = 2 + b[0];\r\n        }\r\n\r\n\r\n        if (y) {\r\n            b[0] = 4 + b[0];\r\n        } else {\r\n            b[0] = 2 + b[0];\r\n        }\r\n\r\n        System.out.println(\"reached the end.\");\r\n        return b[0];\r\n    }\r\n`"},"comment":{"url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/comments/433636491","html_url":"https://github.com/sohah/VeritestingTransformations/issues/25#issuecomment-433636491","issue_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/25","id":433636491,"node_id":"MDEyOklzc3VlQ29tbWVudDQzMzYzNjQ5MQ==","user":{"login":"mwwhalen","id":5216954,"node_id":"MDQ6VXNlcjUyMTY5NTQ=","avatar_url":"https://avatars0.githubusercontent.com/u/5216954?v=4","gravatar_id":"","url":"https://api.github.com/users/mwwhalen","html_url":"https://github.com/mwwhalen","followers_url":"https://api.github.com/users/mwwhalen/followers","following_url":"https://api.github.com/users/mwwhalen/following{/other_user}","gists_url":"https://api.github.com/users/mwwhalen/gists{/gist_id}","starred_url":"https://api.github.com/users/mwwhalen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mwwhalen/subscriptions","organizations_url":"https://api.github.com/users/mwwhalen/orgs","repos_url":"https://api.github.com/users/mwwhalen/repos","events_url":"https://api.github.com/users/mwwhalen/events{/privacy}","received_events_url":"https://api.github.com/users/mwwhalen/received_events","type":"User","site_admin":false},"created_at":"2018-10-27T16:48:55Z","updated_at":"2018-10-27T16:48:55Z","author_association":"COLLABORATOR","body":"I am not sure I understand; now that I am back in town, could we discuss at\nour next meeting on Tuesday?\n\nMike\n\nOn Fri, Oct 26, 2018 at 12:27 PM sohah <notifications@github.com> wrote:\n\n> We are having an issue, it initially happened in replace_5 benchmark, but\n> I narrowed it down to a small example. It basically happens when we are\n> running in SPFCases mode and on the veritesting choice. This problems only\n> manifest for arrays, fields and locals are fine if we run the same example.\n>\n> What happens is that in the veritesting path, we check if the solver\n> thinks it is SAT and the solver says no, however if we ignore the checking\n> for solver SAT in the listener and let SPF figure it out on its own, SPF is\n> able to finish the path, no problem.\n>\n> The example is below and the jpf file is here\n> <https://github.com/sohah/VeritestingTransformations/blob/e1922edcf5d3c41f2045e5c6d1c950c49456b7fb/src/examples/ObjectCreationTC9.jpf>\n> .\n>\n> `public int createObjectTC9(boolean x, boolean y) {\n> int[] b = {0,1};\n>\n>     if (x) {\n>         b[0] = 3 + b[0];\n>     } else {\n>         b[0] = 2 + b[0];\n>     }\n>\n>\n>     if (y) {\n>         b[0] = 4 + b[0];\n>     } else {\n>         b[0] = 2 + b[0];\n>     }\n>\n>     System.out.println(\"reached the end.\");\n>     return b[0];\n> }\n>\n> `\n>\n> —\n> You are receiving this because you are subscribed to this thread.\n> Reply to this email directly, view it on GitHub\n> <https://github.com/sohah/VeritestingTransformations/issues/25>, or mute\n> the thread\n> <https://github.com/notifications/unsubscribe-auth/AE-aumgYs2iWHGMn2lWmIJLE2F40S9uIks5uo0X3gaJpZM4X8pzl>\n> .\n>\n\n\n-- \nMichael Whalen\nAdjunct Professor, University of Minnesota Software Engineering Center\n(UMSEC)\n200 Union St. 4-192\nMinneapolis, MN 55455\nOffice: 612-624-5130\nCell: 651-442-8834\n"}}
{"actor":{"display_login":"mwwhalen"}}