{"action":"created","issue":{"url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/13","repository_url":"https://api.github.com/repos/sohah/VeritestingTransformations","labels_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/13/labels{/name}","comments_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/13/comments","events_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/13/events","html_url":"https://github.com/sohah/VeritestingTransformations/issues/13","id":360092879,"node_id":"MDU6SXNzdWUzNjAwOTI4Nzk=","number":13,"title":"TestAndIte equivalence-check fails","user":{"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},"labels":[{"id":993115069,"node_id":"MDU6TGFiZWw5OTMxMTUwNjk=","url":"https://api.github.com/repos/sohah/VeritestingTransformations/labels/bug","name":"bug","color":"d73a4a","default":true},{"id":1056079454,"node_id":"MDU6TGFiZWwxMDU2MDc5NDU0","url":"https://api.github.com/repos/sohah/VeritestingTransformations/labels/fixed%20but%20needs%20check%20to%20close","name":"fixed but needs check to close","color":"ffeeb5","default":false}],"state":"closed","locked":false,"assignee":{"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},"assignees":[{"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":1,"created_at":"2018-09-13T22:42:11Z","updated_at":"2018-09-14T15:08:03Z","closed_at":"2018-09-14T15:08:03Z","author_association":"COLLABORATOR","body":"Please find the source code for [TestAndIte](https://github.com/sohah/VeritestingTransformations/blob/master/src/examples/TestAndIte.java) equivalence check here and run it using [this JPF configuration file](https://github.com/sohah/VeritestingTransformations/blob/master/src/examples/TestAndIte.jpf). \r\n\r\nPlease find my log file here: [TestAndIte.log](https://github.com/sohah/VeritestingTransformations/files/2380953/TestAndIte.log)\r\n\r\nThe equivalence checker finds that the branch side where the outputs aren't equal is feasible. \r\n\r\n### Disclaimer\r\nPlease feel free to stop reading this bug report at this point and investigate this issue on your own. I did some preliminary investigation of it and report my findings below. But, I could be going down the wrong path with my investigation. \r\n\r\n----------\r\n### Preliminary investigation\r\nI ran this example with `symbolic.debug` set to `true`. I used the printed solver output in this file to create the following SMT query:  [test.txt](https://github.com/sohah/VeritestingTransformations/files/2381227/test.txt)\r\n\r\nNear the beginning, `@w9$1` is set to equal `in0 + 1` on the line `  (= (bvadd in0 #x00000001) @w9$1)`. \r\n\r\nAs we can also see, the input to the veritesting region is in `@w3$1`. The output of the region, `@w9$1` is going to be either `@w3$1 + 1` or `@w3$1 - 1`.  \r\n\r\nSince `in0` and `@w3$1` are both unconstrained, the solver can easily set them to different values. I added the assertion `(assert (not (= in0 @w3$1)))` at the end to check if the solver can make the input `in0` unequal to `@w3$1`. If it were never possible for these two variables to be unequal, the solver would report \"unsat\". Unfortunately, the solver reports \"sat\" along with a model that shows the value of `in0` can be different from the value of `@w3$1`. \r\n\r\nThe integer input to the region should really have been `in0`. In other words, `in0` should have been equal to `@w3$1`. Since there is no clause which establishes this equality, the solver finds a inequivalence. I am guessing this is an issue with input substitution and assigning this issue to Soha. "},"comment":{"url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/comments/421388947","html_url":"https://github.com/sohah/VeritestingTransformations/issues/13#issuecomment-421388947","issue_url":"https://api.github.com/repos/sohah/VeritestingTransformations/issues/13","id":421388947,"node_id":"MDEyOklzc3VlQ29tbWVudDQyMTM4ODk0Nw==","user":{"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},"created_at":"2018-09-14T15:08:03Z","updated_at":"2018-09-14T15:08:03Z","author_association":"COLLABORATOR","body":"Wonderful! I've verified that I can see the input being correctly populated in the SMT formula. Here's the portion of the formula last printed by SPF after the fix. \r\n```\r\n(bvsge in0 #x80000000)\r\n  (bvsle in0 #x7fffffff)\r\n  (bvsge @w9$5 #x80000000)\r\n  (bvsle @w9$5 #x7fffffff)\r\n  (= (bvsub in0 #x00000001) @w9$5)\r\n  (bvsge @w8$5 #x80000000)\r\n  (bvsle @w8$5 #x7fffffff)\r\n  (bvsge in0 #x80000000)\r\n  (bvsle in0 #x7fffffff)\r\n  (bvsge @w7$5 #x80000000)\r\n  (bvsle @w7$5 #x7fffffff)\r\n  (bvsge b0 #x00000000)\r\n  (bvsle b0 #x00000001)\r\n  (bvsge b1 #x00000000)\r\n  (bvsle b1 #x00000001)\r\n  (bvsge @w9$5 #x80000000)\r\n  (bvsle @w9$5 #x7fffffff)\r\n  (let ((a!1 (or (= b0 #x00000000)\r\n                 (and (not (= b0 #x00000000)) (= b1 #x00000000)))))\r\n    (and (= @w8$5 (bvsub in0 #x00000001))\r\n         (= @w7$5 (bvadd in0 #x00000001))\r\n         (or (and (= #x00000000 #x00000000) a!1 (= @w9$5 @w8$5))\r\n             (and (= #x00000000 #x00000000) (not a!1) (= @w9$5 @w7$5)))))\r\n  (bvsge b0 #x00000000)\r\n  (bvsle b0 #x00000001)\r\n  (= b0 #x00000000))\r\n```\r\nWe can see that now that the veritesting formula now uses `in0` as the input to the region. Previously, it used `@w3$1` as the input which was a unconstrainted symbolic variable different from `in0`.  "}}
{"actor":{"display_login":"vaibhavbsharma"}}