{"action":"created","issue":{"url":"https://api.github.com/repos/agra-uni-bremen/metaSMT/issues/23","labels_url":"https://api.github.com/repos/agra-uni-bremen/metaSMT/issues/23/labels{/name}","comments_url":"https://api.github.com/repos/agra-uni-bremen/metaSMT/issues/23/comments","events_url":"https://api.github.com/repos/agra-uni-bremen/metaSMT/issues/23/events","html_url":"https://github.com/agra-uni-bremen/metaSMT/issues/23","id":69443757,"number":23,"title":"Integrate CVC4","user":{"login":"anithag","id":6982559,"avatar_url":"https://avatars.githubusercontent.com/u/6982559?v=3","gravatar_id":"","url":"https://api.github.com/users/anithag","html_url":"https://github.com/anithag","followers_url":"https://api.github.com/users/anithag/followers","following_url":"https://api.github.com/users/anithag/following{/other_user}","gists_url":"https://api.github.com/users/anithag/gists{/gist_id}","starred_url":"https://api.github.com/users/anithag/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/anithag/subscriptions","organizations_url":"https://api.github.com/users/anithag/orgs","repos_url":"https://api.github.com/users/anithag/repos","events_url":"https://api.github.com/users/anithag/events{/privacy}","received_events_url":"https://api.github.com/users/anithag/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":12,"created_at":"2015-04-19T17:03:37Z","updated_at":"2015-04-20T12:39:18Z","closed_at":null,"body":"I have built metasmt with CVC4 and Z3 (only).  The build suceeded. Now I am trying to build klee with this metaSMT. I have made few changes to make sure CVC4  backend is accepted. I get build error. Relevant change and error is shown below:\r\n\r\n@@ -314,6 +315,10 @@ Executor::Executor(const InterpreterOptions &opts,\r\n               backend = \"Z3\";\r\n               coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > > (UseForkedCoreSolver, CoreSolverOptimizeDivides);\r\n               break;\r\n\\+          case METASMT_BACKEND_CVC4:\r\n\\+              backend = \"CVC4\";\r\n\\+              coreSolver = new MetaSMTSolver< DirectSolver_Context < CVC4 > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);\r\n\\+              break;\r\n           case METASMT_BACKEND_BOOLECTOR:\r\n               backend = \"Boolector\";\r\n\r\n------------------------------\r\nThis is giving me following compilation error. Any idea why? Note that METASMT_BACKEND_CVC4 is recognised and I have included CVC4.hpp in Executor.cpp. CVC4 is getting recognized but still is giving template 1 is invalid. Most of the code follows Z3_Backend.\r\n\r\nExecutor.cpp: In constructor ‘klee::Executor::Executor(const klee::Interpreter::InterpreterOptions&, klee::InterpreterHandler\\*)’:\r\nExecutor.cpp:320:75:  error: **template argument 1 is invalid**\r\n               coreSolver = new MetaSMTSolver< DirectSolver_Context < CVC4 > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);\r\n                                                                           ^\r\nExecutor.cpp:320:77: error: template argument 1 is invalid\r\n               coreSolver = new MetaSMTSolver< DirectSolver_Context < CVC4 > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);\r\n\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/agra-uni-bremen/metaSMT/issues/comments/94441601","html_url":"https://github.com/agra-uni-bremen/metaSMT/issues/23#issuecomment-94441601","issue_url":"https://api.github.com/repos/agra-uni-bremen/metaSMT/issues/23","id":94441601,"user":{"login":"finnhaedicke","id":853839,"avatar_url":"https://avatars.githubusercontent.com/u/853839?v=3","gravatar_id":"","url":"https://api.github.com/users/finnhaedicke","html_url":"https://github.com/finnhaedicke","followers_url":"https://api.github.com/users/finnhaedicke/followers","following_url":"https://api.github.com/users/finnhaedicke/following{/other_user}","gists_url":"https://api.github.com/users/finnhaedicke/gists{/gist_id}","starred_url":"https://api.github.com/users/finnhaedicke/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/finnhaedicke/subscriptions","organizations_url":"https://api.github.com/users/finnhaedicke/orgs","repos_url":"https://api.github.com/users/finnhaedicke/repos","events_url":"https://api.github.com/users/finnhaedicke/events{/privacy}","received_events_url":"https://api.github.com/users/finnhaedicke/received_events","type":"User","site_admin":false},"created_at":"2015-04-20T12:39:18Z","updated_at":"2015-04-20T12:39:18Z","body":"I think it is still required, because Klee uses its own version of STP with Minisat. See https://github.com/anithag/kleestr/blob/master/stp-r940/src/sat/core/Solver.h\r\n\r\nNode your might want to also pull the new version Z3 (zZ3-git, MIT license)."}}