{"action":"created","issue":{"url":"https://api.github.com/repos/seahorn/seahorn/issues/3","labels_url":"https://api.github.com/repos/seahorn/seahorn/issues/3/labels{/name}","comments_url":"https://api.github.com/repos/seahorn/seahorn/issues/3/comments","events_url":"https://api.github.com/repos/seahorn/seahorn/issues/3/events","html_url":"https://github.com/seahorn/seahorn/issues/3","id":62889310,"number":3,"title":"Spacer/Z3 fails with small step and interproc encoding","user":{"login":"jorgenavas","id":5025780,"avatar_url":"https://avatars.githubusercontent.com/u/5025780?v=3","gravatar_id":"","url":"https://api.github.com/users/jorgenavas","html_url":"https://github.com/jorgenavas","followers_url":"https://api.github.com/users/jorgenavas/followers","following_url":"https://api.github.com/users/jorgenavas/following{/other_user}","gists_url":"https://api.github.com/users/jorgenavas/gists{/gist_id}","starred_url":"https://api.github.com/users/jorgenavas/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jorgenavas/subscriptions","organizations_url":"https://api.github.com/users/jorgenavas/orgs","repos_url":"https://api.github.com/users/jorgenavas/repos","events_url":"https://api.github.com/users/jorgenavas/events{/privacy}","received_events_url":"https://api.github.com/users/jorgenavas/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"agurfinkel","id":6082023,"avatar_url":"https://avatars.githubusercontent.com/u/6082023?v=3","gravatar_id":"","url":"https://api.github.com/users/agurfinkel","html_url":"https://github.com/agurfinkel","followers_url":"https://api.github.com/users/agurfinkel/followers","following_url":"https://api.github.com/users/agurfinkel/following{/other_user}","gists_url":"https://api.github.com/users/agurfinkel/gists{/gist_id}","starred_url":"https://api.github.com/users/agurfinkel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/agurfinkel/subscriptions","organizations_url":"https://api.github.com/users/agurfinkel/orgs","repos_url":"https://api.github.com/users/agurfinkel/repos","events_url":"https://api.github.com/users/agurfinkel/events{/privacy}","received_events_url":"https://api.github.com/users/agurfinkel/received_events","type":"User","site_admin":false},"milestone":null,"comments":1,"created_at":"2015-03-19T06:08:34Z","updated_at":"2015-03-19T14:36:54Z","closed_at":null,"body":"I think this error has been there for a while.\r\nThe commands are:\r\n\r\n```clang -c -emit-llvm ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c -o cdaudio_simpl1_false-unreach-call_true-termination.cil.bc```\r\n\r\n```seapp cdaudio_simpl1_false-unreach-call_true-termination.cil.bc -horn-mixed-sem -o  cdaudio_simpl1_false-unreach-call_true-termination.cil.mixed.pp.bc```\r\n\r\n```seahorn cdaudio_simpl1_false-unreach-call_true-termination.cil.mixed.pp.bc -horn-inter-proc -horn-solve```\r\n\r\nproduces the error:\r\n\r\nASSERTION VIOLATION\r\nFile: ../src/ast/ast.cpp\r\nLine: 2484\r\nto_app(get_fact(p2))->get_arg(0) == get_fact(p1)\r\n(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\r\n"},"comment":{"url":"https://api.github.com/repos/seahorn/seahorn/issues/comments/83611293","html_url":"https://github.com/seahorn/seahorn/issues/3#issuecomment-83611293","issue_url":"https://api.github.com/repos/seahorn/seahorn/issues/3","id":83611293,"user":{"login":"agurfinkel","id":6082023,"avatar_url":"https://avatars.githubusercontent.com/u/6082023?v=3","gravatar_id":"","url":"https://api.github.com/users/agurfinkel","html_url":"https://github.com/agurfinkel","followers_url":"https://api.github.com/users/agurfinkel/followers","following_url":"https://api.github.com/users/agurfinkel/following{/other_user}","gists_url":"https://api.github.com/users/agurfinkel/gists{/gist_id}","starred_url":"https://api.github.com/users/agurfinkel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/agurfinkel/subscriptions","organizations_url":"https://api.github.com/users/agurfinkel/orgs","repos_url":"https://api.github.com/users/agurfinkel/repos","events_url":"https://api.github.com/users/agurfinkel/events{/privacy}","received_events_url":"https://api.github.com/users/agurfinkel/received_events","type":"User","site_admin":false},"created_at":"2015-03-19T14:36:54Z","updated_at":"2015-03-19T14:36:54Z","body":"@jorgenavas This seems to have something to do with covers. Triggers an issue deep inside proof-producing portion of Z3. Similar to an issue we had before.\r\n\r\nSeems to work using `z3_smt2.py` script. So should work with `seahorn_inter.py`. Let me know how urgent this is. I'll try to look into it on the weekend. A quick look now tells me that it is different (but similar) to the other time this assertion was triggered.\r\n"}}