{"action":"created","comment":{"url":"https://api.github.com/repos/seahorn/seahorn/pulls/comments/68883477","id":68883477,"diff_hunk":"@@ -0,0 +1,292 @@\n+#include \"seahorn/Houdini.hh\"\n+#include \"seahorn/HornifyModule.hh\"\n+#include \"seahorn/HornClauseDBTransf.hh\"\n+#include \"seahorn/HornClauseDB.hh\"\n+\n+#include \"llvm/IR/Function.h\"\n+#include \"llvm/Support/CommandLine.h\"\n+\n+#include \"ufo/Expr.hpp\"\n+#include \"ufo/Smt/Z3n.hpp\"\n+#include \"ufo/Smt/EZ3.hh\"\n+#include <vector>\n+\n+using namespace llvm;\n+\n+namespace seahorn\n+{\n+  char Houdini::ID = 0;\n+\n+  struct IsBVar : public std::unary_function<Expr, bool>\n+  {\n+     IsBVar () {}\n+     bool operator() (Expr e)\n+     {return bind::isBVar (e);}\n+  };\n+\n+  struct IsPredApp : public std::unary_function<Expr, bool>\n+  {\n+     HornClauseDB &m_db;\n+     IsPredApp (HornClauseDB &db) : m_db (db) {}\n+\n+     bool operator() (Expr e)\n+     {return bind::isFapp (e) && m_db.hasRelation (bind::fname(e));}\n+  };\n+\n+  /*\n+   * Extract all bvars in an expression\n+   */\n+  template<typename OutputIterator>\n+  void Houdini::get_all_bvars (Expr e, OutputIterator out)\n+  {filter (e, IsBVar(), out);}\n+\n+  /*\n+   * Extract all predicates in an expression\n+   */\n+  template<typename OutputIterator>\n+  void Houdini::get_all_pred_apps (Expr e, HornClauseDB &db, OutputIterator out)\n+  {filter (e, IsPredApp(db), out);}\n+\n+  bool Houdini::runOnModule (Module &M)\n+  {\n+    HornifyModule &hm = getAnalysis<HornifyModule> ();\n+\n+    //load the Horn clause database\n+    auto &db = hm.getHornClauseDB ();\n+    db.buildIndexes ();\n+\n+    runHoudini(db, hm);\n+\n+    return false;\n+  }\n+\n+  void Houdini::getAnalysisUsage (AnalysisUsage &AU) const\n+  {\n+    AU.addRequired<HornifyModule> ();\n+    AU.setPreservesAll();\n+  }\n+\n+  /*\n+   * Use template to convert a predicate to candidate\n+   */\n+  Expr Houdini::relToCand(Expr fdecl)\n+  {\n+\tExprVector bvars;\n+\tExprVector bins;   // a vector of LT expressions\n+\tExpr cand = NULL;\n+\n+\tint bvar_count = 0;\n+\tunsigned i = 0;\n+\tfor (i=0; i < bind::domainSz(fdecl); i++)\n+\t{\n+\t\t// if its type is INT\n+\t\tif (isOpX<INT_TY>(bind::domainTy(fdecl, i)))\n+\t\t{\n+\t\t\t// what is efac?\n+\t\t\tExpr bvar = bind::bvar (i, mk<INT_TY>(bind::domainTy(fdecl, i)->efac())); //the id of bvar is the same as related arg index\n+\t\t\tbvars.push_back(bvar);\n+\t\t\tbvar_count ++;\n+\t\t}\n+\t}\n+\n+\t//What if there's no bvar?\n+\tif(bvar_count == 0)\n+\t{\n+\t\tcand = mk<TRUE>(fdecl->efac());\n+\t}\n+\t// if there is only one bvar, create a int constant and make an lt expr\n+\telse if(bvar_count == 1)\n+\t{\n+\t\tExpr zero = mkTerm<mpz_class> (0, fdecl->efac());\n+\t\tcand = mk<LT>(bvars[0], zero);\n+\t}\n+\t// if there are more than two bvars, make an lt expr\n+\telse if(bvar_count == 2)\n+\t{\n+\t\tExpr lt1 = mk<LT>(bvars[0], bvars[1]);\n+\t\tExpr lt2 = mk<LT>(bvars[1], bvars[0]);\n+\t\tbins.push_back(lt1);\n+\t\tbins.push_back(lt2);\n+\n+\t\tcand = mknary<AND>(bins.begin(), bins.end());\n+\t}\n+\telse // bvar_count > 2\n+\t{\n+\t\tfor(int j=0; j<bvars.size()-1; j++)\n+\t\t{\n+\t\t\tExpr lt = mk<LT>(bvars[j], bvars[j+1]);\n+\t\t\tbins.push_back(lt);\n+\t\t}\n+\t\tcand = mknary<AND>(bins.begin(), bins.end());\n+\t}\n+\n+\treturn cand;\n+  }\n+\n+  #define SAT true\n+  #define UNSAT false\n+\n+  std::map<Expr, Expr> Houdini::currentCandidates;\t//a map from predicates to candidates\n+\n+  /*\n+   * Build the map from predicates to candidates\n+   */\n+  void Houdini::guessCandidate(HornClauseDB &db)\n+  {\n+\t  for(Expr rel : db.getRelations())\n+\t  {\n+\t\t  if(bind::isFdecl(rel))\n+\t\t  {\n+\t\t\t  Expr cand = relToCand(rel);\n+\t\t\t  currentCandidates.insert(std::pair<Expr, Expr>(rel, cand));\n+\t\t  }\n+\t  }\n+  }\n+\n+  /*\n+   * Main loop of Houdini algorithm\n+   */\n+  void Houdini::runHoudini(HornClauseDB &db, HornifyModule &hm)\n+  {\n+\t  guessCandidate(db);\n+\n+\t  HornClauseDB::RuleVector workList;\n+\t  workList.insert(workList.end(), db.getRules().begin(), db.getRules().end());\n+\n+\t  while(!workList.empty())\n+\t  {\n+\t\t  HornRule r = workList.front();\n+\t\t  errs() << \"RULE HEAD: \" << *(r.head()) << \"\\n\";\n+\t\t  errs() << \"RULE BODY: \" << *(r.body()) << \"\\n\";\n+\t\t  while (validateRule(r, db, hm) == SAT)\n+\t\t  {\n+\t\t\t  workList = addUsedRulesBackToWorkList(db, workList, r.head());\n+\t\t\t  weakenRuleHeadCand(r);\n+\t\t  }\n+\t\t  workList.erase(workList.begin());\n+\t  }\n+  }\n+\n+  /*\n+   * Given a rule, check if it's validate\n+   */\n+  bool Houdini::validateRule(HornRule r, HornClauseDB &db, HornifyModule &hm)\n+  {\n+\t  Expr ruleHead_cand_app = applyActualArgsToCand(r.head());\n+\t  Expr neg_ruleHead_cand_app = mk<NEG>(ruleHead_cand_app);\n+\n+\t  Expr ruleBody = r.body();\n+\t  ExprMap body_map;\n+\t  ExprVector body_pred_apps;\n+\t  get_all_pred_apps(ruleBody, db, std::back_inserter(body_pred_apps));\n+\n+\t  for(ExprVector::iterator itr = body_pred_apps.begin(); itr != body_pred_apps.end(); ++itr)\n+\t  {\n+\t\t  body_map.insert(std::pair<Expr, Expr>(*itr, applyActualArgsToCand(*itr)));\n+\t  }\n+\n+\t  Expr body_cand_app = replace(ruleBody, body_map);\n+\n+\t  Expr whole_cand = mk<AND>(neg_ruleHead_cand_app, body_cand_app);\n+\n+\t  errs() << \"WHOLE CANDIDATE: \" << *whole_cand << \"\\n\";\n+\n+\t  ZSolver<EZ3> solver(hm.getZContext ());\n+\t  solver.assertExpr(whole_cand);\n+\t  solver.toSmtLib(errs());\n+\t  bool isSat = solver.solve();","path":"lib/seahorn/Houdini.cc","position":null,"original_position":197,"commit_id":"911de78c9b74e2c6964540c9c3086c4c3edf23d2","original_commit_id":"cce7a302670f7c9e1a2207c15b3c5d1ac93ec881","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},"body":"if the result is neither true nor false you can still use the model to try\nto throw out a lemma. If nothing works, remove a lemma arbitrarily. In the\nworst case, the invariant is weakened to true and the algorithm stops.\nOn Wed, Jun 29, 2016 at 00:22 Chenguang-Zhu <notifications@github.com>\nwrote:\n\n> In lib/seahorn/Houdini.cc\n> <https://github.com/seahorn/seahorn/pull/33#discussion_r68883313>:\n>\n> > +\n> > +\t  for(ExprVector::iterator itr = body_pred_apps.begin(); itr != body_pred_apps.end(); ++itr)\n> > +\t  {\n> > +\t\t  body_map.insert(std::pair<\n>\n> Expr, Expr>(*itr, applyActualArgsToCand(*itr)));\n> > +\t  }\n> > +\n> > +\t  Expr body_cand_app = replace(ruleBody, body_map);\n> > +\n> > +\t  Expr whole_cand = mk<AND>(neg_ruleHead_cand_app, body_cand_app);\n> > +\n> > +\t  errs() << \"WHOLE CANDIDATE: \" << *whole_cand << \"\\n\";\n> > +\n> > +\t  ZSolver<EZ3> solver(hm.getZContext ());\n> > +\t  solver.assertExpr(whole_cand);\n> > +\t  solver.toSmtLib(errs());\n> > +\t  bool isSat = solver.solve();\n>\n> If solver returns indeterminate for a rule, then how to deal with it? I\n> think maybe we should also try to weaken it until solver can say UNSAT?\n>\n> —\n> You are receiving this because you commented.\n>\n>\n> Reply to this email directly, view it on GitHub\n> <https://github.com/seahorn/seahorn/pull/33/files/cce7a302670f7c9e1a2207c15b3c5d1ac93ec881#r68883313>,\n> or mute the thread\n> <https://github.com/notifications/unsubscribe/AFzN5xb4p6U_AMeP-eMtFY2dN_7tNoufks5qQfMjgaJpZM4I7V-j>\n> .\n>\n","created_at":"2016-06-29T04:25:23Z","updated_at":"2016-06-29T04:25:23Z","html_url":"https://github.com/seahorn/seahorn/pull/33#discussion_r68883477","pull_request_url":"https://api.github.com/repos/seahorn/seahorn/pulls/33","_links":{"self":{"href":"https://api.github.com/repos/seahorn/seahorn/pulls/comments/68883477"},"html":{"href":"https://github.com/seahorn/seahorn/pull/33#discussion_r68883477"},"pull_request":{"href":"https://api.github.com/repos/seahorn/seahorn/pulls/33"}}},"pull_request":{"url":"https://api.github.com/repos/seahorn/seahorn/pulls/33","id":74714293,"html_url":"https://github.com/seahorn/seahorn/pull/33","diff_url":"https://github.com/seahorn/seahorn/pull/33.diff","patch_url":"https://github.com/seahorn/seahorn/pull/33.patch","issue_url":"https://api.github.com/repos/seahorn/seahorn/issues/33","number":33,"state":"open","locked":false,"title":"Houdini Pass","user":{"login":"Chenguang-Zhu","id":19936324,"avatar_url":"https://avatars.githubusercontent.com/u/19936324?v=3","gravatar_id":"","url":"https://api.github.com/users/Chenguang-Zhu","html_url":"https://github.com/Chenguang-Zhu","followers_url":"https://api.github.com/users/Chenguang-Zhu/followers","following_url":"https://api.github.com/users/Chenguang-Zhu/following{/other_user}","gists_url":"https://api.github.com/users/Chenguang-Zhu/gists{/gist_id}","starred_url":"https://api.github.com/users/Chenguang-Zhu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Chenguang-Zhu/subscriptions","organizations_url":"https://api.github.com/users/Chenguang-Zhu/orgs","repos_url":"https://api.github.com/users/Chenguang-Zhu/repos","events_url":"https://api.github.com/users/Chenguang-Zhu/events{/privacy}","received_events_url":"https://api.github.com/users/Chenguang-Zhu/received_events","type":"User","site_admin":false},"body":"The new added Houdini pass; Fix the problem of initializing workList from Rule DB; Fix the design of weakening rule head candidate until it's true.","created_at":"2016-06-22T02:12:50Z","updated_at":"2016-06-29T04:25:24Z","closed_at":null,"merged_at":null,"merge_commit_sha":"016285b75afae61996afa64e8200657c7376430d","assignee":null,"assignees":[],"milestone":null,"commits_url":"https://api.github.com/repos/seahorn/seahorn/pulls/33/commits","review_comments_url":"https://api.github.com/repos/seahorn/seahorn/pulls/33/comments","review_comment_url":"https://api.github.com/repos/seahorn/seahorn/pulls/comments{/number}","comments_url":"https://api.github.com/repos/seahorn/seahorn/issues/33/comments","statuses_url":"https://api.github.com/repos/seahorn/seahorn/statuses/911de78c9b74e2c6964540c9c3086c4c3edf23d2","head":{"label":"Chenguang-Zhu:test","ref":"test","sha":"911de78c9b74e2c6964540c9c3086c4c3edf23d2","user":{"login":"Chenguang-Zhu","id":19936324,"avatar_url":"https://avatars.githubusercontent.com/u/19936324?v=3","gravatar_id":"","url":"https://api.github.com/users/Chenguang-Zhu","html_url":"https://github.com/Chenguang-Zhu","followers_url":"https://api.github.com/users/Chenguang-Zhu/followers","following_url":"https://api.github.com/users/Chenguang-Zhu/following{/other_user}","gists_url":"https://api.github.com/users/Chenguang-Zhu/gists{/gist_id}","starred_url":"https://api.github.com/users/Chenguang-Zhu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Chenguang-Zhu/subscriptions","organizations_url":"https://api.github.com/users/Chenguang-Zhu/orgs","repos_url":"https://api.github.com/users/Chenguang-Zhu/repos","events_url":"https://api.github.com/users/Chenguang-Zhu/events{/privacy}","received_events_url":"https://api.github.com/users/Chenguang-Zhu/received_events","type":"User","site_admin":false},"repo":{"id":61146470,"name":"seahorn","full_name":"Chenguang-Zhu/seahorn","owner":{"login":"Chenguang-Zhu","id":19936324,"avatar_url":"https://avatars.githubusercontent.com/u/19936324?v=3","gravatar_id":"","url":"https://api.github.com/users/Chenguang-Zhu","html_url":"https://github.com/Chenguang-Zhu","followers_url":"https://api.github.com/users/Chenguang-Zhu/followers","following_url":"https://api.github.com/users/Chenguang-Zhu/following{/other_user}","gists_url":"https://api.github.com/users/Chenguang-Zhu/gists{/gist_id}","starred_url":"https://api.github.com/users/Chenguang-Zhu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Chenguang-Zhu/subscriptions","organizations_url":"https://api.github.com/users/Chenguang-Zhu/orgs","repos_url":"https://api.github.com/users/Chenguang-Zhu/repos","events_url":"https://api.github.com/users/Chenguang-Zhu/events{/privacy}","received_events_url":"https://api.github.com/users/Chenguang-Zhu/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/Chenguang-Zhu/seahorn","description":"SeaHorn Verification Framework","fork":true,"url":"https://api.github.com/repos/Chenguang-Zhu/seahorn","forks_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/forks","keys_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/keys{/key_id}","collaborators_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/teams","hooks_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/hooks","issue_events_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/issues/events{/number}","events_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/events","assignees_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/assignees{/user}","branches_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/branches{/branch}","tags_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/tags","blobs_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/git/refs{/sha}","trees_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/git/trees{/sha}","statuses_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/statuses/{sha}","languages_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/languages","stargazers_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/stargazers","contributors_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/contributors","subscribers_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/subscribers","subscription_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/subscription","commits_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/commits{/sha}","git_commits_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/git/commits{/sha}","comments_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/comments{/number}","issue_comment_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/issues/comments{/number}","contents_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/contents/{+path}","compare_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/compare/{base}...{head}","merges_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/merges","archive_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/downloads","issues_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/issues{/number}","pulls_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/pulls{/number}","milestones_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/milestones{/number}","notifications_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/labels{/name}","releases_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/releases{/id}","deployments_url":"https://api.github.com/repos/Chenguang-Zhu/seahorn/deployments","created_at":"2016-06-14T18:30:15Z","updated_at":"2016-06-14T18:30:17Z","pushed_at":"2016-06-29T04:10:11Z","git_url":"git://github.com/Chenguang-Zhu/seahorn.git","ssh_url":"git@github.com:Chenguang-Zhu/seahorn.git","clone_url":"https://github.com/Chenguang-Zhu/seahorn.git","svn_url":"https://github.com/Chenguang-Zhu/seahorn","homepage":null,"size":1590,"stargazers_count":0,"watchers_count":0,"language":"C++","has_issues":false,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"open_issues_count":0,"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"seahorn:master","ref":"master","sha":"94a8b9a3f56d008f03002f3d85c3b517630960e4","user":{"login":"seahorn","id":11098044,"avatar_url":"https://avatars.githubusercontent.com/u/11098044?v=3","gravatar_id":"","url":"https://api.github.com/users/seahorn","html_url":"https://github.com/seahorn","followers_url":"https://api.github.com/users/seahorn/followers","following_url":"https://api.github.com/users/seahorn/following{/other_user}","gists_url":"https://api.github.com/users/seahorn/gists{/gist_id}","starred_url":"https://api.github.com/users/seahorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/seahorn/subscriptions","organizations_url":"https://api.github.com/users/seahorn/orgs","repos_url":"https://api.github.com/users/seahorn/repos","events_url":"https://api.github.com/users/seahorn/events{/privacy}","received_events_url":"https://api.github.com/users/seahorn/received_events","type":"Organization","site_admin":false},"repo":{"id":31487486,"name":"seahorn","full_name":"seahorn/seahorn","owner":{"login":"seahorn","id":11098044,"avatar_url":"https://avatars.githubusercontent.com/u/11098044?v=3","gravatar_id":"","url":"https://api.github.com/users/seahorn","html_url":"https://github.com/seahorn","followers_url":"https://api.github.com/users/seahorn/followers","following_url":"https://api.github.com/users/seahorn/following{/other_user}","gists_url":"https://api.github.com/users/seahorn/gists{/gist_id}","starred_url":"https://api.github.com/users/seahorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/seahorn/subscriptions","organizations_url":"https://api.github.com/users/seahorn/orgs","repos_url":"https://api.github.com/users/seahorn/repos","events_url":"https://api.github.com/users/seahorn/events{/privacy}","received_events_url":"https://api.github.com/users/seahorn/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/seahorn/seahorn","description":"SeaHorn Verification Framework","fork":false,"url":"https://api.github.com/repos/seahorn/seahorn","forks_url":"https://api.github.com/repos/seahorn/seahorn/forks","keys_url":"https://api.github.com/repos/seahorn/seahorn/keys{/key_id}","collaborators_url":"https://api.github.com/repos/seahorn/seahorn/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/seahorn/seahorn/teams","hooks_url":"https://api.github.com/repos/seahorn/seahorn/hooks","issue_events_url":"https://api.github.com/repos/seahorn/seahorn/issues/events{/number}","events_url":"https://api.github.com/repos/seahorn/seahorn/events","assignees_url":"https://api.github.com/repos/seahorn/seahorn/assignees{/user}","branches_url":"https://api.github.com/repos/seahorn/seahorn/branches{/branch}","tags_url":"https://api.github.com/repos/seahorn/seahorn/tags","blobs_url":"https://api.github.com/repos/seahorn/seahorn/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/seahorn/seahorn/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/seahorn/seahorn/git/refs{/sha}","trees_url":"https://api.github.com/repos/seahorn/seahorn/git/trees{/sha}","statuses_url":"https://api.github.com/repos/seahorn/seahorn/statuses/{sha}","languages_url":"https://api.github.com/repos/seahorn/seahorn/languages","stargazers_url":"https://api.github.com/repos/seahorn/seahorn/stargazers","contributors_url":"https://api.github.com/repos/seahorn/seahorn/contributors","subscribers_url":"https://api.github.com/repos/seahorn/seahorn/subscribers","subscription_url":"https://api.github.com/repos/seahorn/seahorn/subscription","commits_url":"https://api.github.com/repos/seahorn/seahorn/commits{/sha}","git_commits_url":"https://api.github.com/repos/seahorn/seahorn/git/commits{/sha}","comments_url":"https://api.github.com/repos/seahorn/seahorn/comments{/number}","issue_comment_url":"https://api.github.com/repos/seahorn/seahorn/issues/comments{/number}","contents_url":"https://api.github.com/repos/seahorn/seahorn/contents/{+path}","compare_url":"https://api.github.com/repos/seahorn/seahorn/compare/{base}...{head}","merges_url":"https://api.github.com/repos/seahorn/seahorn/merges","archive_url":"https://api.github.com/repos/seahorn/seahorn/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/seahorn/seahorn/downloads","issues_url":"https://api.github.com/repos/seahorn/seahorn/issues{/number}","pulls_url":"https://api.github.com/repos/seahorn/seahorn/pulls{/number}","milestones_url":"https://api.github.com/repos/seahorn/seahorn/milestones{/number}","notifications_url":"https://api.github.com/repos/seahorn/seahorn/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/seahorn/seahorn/labels{/name}","releases_url":"https://api.github.com/repos/seahorn/seahorn/releases{/id}","deployments_url":"https://api.github.com/repos/seahorn/seahorn/deployments","created_at":"2015-03-01T05:08:17Z","updated_at":"2016-06-14T05:25:04Z","pushed_at":"2016-06-29T04:10:11Z","git_url":"git://github.com/seahorn/seahorn.git","ssh_url":"git@github.com:seahorn/seahorn.git","clone_url":"https://github.com/seahorn/seahorn.git","svn_url":"https://github.com/seahorn/seahorn","homepage":null,"size":1677,"stargazers_count":28,"watchers_count":28,"language":"C++","has_issues":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":14,"mirror_url":null,"open_issues_count":6,"forks":14,"open_issues":6,"watchers":28,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/seahorn/seahorn/pulls/33"},"html":{"href":"https://github.com/seahorn/seahorn/pull/33"},"issue":{"href":"https://api.github.com/repos/seahorn/seahorn/issues/33"},"comments":{"href":"https://api.github.com/repos/seahorn/seahorn/issues/33/comments"},"review_comments":{"href":"https://api.github.com/repos/seahorn/seahorn/pulls/33/comments"},"review_comment":{"href":"https://api.github.com/repos/seahorn/seahorn/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/seahorn/seahorn/pulls/33/commits"},"statuses":{"href":"https://api.github.com/repos/seahorn/seahorn/statuses/911de78c9b74e2c6964540c9c3086c4c3edf23d2"}}}}
{"actor":{"display_login":"agurfinkel"}}