{"action":"created","issue":{"url":"https://api.github.com/repos/lonsing/depqbf/issues/4","labels_url":"https://api.github.com/repos/lonsing/depqbf/issues/4/labels{/name}","comments_url":"https://api.github.com/repos/lonsing/depqbf/issues/4/comments","events_url":"https://api.github.com/repos/lonsing/depqbf/issues/4/events","html_url":"https://github.com/lonsing/depqbf/issues/4","id":54472698,"number":4,"title":"segfault when using push/pop","user":{"login":"c-cube","id":1274291,"avatar_url":"https://avatars.githubusercontent.com/u/1274291?v=3","gravatar_id":"","url":"https://api.github.com/users/c-cube","html_url":"https://github.com/c-cube","followers_url":"https://api.github.com/users/c-cube/followers","following_url":"https://api.github.com/users/c-cube/following{/other_user}","gists_url":"https://api.github.com/users/c-cube/gists{/gist_id}","starred_url":"https://api.github.com/users/c-cube/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/c-cube/subscriptions","organizations_url":"https://api.github.com/users/c-cube/orgs","repos_url":"https://api.github.com/users/c-cube/repos","events_url":"https://api.github.com/users/c-cube/events{/privacy}","received_events_url":"https://api.github.com/users/c-cube/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-01-15T16:48:45Z","updated_at":"2015-01-16T08:55:21Z","closed_at":null,"body":"Hello, maybe I missed something in the documentation, but I get:\r\n\r\n> qdpll.c:4270: init_literal_watchers: Assertion `!qdpll->result_constraint' failed.\r\n\r\nwith the following file (and depqbf 3.04):\r\n\r\n```c\r\n\r\n#include <assert.h>\r\n#include \"qdpll.h\"\r\n\r\nint main()\r\n{\r\n  QDPLL* s = qdpll_create();\r\n\r\n  qdpll_configure(s, \"--incremental-use\");\r\n\r\n  Nesting l1 = qdpll_new_scope(s, QDPLL_QTYPE_FORALL);\r\n  qdpll_add(s, 1);\r\n  qdpll_add(s, 2);\r\n  qdpll_add(s, 0);\r\n\r\n  Nesting l2 = qdpll_new_scope(s, QDPLL_QTYPE_EXISTS);\r\n  qdpll_add(s, 4);\r\n  qdpll_add(s, 5);\r\n  qdpll_add(s, 0);\r\n\r\n  qdpll_add_var_to_scope(s, 3, l1);\r\n\r\n  /* clause */\r\n  qdpll_add(s, 1);\r\n  qdpll_add(s, 2);\r\n  qdpll_add(s, 3);\r\n  qdpll_add(s, 0);\r\n\r\n  qdpll_add(s, 3);\r\n  qdpll_add(s, 5);\r\n  qdpll_add(s, 0);\r\n\r\n  /* push and add other clauses */\r\n  qdpll_push(s);\r\n  qdpll_add(s, 1);\r\n  qdpll_add(s, -2);\r\n  qdpll_add(s, 3);\r\n  qdpll_add(s, 0);\r\n\r\n  qdpll_add(s, -3);\r\n  qdpll_add(s, 0);\r\n\r\n  QDPLLResult res = qdpll_sat(s);\r\n  assert(res = QDPLL_RESULT_UNSAT);\r\n\r\n  /* pop, keeping only the 2 first clauses */\r\n  qdpll_pop(s);\r\n  qdpll_gc(s);\r\n\r\n\r\n  res = qdpll_sat(s);  /* error here */\r\n  assert(res = QDPLL_RESULT_SAT);\r\n\r\n  return 0;\r\n}\r\n```"},"comment":{"url":"https://api.github.com/repos/lonsing/depqbf/issues/comments/70225012","html_url":"https://github.com/lonsing/depqbf/issues/4#issuecomment-70225012","issue_url":"https://api.github.com/repos/lonsing/depqbf/issues/4","id":70225012,"user":{"login":"lonsing","id":1989839,"avatar_url":"https://avatars.githubusercontent.com/u/1989839?v=3","gravatar_id":"","url":"https://api.github.com/users/lonsing","html_url":"https://github.com/lonsing","followers_url":"https://api.github.com/users/lonsing/followers","following_url":"https://api.github.com/users/lonsing/following{/other_user}","gists_url":"https://api.github.com/users/lonsing/gists{/gist_id}","starred_url":"https://api.github.com/users/lonsing/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lonsing/subscriptions","organizations_url":"https://api.github.com/users/lonsing/orgs","repos_url":"https://api.github.com/users/lonsing/repos","events_url":"https://api.github.com/users/lonsing/events{/privacy}","received_events_url":"https://api.github.com/users/lonsing/received_events","type":"User","site_admin":false},"created_at":"2015-01-16T08:55:20Z","updated_at":"2015-01-16T08:55:20Z","body":"Hi Simon,\r\n\r\nthank you for your example! To solve the problem, 'qdpll_reset(s)' should be called before calling 'qdpll_sat(s)' again and before calling 'qdpll_pop(s)' in your program. \r\n\r\nThe assertion failure was expected but I will update the documentation of the API in the next release.\r\n\r\nFlorian  "}}