{"action":"created","issue":{"url":"https://api.github.com/repos/seahorn/seahorn/issues/61","repository_url":"https://api.github.com/repos/seahorn/seahorn","labels_url":"https://api.github.com/repos/seahorn/seahorn/issues/61/labels{/name}","comments_url":"https://api.github.com/repos/seahorn/seahorn/issues/61/comments","events_url":"https://api.github.com/repos/seahorn/seahorn/issues/61/events","html_url":"https://github.com/seahorn/seahorn/issues/61","id":196481153,"number":61,"title":"Counter-example does not violate the assertion","user":{"login":"leonardoalt","id":504195,"avatar_url":"https://avatars.githubusercontent.com/u/504195?v=3","gravatar_id":"","url":"https://api.github.com/users/leonardoalt","html_url":"https://github.com/leonardoalt","followers_url":"https://api.github.com/users/leonardoalt/followers","following_url":"https://api.github.com/users/leonardoalt/following{/other_user}","gists_url":"https://api.github.com/users/leonardoalt/gists{/gist_id}","starred_url":"https://api.github.com/users/leonardoalt/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leonardoalt/subscriptions","organizations_url":"https://api.github.com/users/leonardoalt/orgs","repos_url":"https://api.github.com/users/leonardoalt/repos","events_url":"https://api.github.com/users/leonardoalt/events{/privacy}","received_events_url":"https://api.github.com/users/leonardoalt/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-12-19T18:00:56Z","updated_at":"2016-12-19T18:12:51Z","closed_at":null,"body":"Hi there,\r\n\r\nI'm verifying the following code:\r\n```\r\n#include \"seahorn/seahorn.h\"\r\n\r\nint nondet();\r\n\r\nint square(int x)\r\n{\r\n    return x*x;\r\n}\r\n\r\nint main()\r\n{\r\n    int x = nondet();\r\n    assume(x>1);\r\n    assume(x<100);\r\n    int y = square(x);\r\n    sassert(y>0);\r\n    return 0;\r\n}\r\n```\r\nSeaHorn gives SAT for this assertion.\r\nWhen I generate the counter-example, the error location is not executed.\r\nBesides, when debugging, it says the values are x=2 and y=4, which shouldn't violate the assertion.\r\n\r\nAny clues on what could be wrong here?\r\n\r\nCheers,\r\nLeonardo\r\n"},"comment":{"url":"https://api.github.com/repos/seahorn/seahorn/issues/comments/268035994","html_url":"https://github.com/seahorn/seahorn/issues/61#issuecomment-268035994","issue_url":"https://api.github.com/repos/seahorn/seahorn/issues/61","id":268035994,"user":{"login":"caballa","id":5025780,"avatar_url":"https://avatars.githubusercontent.com/u/5025780?v=3","gravatar_id":"","url":"https://api.github.com/users/caballa","html_url":"https://github.com/caballa","followers_url":"https://api.github.com/users/caballa/followers","following_url":"https://api.github.com/users/caballa/following{/other_user}","gists_url":"https://api.github.com/users/caballa/gists{/gist_id}","starred_url":"https://api.github.com/users/caballa/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/caballa/subscriptions","organizations_url":"https://api.github.com/users/caballa/orgs","repos_url":"https://api.github.com/users/caballa/repos","events_url":"https://api.github.com/users/caballa/events{/privacy}","received_events_url":"https://api.github.com/users/caballa/received_events","type":"User","site_admin":false},"created_at":"2016-12-19T18:12:50Z","updated_at":"2016-12-19T18:12:50Z","body":"I think the problem is Z3 with non-linear constraints.\n\n\nJorge\n\n\nOn 12/19/16 10:00 AM, Leonardo wrote:\n>\n> Hi there,\n>\n> I'm verifying the following code:\n>\n> |#include \"seahorn/seahorn.h\" int nondet(); int square(int x) { return \n> x*x; } int main() { int x = nondet(); assume(x>1); assume(x<100); int \n> y = square(x); sassert(y>0); return 0; } |\n>\n> SeaHorn gives SAT for this assertion.\n> When I generate the counter-example, the error location is not executed.\n> Besides, when debugging, it says the values are x=2 and y=4, which \n> shouldn't violate the assertion.\n>\n> Any clues on what could be wrong here?\n>\n> Cheers,\n> Leonardo\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/seahorn/seahorn/issues/61>, or mute the thread \n> <https://github.com/notifications/unsubscribe-auth/AEyv9GgN-E-FddRqdUkAKghnGSXXSA2Iks5rJsZYgaJpZM4LRA9n>.\n>\n\n"}}
{"actor":{"display_login":"caballa"}}