{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/502","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/502/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/502/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/502/events","html_url":"https://github.com/Z3Prover/z3/issues/502","id":139571546,"number":502,"title":"C++ API Memory Leak","user":{"login":"whaaswijk","id":3306383,"avatar_url":"https://avatars.githubusercontent.com/u/3306383?v=3","gravatar_id":"","url":"https://api.github.com/users/whaaswijk","html_url":"https://github.com/whaaswijk","followers_url":"https://api.github.com/users/whaaswijk/followers","following_url":"https://api.github.com/users/whaaswijk/following{/other_user}","gists_url":"https://api.github.com/users/whaaswijk/gists{/gist_id}","starred_url":"https://api.github.com/users/whaaswijk/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/whaaswijk/subscriptions","organizations_url":"https://api.github.com/users/whaaswijk/orgs","repos_url":"https://api.github.com/users/whaaswijk/repos","events_url":"https://api.github.com/users/whaaswijk/events{/privacy}","received_events_url":"https://api.github.com/users/whaaswijk/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-03-09T13:03:04Z","updated_at":"2016-03-09T13:25:11Z","closed_at":"2016-03-09T13:25:11Z","body":"I am running into some memory leaks using Z3 C++ API. For example, see this very simple program adapted from the C++ API examples:\r\n`#include<vector>\r\n#include\"z3++.h\"\r\n\r\nusing namespace z3;\r\n\r\nint main(void) {\r\n std::cout << \"de-Morgan example\\n\";\r\n\r\n context c;\r\n\r\n expr x = c.bool_const(\"x\");\r\n expr y = c.bool_const(\"y\");\r\n expr conjecture = !(x && y) == (!x || !y);\r\n\r\n solver s(c);\r\n // adding the negation of the conjecture as a constraint.\r\n s.add(!conjecture);\r\n std::cout << s << \"\\n\";\r\n switch (s.check()) {\r\n     case unsat:   std::cout << \"de-Morgan is valid\\n\"; break;\r\n     case sat:     std::cout << \"de-Morgan is not valid\\n\"; break;\r\n     case unknown: std::cout << \"unknown\\n\"; break;\r\n }\r\n\r\n return 0;\r\n}`\r\n\r\nRunning this through Valgrind reports 75 errors and about 25K memory lost. I'm using Apple LLVM 7.0.2 (clang-700.1.81) on OSX 10.10.5 and the latest revision of Z3's master branch. Am I using the API incorrectly here?\r\n\r\n\r\n"}}