{"action":"created","issue":{"url":"https://api.github.com/repos/smackers/smack/issues/102","labels_url":"https://api.github.com/repos/smackers/smack/issues/102/labels{/name}","comments_url":"https://api.github.com/repos/smackers/smack/issues/102/comments","events_url":"https://api.github.com/repos/smackers/smack/issues/102/events","html_url":"https://github.com/smackers/smack/issues/102","id":87124242,"number":102,"title":"VERIFIER_nondet functions do not work properly for unsigned types","user":{"login":"zvonimir","id":1040926,"avatar_url":"https://avatars.githubusercontent.com/u/1040926?v=3","gravatar_id":"","url":"https://api.github.com/users/zvonimir","html_url":"https://github.com/zvonimir","followers_url":"https://api.github.com/users/zvonimir/followers","following_url":"https://api.github.com/users/zvonimir/following{/other_user}","gists_url":"https://api.github.com/users/zvonimir/gists{/gist_id}","starred_url":"https://api.github.com/users/zvonimir/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zvonimir/subscriptions","organizations_url":"https://api.github.com/users/zvonimir/orgs","repos_url":"https://api.github.com/users/zvonimir/repos","events_url":"https://api.github.com/users/zvonimir/events{/privacy}","received_events_url":"https://api.github.com/users/zvonimir/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-06-10T22:08:16Z","updated_at":"2015-06-10T23:30:16Z","closed_at":null,"body":"Here is an example:\r\n```\r\n#include \"smack.h\"\r\n\r\nint main(void) {\r\n  unsigned x = __VERIFIER_nondet_unsigned();\r\n  assert (x > 0);\r\n}\r\n```\r\nThis should I believe pass, and yet it does not.\r\nIf you look at `smack-svcomp.h`, unsigned nondet functions there assume that the returned value is >= 0. I am not sure if that is the best solution."},"comment":{"url":"https://api.github.com/repos/smackers/smack/issues/comments/110945862","html_url":"https://github.com/smackers/smack/issues/102#issuecomment-110945862","issue_url":"https://api.github.com/repos/smackers/smack/issues/102","id":110945862,"user":{"login":"MontyCarter","id":4269524,"avatar_url":"https://avatars.githubusercontent.com/u/4269524?v=3","gravatar_id":"","url":"https://api.github.com/users/MontyCarter","html_url":"https://github.com/MontyCarter","followers_url":"https://api.github.com/users/MontyCarter/followers","following_url":"https://api.github.com/users/MontyCarter/following{/other_user}","gists_url":"https://api.github.com/users/MontyCarter/gists{/gist_id}","starred_url":"https://api.github.com/users/MontyCarter/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MontyCarter/subscriptions","organizations_url":"https://api.github.com/users/MontyCarter/orgs","repos_url":"https://api.github.com/users/MontyCarter/repos","events_url":"https://api.github.com/users/MontyCarter/events{/privacy}","received_events_url":"https://api.github.com/users/MontyCarter/received_events","type":"User","site_admin":false},"created_at":"2015-06-10T23:30:16Z","updated_at":"2015-06-10T23:30:16Z","body":"Does it work if you correct the assertion?  `assert (x >= 0)`...  ;)\r\n\r\nAlso, is this within the context of the svcomp pull request (#100), or the develop branch as is?"}}