new: persistent ptree (-write-ptree) and klee-ptree

Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
     and tracks information such as branch type, termination
     type or source location (asm) in nodes. Enabled with
     -write-ptree

ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.

40 files changed, 1520 insertions, 131 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 19e9fc06..4fd68d42 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -310,6 +310,16 @@ if (NOT SQLite3_FOUND)
   message( FATAL_ERROR "SQLite3 not found, please install" )
 endif()
 
+find_program(
+  SQLITE_CLI
+  NAMES "sqlite3"
+  DOC "Path to sqlite3 tool"
+)
+
+if (NOT SQLITE_CLI)
+  set(SQLITE_CLI "")
+endif()
+
 ################################################################################
 # Detect libcap
 ################################################################################
diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h
index 430ff7b1..152241c9 100644
--- a/include/klee/Support/OptionCategories.h
+++ b/include/klee/Support/OptionCategories.h
@@ -29,6 +29,7 @@ namespace klee {
   extern llvm::cl::OptionCategory MiscCat;
   extern llvm::cl::OptionCategory ModuleCat;
   extern llvm::cl::OptionCategory SearchCat;
+  extern llvm::cl::OptionCategory PTreeCat;
   extern llvm::cl::OptionCategory SeedingCat;
   extern llvm::cl::OptionCategory SolvingCat;
   extern llvm::cl::OptionCategory StatsCat;
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 9005a1ff..8df3e259 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -20,6 +20,7 @@ add_library(kleeCore
   Memory.cpp
   MemoryManager.cpp
   PTree.cpp
+  PTreeWriter.cpp
   Searcher.cpp
   SeedInfo.cpp
   SpecialFunctionHandler.cpp
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b4da6a08..8f70540c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3639,14 +3639,15 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   return info.str();
 }
 
-
-void Executor::terminateState(ExecutionState &state) {
+void Executor::terminateState(ExecutionState &state,
+                              StateTerminationType reason) {
   if (replayKTest && replayPosition!=replayKTest->numObjects) {
     klee_warning_once(replayKTest,
                       "replay did not consume all objects in test input.");
   }
 
   interpreterHandler->incPathsExplored();
+  processTree->setTerminationType(state, reason);
 
   std::vector<ExecutionState *>::iterator it =
       std::find(addedStates.begin(), addedStates.end(), &state);
@@ -3690,7 +3691,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
-  terminateState(state);
+  terminateState(state, StateTerminationType::Exit);
 }
 
 void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
@@ -3707,7 +3708,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
         terminationTypeFileExtension(reason).c_str());
   }
 
-  terminateState(state);
+  terminateState(state, reason);
 }
 
 void Executor::terminateStateEarlyAlgorithm(ExecutionState &state,
@@ -3815,7 +3816,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
 
-  terminateState(state);
+  terminateState(state, terminationType);
 
   if (shouldExitOn(terminationType))
     haltExecution = true;
@@ -3848,9 +3849,14 @@ void Executor::terminateStateOnSolverError(ExecutionState &state,
 }
 
 void Executor::terminateStateOnUserError(ExecutionState &state,
-                                         const llvm::Twine &message) {
+                                         const llvm::Twine &message,
+                                         bool writeErr) {
   ++stats::terminationUserError;
-  terminateStateOnError(state, message, StateTerminationType::User, "");
+  if (writeErr) {
+    terminateStateOnError(state, message, StateTerminationType::User, "");
+  } else {
+    terminateState(state, StateTerminationType::User);
+  }
 }
 
 // XXX shoot me
@@ -4601,7 +4607,8 @@ void Executor::runFunctionAsMain(Function *f,
   
   initializeGlobals(*state);
 
-  processTree = std::make_unique<PTree>(state);
+  processTree = createPTree(*state, userSearcherRequiresInMemoryPTree(),
+                            *interpreterHandler);
   run(*state);
   processTree = nullptr;
 
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 204638e8..3635de78 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -412,7 +412,7 @@ private:
 
   /// Remove state from queue and delete state. This function should only be
   /// used in the termination functions below.
-  void terminateState(ExecutionState &state);
+  void terminateState(ExecutionState &state, StateTerminationType reason);
 
   /// Call exit handler and terminate state normally
   /// (end of execution path)
@@ -467,7 +467,8 @@ private:
   /// Call error handler and terminate state for user errors
   /// (e.g. wrong usage of klee.h API)
   void terminateStateOnUserError(ExecutionState &state,
-                                 const llvm::Twine &message);
+                                 const llvm::Twine &message,
+                                 bool writeErr = true);
 
   /// bindModuleConstants - Initialize the module constant table.
   void bindModuleConstants();
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index 6c17e296..c5b640d3 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -11,49 +11,88 @@
 
 #include "ExecutionState.h"
 
-#include "klee/Expr/Expr.h"
+#include "klee/Core/Interpreter.h"
 #include "klee/Expr/ExprPPrinter.h"
+#include "klee/Module/KInstruction.h"
 #include "klee/Support/OptionCategories.h"
 
 #include <bitset>
 #include <vector>
 
 using namespace klee;
-using namespace llvm;
+
+namespace klee {
+llvm::cl::OptionCategory
+    PTreeCat("Process tree related options",
+             "These options affect the process tree handling.");
+}
 
 namespace {
+llvm::cl::opt<bool> CompressProcessTree(
+    "compress-process-tree",
+    llvm::cl::desc("Remove intermediate nodes in the process "
+                   "tree whenever possible (default=false)"),
+    llvm::cl::init(false), llvm::cl::cat(PTreeCat));
+
+llvm::cl::opt<bool> WritePTree(
+    "write-ptree", llvm::cl::init(false),
+    llvm::cl::desc("Write process tree into ptree.db (default=false)"),
+    llvm::cl::cat(PTreeCat));
+} // namespace
 
-cl::opt<bool>
-    CompressProcessTree("compress-process-tree",
-                        cl::desc("Remove intermediate nodes in the process "
-                                 "tree whenever possible (default=false)"),
-                        cl::init(false), cl::cat(MiscCat));
+// PTreeNode
 
-} // namespace
+PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept
+    : parent{parent}, left{nullptr}, right{nullptr}, state{state} {
+  state->ptreeNode = this;
+}
+
+// AnnotatedPTreeNode
+
+AnnotatedPTreeNode::AnnotatedPTreeNode(PTreeNode *parent,
+                                       ExecutionState *state) noexcept
+    : PTreeNode(parent, state) {
+  id = nextID++;
+}
 
-PTree::PTree(ExecutionState *initialState)
-    : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) {
-  initialState->ptreeNode = root.getPointer();
+// NoopPTree
+
+void NoopPTree::dump(llvm::raw_ostream &os) noexcept {
+  os << "digraph G {\nTreeNotAvailable [shape=box]\n}";
 }
 
-void PTree::attach(PTreeNode *node, ExecutionState *leftState,
-                   ExecutionState *rightState, BranchType reason) {
+// InMemoryPTree
+
+InMemoryPTree::InMemoryPTree(ExecutionState &initialState) noexcept {
+  root = PTreeNodePtr(createNode(nullptr, &initialState));
+  initialState.ptreeNode = root.getPointer();
+}
+
+PTreeNode *InMemoryPTree::createNode(PTreeNode *parent, ExecutionState *state) {
+  return new PTreeNode(parent, state);
+}
+
+void InMemoryPTree::attach(PTreeNode *node, ExecutionState *leftState,
+                           ExecutionState *rightState,
+                           BranchType reason) noexcept {
   assert(node && !node->left.getPointer() && !node->right.getPointer());
   assert(node == rightState->ptreeNode &&
          "Attach assumes the right state is the current state");
-  node->state = nullptr;
-  node->left = PTreeNodePtr(new PTreeNode(node, leftState));
+  node->left = PTreeNodePtr(createNode(node, leftState));
   // The current node inherits the tag
   uint8_t currentNodeTag = root.getInt();
   if (node->parent)
     currentNodeTag = node->parent->left.getPointer() == node
                          ? node->parent->left.getInt()
                          : node->parent->right.getInt();
-  node->right = PTreeNodePtr(new PTreeNode(node, rightState), currentNodeTag);
+  node->right = PTreeNodePtr(createNode(node, rightState), currentNodeTag);
+  updateBranchingNode(*node, reason);
+  node->state = nullptr;
 }
 
-void PTree::remove(PTreeNode *n) {
+void InMemoryPTree::remove(PTreeNode *n) noexcept {
   assert(!n->left.getPointer() && !n->right.getPointer());
+  updateTerminatingNode(*n);
   do {
     PTreeNode *p = n->parent;
     if (p) {
@@ -92,17 +131,17 @@ void PTree::remove(PTreeNode *n) {
   }
 }
 
-void PTree::dump(llvm::raw_ostream &os) {
-  ExprPPrinter *pp = ExprPPrinter::create(os);
+void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept {
+  std::unique_ptr<ExprPPrinter> pp(ExprPPrinter::create(os));
   pp->setNewline("\\l");
-  os << "digraph G {\n";
-  os << "\tsize=\"10,7.5\";\n";
-  os << "\tratio=fill;\n";
-  os << "\trotate=90;\n";
-  os << "\tcenter = \"true\";\n";
-  os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n";
-  os << "\tedge [arrowsize=.3]\n";
-  std::vector<const PTreeNode*> stack;
+  os << "digraph G {\n"
+     << "\tsize=\"10,7.5\";\n"
+     << "\tratio=fill;\n"
+     << "\trotate=90;\n"
+     << "\tcenter = \"true\";\n"
+     << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
+     << "\tedge [arrowsize=.3]\n";
+  std::vector<const PTreeNode *> stack;
   stack.push_back(root.getPointer());
   while (!stack.empty()) {
     const PTreeNode *n = stack.back();
@@ -112,24 +151,85 @@ void PTree::dump(llvm::raw_ostream &os) {
       os << ",fillcolor=green";
     os << "];\n";
     if (n->left.getPointer()) {
-      os << "\tn" << n << " -> n" << n->left.getPointer();
-      os << " [label=0b"
+      os << "\tn" << n << " -> n" << n->left.getPointer() << " [label=0b"
          << std::bitset<PtrBitCount>(n->left.getInt()).to_string() << "];\n";
       stack.push_back(n->left.getPointer());
     }
     if (n->right.getPointer()) {
-      os << "\tn" << n << " -> n" << n->right.getPointer();
-      os << " [label=0b"
+      os << "\tn" << n << " -> n" << n->right.getPointer() << " [label=0b"
          << std::bitset<PtrBitCount>(n->right.getInt()).to_string() << "];\n";
       stack.push_back(n->right.getPointer());
     }
   }
   os << "}\n";
-  delete pp;
 }
 
-PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) : parent{parent}, state{state} {
-  state->ptreeNode = this;
-  left = PTreeNodePtr(nullptr);
-  right = PTreeNodePtr(nullptr);
+std::uint8_t InMemoryPTree::getNextId() noexcept {
+  static_assert(PtrBitCount <= 8);
+  std::uint8_t id = 1 << registeredIds++;
+  if (registeredIds > PtrBitCount) {
+    klee_error("PTree cannot support more than %d RandomPathSearchers",
+               PtrBitCount);
+  }
+  return id;
+}
+
+// PersistentPTree
+
+PersistentPTree::PersistentPTree(ExecutionState &initialState,
+                                 InterpreterHandler &ih) noexcept
+    : writer(ih.getOutputFilename("ptree.db")) {
+  root = PTreeNodePtr(createNode(nullptr, &initialState));
+  initialState.ptreeNode = root.getPointer();
+}
+
+void PersistentPTree::dump(llvm::raw_ostream &os) noexcept {
+  writer.batchCommit(true);
+  InMemoryPTree::dump(os);
+}
+
+PTreeNode *PersistentPTree::createNode(PTreeNode *parent,
+                                       ExecutionState *state) {
+  return new AnnotatedPTreeNode(parent, state);
+}
+
+void PersistentPTree::setTerminationType(ExecutionState &state,
+                                         StateTerminationType type) {
+  auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(state.ptreeNode);
+  annotatedNode->kind = type;
+}
+
+void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) {
+  auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(&node);
+  const auto &state = *node.state;
+  const auto prevPC = state.prevPC;
+  annotatedNode->asmLine =
+      prevPC && prevPC->info ? prevPC->info->assemblyLine : 0;
+  annotatedNode->kind = reason;
+  writer.write(*annotatedNode);
+}
+
+void PersistentPTree::updateTerminatingNode(PTreeNode &node) {
+  assert(node.state);
+  auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(&node);
+  const auto &state = *node.state;
+  const auto prevPC = state.prevPC;
+  annotatedNode->asmLine =
+      prevPC && prevPC->info ? prevPC->info->assemblyLine : 0;
+  annotatedNode->stateID = state.getID();
+  writer.write(*annotatedNode);
 }
+
+// Factory
+
+std::unique_ptr<PTree> klee::createPTree(ExecutionState &initialState,
+                                         bool inMemory,
+                                         InterpreterHandler &ih) {
+  if (WritePTree)
+    return std::make_unique<PersistentPTree>(initialState, ih);
+
+  if (inMemory)
+    return std::make_unique<InMemoryPTree>(initialState);
+
+  return std::make_unique<NoopPTree>();
+};
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index dbee70dd..ab3f0433 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -10,57 +10,170 @@
 #ifndef KLEE_PTREE_H
 #define KLEE_PTREE_H
 
+#include "PTreeWriter.h"
+#include "UserSearcher.h"
 #include "klee/Core/BranchTypes.h"
+#include "klee/Core/TerminationTypes.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Support/ErrorHandling.h"
+
 #include "llvm/ADT/PointerIntPair.h"
+#include "llvm/Support/Casting.h"
+
+#include <cstdint>
+#include <variant>
 
 namespace klee {
-  class ExecutionState;
-  class PTreeNode;
-  /* PTreeNodePtr is used by the Random Path Searcher object to efficiently
-  record which PTreeNode belongs to it. PTree is a global structure that
-  captures all  states, whereas a Random Path Searcher might only care about
-  a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which
-  Random Path Searchers PTreeNode belongs to. */
-  constexpr int PtrBitCount = 3;
-  using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
-
-  class PTreeNode {
-  public:
-    PTreeNode *parent = nullptr;
-
-    PTreeNodePtr left; 
-    PTreeNodePtr right;
-    ExecutionState *state = nullptr;
-
-    PTreeNode(const PTreeNode&) = delete;
-    PTreeNode(PTreeNode *parent, ExecutionState *state);
-    ~PTreeNode() = default;
-  };
-
-  class PTree {
-    // Number of registered ID
-    int registeredIds = 0;
-
-  public:
-    PTreeNodePtr root;
-    explicit PTree(ExecutionState *initialState);
-    ~PTree() = default;
-
-    void attach(PTreeNode *node, ExecutionState *leftState,
-                ExecutionState *rightState, BranchType reason);
-    void remove(PTreeNode *node);
-    void dump(llvm::raw_ostream &os);
-    std::uint8_t getNextId() {
-      std::uint8_t id = 1 << registeredIds++;
-      if (registeredIds > PtrBitCount) {
-        klee_error("PTree cannot support more than %d RandomPathSearchers",
-                   PtrBitCount);
-      }
-      return id;
-    }
-  };
-}
+class ExecutionState;
+class Executor;
+class InMemoryPTree;
+class InterpreterHandler;
+class PTreeNode;
+class Searcher;
+
+/* PTreeNodePtr is used by the Random Path Searcher object to efficiently
+record which PTreeNode belongs to it. PTree is a global structure that
+captures all  states, whereas a Random Path Searcher might only care about
+a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which
+Random Path Searchers PTreeNode belongs to. */
+constexpr std::uint8_t PtrBitCount = 3;
+using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
+
+class PTreeNode {
+public:
+  enum class NodeType : std::uint8_t { Basic, Annotated };
+
+  PTreeNode *parent{nullptr};
+  PTreeNodePtr left;
+  PTreeNodePtr right;
+  ExecutionState *state{nullptr};
+
+  PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
+  virtual ~PTreeNode() = default;
+  PTreeNode(const PTreeNode &) = delete;
+  PTreeNode &operator=(PTreeNode const &) = delete;
+  PTreeNode(PTreeNode &&) = delete;
+  PTreeNode &operator=(PTreeNode &&) = delete;
+
+  [[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; }
+  static bool classof(const PTreeNode *N) { return true; }
+};
+
+class AnnotatedPTreeNode : public PTreeNode {
+  inline static std::uint32_t nextID{1};
+
+public:
+  std::uint32_t id{0};
+  std::uint32_t stateID{0};
+  std::uint32_t asmLine{0};
+  std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
+
+  AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
+  ~AnnotatedPTreeNode() override = default;
+
+  [[nodiscard]] NodeType getType() const override { return NodeType::Annotated; }
+  static bool classof(const PTreeNode *N) {
+    return N->getType() == NodeType::Annotated;
+  }
+};
+
+class PTree {
+public:
+  enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent };
+
+  /// Branch from PTreeNode and attach states, convention: rightState is
+  /// parent
+  virtual void attach(PTreeNode *node, ExecutionState *leftState,
+                      ExecutionState *rightState, BranchType reason) = 0;
+  /// Dump process tree in .dot format into os (debug)
+  virtual void dump(llvm::raw_ostream &os) = 0;
+  /// Remove node from tree
+  virtual void remove(PTreeNode *node) = 0;
+  /// Set termination type (on state removal)
+  virtual void setTerminationType(ExecutionState &state,
+                                  StateTerminationType type){}
+
+  virtual ~PTree() = default;
+  PTree(PTree const &) = delete;
+  PTree &operator=(PTree const &) = delete;
+  PTree(PTree &&) = delete;
+  PTree &operator=(PTree &&) = delete;
+
+  [[nodiscard]] virtual PTreeType getType() const = 0;
+  static bool classof(const PTreeNode *N) { return true; }
+
+protected:
+  explicit PTree() noexcept = default;
+};
+
+/// @brief A pseudo process tree that does not maintain any nodes.
+class NoopPTree final : public PTree {
+public:
+  NoopPTree() noexcept = default;
+  ~NoopPTree() override = default;
+  void attach(PTreeNode *node, ExecutionState *leftState,
+              ExecutionState *rightState,
+              BranchType reason) noexcept override{}
+  void dump(llvm::raw_ostream &os) noexcept override;
+  void remove(PTreeNode *node) noexcept override{}
+
+  [[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; };
+  static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; }
+};
+
+/// @brief An in-memory process tree required by RandomPathSearcher
+class InMemoryPTree : public PTree {
+public:
+  PTreeNodePtr root;
+
+private:
+  /// Number of registered IDs ("users", e.g. RandomPathSearcher)
+  std::uint8_t registeredIds = 0;
+
+  virtual PTreeNode *createNode(PTreeNode *parent, ExecutionState *state);
+  virtual void updateBranchingNode(PTreeNode &node, BranchType reason){}
+  virtual void updateTerminatingNode(PTreeNode &node){}
+
+public:
+  InMemoryPTree() noexcept = default;
+  explicit InMemoryPTree(ExecutionState &initialState) noexcept;
+  ~InMemoryPTree() override = default;
+
+  void attach(PTreeNode *node, ExecutionState *leftState,
+              ExecutionState *rightState, BranchType reason) noexcept override;
+  void dump(llvm::raw_ostream &os) noexcept override;
+  std::uint8_t getNextId() noexcept;
+  void remove(PTreeNode *node) noexcept override;
+
+  [[nodiscard]] PTreeType getType() const override { return PTreeType::InMemory; };
+  static bool classof(const PTree *T) {
+    return (T->getType() == PTreeType::InMemory) || (T->getType() == PTreeType::Persistent);
+  }
+};
+
+/// @brief An in-memory process tree that also writes its nodes into an SQLite
+/// database (ptree.db) with a PTreeWriter
+class PersistentPTree : public InMemoryPTree {
+  PTreeWriter writer;
+
+  PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override;
+  void updateBranchingNode(PTreeNode &node, BranchType reason) override;
+  void updateTerminatingNode(PTreeNode &node) override;
+
+public:
+  explicit PersistentPTree(ExecutionState &initialState,
+                           InterpreterHandler &ih) noexcept;
+  ~PersistentPTree() override = default;
+  void dump(llvm::raw_ostream &os) noexcept override;
+  void setTerminationType(ExecutionState &state,
+                          StateTerminationType type) override;
+
+  [[nodiscard]] PTreeType getType() const override { return PTreeType::Persistent; };
+  static bool classof(const PTree *T) { return T->getType() == PTreeType::Persistent; }
+};
+
+std::unique_ptr<PTree> createPTree(ExecutionState &initialState, bool inMemory,
+                                   InterpreterHandler &ih);
+} // namespace klee
 
 #endif /* KLEE_PTREE_H */
diff --git a/lib/Core/PTreeWriter.cpp b/lib/Core/PTreeWriter.cpp
new file mode 100644
index 00000000..a8067a5d
--- /dev/null
+++ b/lib/Core/PTreeWriter.cpp
@@ -0,0 +1,196 @@
+//===-- PTreeWriter.cpp ---------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "PTreeWriter.h"
+
+#include "PTree.h"
+#include "klee/Support/ErrorHandling.h"
+#include "klee/Support/OptionCategories.h"
+
+#include "llvm/Support/CommandLine.h"
+
+namespace {
+llvm::cl::opt<unsigned> BatchSize(
+    "ptree-batch-size", llvm::cl::init(100U),
+    llvm::cl::desc("Number of process tree nodes to batch for writing, "
+                   "see --write-ptree (default=100)"),
+    llvm::cl::cat(klee::PTreeCat));
+} // namespace
+
+using namespace klee;
+
+void prepare_statement(sqlite3 *db, const std::string &query, sqlite3_stmt **stmt) {
+  int result;
+#ifdef SQLITE_PREPARE_PERSISTENT
+  result = sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT,
+                              stmt, nullptr);
+#else
+  result = sqlite3_prepare_v3(db, query.c_str(), -1, 0, stmt, nullptr);
+#endif
+  if (result != SQLITE_OK) {
+    klee_warning("Process tree database: can't prepare query: %s [%s]",
+                 sqlite3_errmsg(db), query.c_str());
+    sqlite3_close(db);
+    klee_error("Process tree database: can't prepare query: %s", query.c_str());
+  }
+}
+
+PTreeWriter::PTreeWriter(const std::string &dbPath) {
+  // create database file
+  if (sqlite3_open(dbPath.c_str(), &db) != SQLITE_OK)
+    klee_error("Can't create process tree database: %s", sqlite3_errmsg(db));
+
+  // - set options: asynchronous + WAL
+  char *errMsg = nullptr;
+  if (sqlite3_exec(db, "PRAGMA synchronous = OFF;", nullptr, nullptr,
+                   &errMsg) != SQLITE_OK) {
+    klee_warning("Process tree database: can't set option: %s", errMsg);
+    sqlite3_free(errMsg);
+  }
+  if (sqlite3_exec(db, "PRAGMA journal_mode = WAL;", nullptr, nullptr,
+                   &errMsg) != SQLITE_OK) {
+    klee_warning("Process tree database: can't set option: %s", errMsg);
+    sqlite3_free(errMsg);
+  }
+
+  // - create table
+  std::string query =
+      "CREATE TABLE IF NOT EXISTS nodes ("
+      "ID INT PRIMARY KEY, stateID INT, leftID INT, rightID INT,"
+      "asmLine INT, kind INT);";
+  char *zErr = nullptr;
+  if (sqlite3_exec(db, query.c_str(), nullptr, nullptr, &zErr) != SQLITE_OK) {
+    klee_warning("Process tree database: initialisation error: %s", zErr);
+    sqlite3_free(zErr);
+    sqlite3_close(db);
+    klee_error("Process tree database: initialisation error.");
+  }
+
+  // create prepared statements
+  // - insertStmt
+  query = "INSERT INTO nodes VALUES (?, ?, ?, ?, ?, ?);";
+  prepare_statement(db, query, &insertStmt);
+  // - transactionBeginStmt
+  query = "BEGIN TRANSACTION";
+  prepare_statement(db, query, &transactionBeginStmt);
+  // - transactionCommitStmt
+  query = "COMMIT TRANSACTION";
+  prepare_statement(db, query, &transactionCommitStmt);
+
+  // begin transaction
+  if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) {
+    klee_warning("Process tree database: can't begin transaction: %s",
+                 sqlite3_errmsg(db));
+  }
+  if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) {
+    klee_warning("Process tree database: can't reset transaction: %s",
+                 sqlite3_errmsg(db));
+  }
+}
+
+PTreeWriter::~PTreeWriter() {
+  batchCommit(!flushed);
+
+  // finalize prepared statements
+  sqlite3_finalize(insertStmt);
+  sqlite3_finalize(transactionBeginStmt);
+  sqlite3_finalize(transactionCommitStmt);
+
+  // commit
+  if (sqlite3_exec(db, "END TRANSACTION", nullptr, nullptr, nullptr) !=
+      SQLITE_OK) {
+    klee_warning("Process tree database: can't end transaction: %s",
+                 sqlite3_errmsg(db));
+  }
+
+  if (sqlite3_close(db) != SQLITE_OK) {
+    klee_warning("Process tree database: can't close database: %s",
+                 sqlite3_errmsg(db));
+  }
+}
+
+void PTreeWriter::batchCommit(bool force) {
+  ++batch;
+  if (batch < BatchSize && !force)
+    return;
+
+  // commit and begin transaction
+  if (sqlite3_step(transactionCommitStmt) != SQLITE_DONE) {
+    klee_warning("Process tree database: transaction commit error: %s",
+                 sqlite3_errmsg(db));
+  }
+
+  if (sqlite3_reset(transactionCommitStmt) != SQLITE_OK) {
+    klee_warning("Process tree database: transaction reset error: %s",
+                 sqlite3_errmsg(db));
+  }
+
+  if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) {
+    klee_warning("Process tree database: transaction begin error: %s",
+                 sqlite3_errmsg(db));
+  }
+
+  if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) {
+    klee_warning("Process tree database: transaction reset error: %s",
+                 sqlite3_errmsg(db));
+  }
+
+  batch = 0;
+  flushed = true;
+}
+
+void PTreeWriter::write(const AnnotatedPTreeNode &node) {
+  unsigned rc = 0;
+
+  // bind values (SQLITE_OK is defined as 0 - just check success once at the
+  // end)
+  rc |= sqlite3_bind_int64(insertStmt, 1, node.id);
+  rc |= sqlite3_bind_int(insertStmt, 2, node.stateID);
+  rc |= sqlite3_bind_int64(
+      insertStmt, 3,
+      node.left.getPointer()
+          ? (static_cast<AnnotatedPTreeNode *>(node.left.getPointer()))->id
+          : 0);
+  rc |= sqlite3_bind_int64(
+      insertStmt, 4,
+      node.right.getPointer()
+          ? (static_cast<AnnotatedPTreeNode *>(node.right.getPointer()))->id
+          : 0);
+  rc |= sqlite3_bind_int(insertStmt, 5, node.asmLine);
+  std::uint8_t value{0};
+  if (std::holds_alternative<BranchType>(node.kind)) {
+    value = static_cast<std::uint8_t>(std::get<BranchType>(node.kind));
+  } else if (std::holds_alternative<StateTerminationType>(node.kind)) {
+    value =
+        static_cast<std::uint8_t>(std::get<StateTerminationType>(node.kind));
+  } else {
+    assert(false && "PTreeWriter: Illegal node kind!");
+  }
+  rc |= sqlite3_bind_int(insertStmt, 6, value);
+  if (rc != SQLITE_OK) {
+    // This is either a programming error (e.g. SQLITE_MISUSE) or we ran out of
+    // resources (e.g. SQLITE_NOMEM). Calling sqlite3_errmsg() after a possible
+    // successful call above is undefined, hence no error message here.
+    klee_error("Process tree database: can't persist data for node: %u",
+               node.id);
+  }
+
+  // insert
+  if (sqlite3_step(insertStmt) != SQLITE_DONE) {
+    klee_warning("Process tree database: can't persist data for node: %u: %s",
+                 node.id, sqlite3_errmsg(db));
+  }
+
+  if (sqlite3_reset(insertStmt) != SQLITE_OK) {
+    klee_warning("Process tree database: error reset node: %u: %s", node.id,
+                 sqlite3_errmsg(db));
+  }
+
+  batchCommit();
+}
diff --git a/lib/Core/PTreeWriter.h b/lib/Core/PTreeWriter.h
new file mode 100644
index 00000000..12709116
--- /dev/null
+++ b/lib/Core/PTreeWriter.h
@@ -0,0 +1,46 @@
+//===-- PTreeWriter.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include <sqlite3.h>
+
+#include <cstdint>
+#include <string>
+
+namespace klee {
+class AnnotatedPTreeNode;
+
+/// @brief Writes process tree nodes into an SQLite database
+class PTreeWriter {
+  friend class PersistentPTree;
+
+  ::sqlite3 *db{nullptr};
+  ::sqlite3_stmt *insertStmt{nullptr};
+  ::sqlite3_stmt *transactionBeginStmt{nullptr};
+  ::sqlite3_stmt *transactionCommitStmt{nullptr};
+  std::uint32_t batch{0};
+  bool flushed{true};
+
+  /// Writes nodes in batches
+  void batchCommit(bool force = false);
+
+public:
+  explicit PTreeWriter(const std::string &dbPath);
+  ~PTreeWriter();
+  PTreeWriter(const PTreeWriter &other) = delete;
+  PTreeWriter(PTreeWriter &&other) noexcept = delete;
+  PTreeWriter &operator=(const PTreeWriter &other) = delete;
+  PTreeWriter &operator=(PTreeWriter &&other) noexcept = delete;
+
+  /// Write new node into database
+  void write(const AnnotatedPTreeNode &node);
+};
+
+} // namespace klee
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index bf98ebc7..1c57eb4e 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -261,15 +261,18 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) {
 #define IS_OUR_NODE_VALID(n)                                                   \
   (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
 
-RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng)
-  : processTree{processTree},
-    theRNG{rng},
-    idBitMask{processTree.getNextId()} {};
+RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng)
+    : processTree{processTree}, theRNG{rng},
+      idBitMask{
+          static_cast<uint8_t>(processTree ? processTree->getNextId() : 0)} {
+
+  assert(processTree);
+};
 
 ExecutionState &RandomPathSearcher::selectState() {
   unsigned flips=0, bits=0;
-  assert(processTree.root.getInt() & idBitMask && "Root should belong to the searcher");
-  PTreeNode *n = processTree.root.getPointer();
+  assert(processTree->root.getInt() & idBitMask && "Root should belong to the searcher");
+  PTreeNode *n = processTree->root.getPointer();
   while (!n->state) {
     if (!IS_OUR_NODE_VALID(n->left)) {
       assert(IS_OUR_NODE_VALID(n->right) && "Both left and right nodes invalid");
@@ -302,7 +305,7 @@ void RandomPathSearcher::update(ExecutionState *current,
 
     childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
                                                               : &parent->right)
-                      : &processTree.root;
+                      : &processTree->root;
     while (pnode && !IS_OUR_NODE_VALID(*childPtr)) {
       childPtr->setInt(childPtr->getInt() | idBitMask);
       pnode = parent;
@@ -312,7 +315,7 @@ void RandomPathSearcher::update(ExecutionState *current,
       childPtr = parent
                      ? ((parent->left.getPointer() == pnode) ? &parent->left
                                                              : &parent->right)
-                     : &processTree.root;
+                     : &processTree->root;
     }
   }
 
@@ -325,7 +328,7 @@ void RandomPathSearcher::update(ExecutionState *current,
       auto childPtr =
           parent ? ((parent->left.getPointer() == pnode) ? &parent->left
                                                          : &parent->right)
-                 : &processTree.root;
+                 : &processTree->root;
       assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours");
       childPtr->setInt(childPtr->getInt() & ~idBitMask);
       pnode = parent;
@@ -336,7 +339,7 @@ void RandomPathSearcher::update(ExecutionState *current,
 }
 
 bool RandomPathSearcher::empty() {
-  return !IS_OUR_NODE_VALID(processTree.root);
+  return !IS_OUR_NODE_VALID(processTree->root);
 }
 
 void RandomPathSearcher::printName(llvm::raw_ostream &os) {
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index e399c616..ddd49264 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -172,7 +172,7 @@ namespace klee {
   ///
   /// The ownership bits are maintained in the update method.
   class RandomPathSearcher final : public Searcher {
-    PTree &processTree;
+    InMemoryPTree *processTree;
     RNG &theRNG;
 
     // Unique bitmask of this searcher
@@ -181,7 +181,7 @@ namespace klee {
   public:
     /// \param processTree The process tree.
     /// \param RNG A random number generator.
-    RandomPathSearcher(PTree &processTree, RNG &rng);
+    RandomPathSearcher(InMemoryPTree *processTree, RNG &rng);
     ~RandomPathSearcher() override = default;
 
     ExecutionState &selectState() override;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 488fba51..4589471c 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -480,12 +480,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
       state.constraints, e, res, state.queryMetaData);
   assert(success && "FIXME: Unhandled solver failure");
   if (res) {
-    if (SilentKleeAssume) {
-      executor.terminateState(state);
-    } else {
-      executor.terminateStateOnUserError(
-          state, "invalid klee_assume call (provably false)");
-    }
+    executor.terminateStateOnUserError(
+        state, "invalid klee_assume call (provably false)", !SilentKleeAssume);
   } else {
     executor.addConstraint(state, e);
   }
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 19ac3718..735075f1 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -100,9 +100,13 @@ bool userSearcherRequiresMD2U() {
           std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
 }
 
+bool userSearcherRequiresInMemoryPTree() {
+  return std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end();
+}
+
 } // namespace klee
 
-Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &processTree) {
+Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree *processTree) {
   Searcher *searcher = nullptr;
   switch (type) {
     case Searcher::DFS: searcher = new DFSSearcher(); break;
@@ -122,15 +126,15 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &process
 }
 
 Searcher *klee::constructUserSearcher(Executor &executor) {
-
-  Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, *executor.processTree);
+  auto *ptree = llvm::dyn_cast<InMemoryPTree>(executor.processTree.get());
+  Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, ptree);
 
   if (CoreSearch.size() > 1) {
     std::vector<Searcher *> s;
     s.push_back(searcher);
 
     for (unsigned i = 1; i < CoreSearch.size(); i++)
-      s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, *executor.processTree));
+      s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, ptree));
 
     searcher = new InterleavedSearcher(s);
   }
diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h
index b0df8239..fe75eb6d 100644
--- a/lib/Core/UserSearcher.h
+++ b/lib/Core/UserSearcher.h
@@ -16,6 +16,7 @@ namespace klee {
 
   // XXX gross, should be on demand?
   bool userSearcherRequiresMD2U();
+  bool userSearcherRequiresInMemoryPTree();
 
   void initializeSearchOptions();
 
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index b4716dae..ae038b80 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -147,7 +147,7 @@ file(GENERATE
 
 add_custom_target(systemtests
   COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
-  DEPENDS klee kleaver klee-replay kleeRuntest ktest-gen ktest-randgen
+  DEPENDS klee kleaver klee-ptree klee-replay kleeRuntest ktest-gen ktest-randgen
   COMMENT "Running system tests"
   USES_TERMINAL
 )
diff --git a/test/Feature/KleePtreeBogus.test b/test/Feature/KleePtreeBogus.test
new file mode 100644
index 00000000..11fe87c8
--- /dev/null
+++ b/test/Feature/KleePtreeBogus.test
@@ -0,0 +1,65 @@
+REQUIRES: sqlite3
+
+fail on broken db (not sqlite)
+RUN: not %klee-ptree tree-info %S/ptree-dbs/not_a.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-CORRUPT -input-file=%t.err %s
+CHECK-CORRUPT: Can't prepare read statement: file is not a database
+
+empty tree
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/empty_db.csv nodes" 
+RUN: %klee-ptree tree-info %t.db > %t.err
+RUN: FileCheck -check-prefix=CHECK-EMPTY -input-file=%t.err %s
+CHECK-EMPTY: Empty tree.
+
+fail on tree with duplicate node IDs
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/duplicated_node.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-DUP -input-file=%t.err %s
+CHECK-DUP: PTree DB contains duplicate child reference or circular structure. Affected node: 2
+
+fail on invalid branch type
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_btype.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-BTYPE -input-file=%t.err %s
+CHECK-BTYPE: PTree DB contains unknown branch type (123) in node 1
+
+fail on invalid termination type
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_ttype.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-TTYPE -input-file=%t.err %s
+CHECK-TTYPE: PTree DB contains unknown termination type (123) in node 3
+
+fail on tree with looping nodes
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/loop.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-LOOP -input-file=%t.err %s
+CHECK-LOOP: PTree DB contains duplicate child reference or circular structure. Affected node: 1
+
+fail on tree with missing node (child node ID > max. ID)
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_after_max.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-MISSA -input-file=%t.err %s
+CHECK-MISSA: PTree DB contains references to non-existing nodes (> max. ID) in node 3
+
+fail on tree with missing node (child node ID < max. ID)
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_before_max.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-MISSB -input-file=%t.err %s
+CHECK-MISSB: PTree DB references undefined node. Affected node: 4
+
+fail on illegal node ID (0)
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/node_id0.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-ID0 -input-file=%t.err %s
+CHECK-ID0: PTree DB contains illegal node ID (0)
+
+cleanup
+RUN rm -f %t.db
diff --git a/test/Feature/WritePtree.c b/test/Feature/WritePtree.c
new file mode 100644
index 00000000..e7bf59ce
--- /dev/null
+++ b/test/Feature/WritePtree.c
@@ -0,0 +1,78 @@
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -write-ptree --output-dir=%t.klee-out %t.bc
+// RUN: %klee-ptree branches %t.klee-out/ptree.db | FileCheck --check-prefix=CHECK-BRANCH %s
+// RUN: %klee-ptree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s
+// RUN: %klee-ptree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s
+// RUN: %klee-ptree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s
+// RUN: %klee-ptree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s
+// RUN: %klee-ptree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s
+// RUN: not %klee-ptree dot %t.klee-out/ptree-doesnotexist.db
+
+#include "klee/klee.h"
+
+#include <stddef.h>
+
+int main(void) {
+  int a = 42;
+  int c0, c1, c2, c3;
+  klee_make_symbolic(&c0, sizeof(c0), "c0");
+  klee_make_symbolic(&c1, sizeof(c1), "c1");
+  klee_make_symbolic(&c2, sizeof(c2), "c2");
+  klee_make_symbolic(&c3, sizeof(c3), "c3");
+
+  if (c0) {
+    a += 17;
+  } else {
+    a -= 4;
+  }
+
+  if (c1) {
+    klee_assume(!c1);
+  } else if (c2) {
+    char *p = NULL;
+    p[4711] = '!';
+  } else if (c3) {
+    klee_silent_exit(0);
+  } else {
+    return a;
+  }
+
+  return 0;
+}
+
+// CHECK-BRANCH: branch type,count
+// CHECK-BRANCH: Conditional,7
+
+// CHECK-DEPTH: depth,count
+// CHECK-DEPTH: 3,2
+// CHECK-DEPTH: 4,2
+// CHECK-DEPTH: 5,4
+
+// CHECK-INSTR: asm line,branches,terminations,termination types
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,User(2)
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Ptr(2)
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,SilentExit(2)
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Exit(2)
+
+// CHECK-TERM: termination type,count
+// CHECK-TERM-DAG: Exit,2
+// CHECK-TERM-DAG: Ptr,2
+// CHECK-TERM-DAG: User,2
+// CHECK-TERM-DAG: SilentExit,2
+
+// CHECK-DOT: strict digraph PTree {
+// CHECK-DOT: node[shape=point,width=0.15,color=darkgrey];
+// CHECK-DOT: edge[color=darkgrey];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Conditional\nnode: {{[0-9]+}}\nstate: 0\nasm: {{[0-9]+}}"];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Exit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=green];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="SilentExit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=orange];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Ptr\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=red];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="User\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=blue];
+// CHECK-DOT-DAG: N{{[0-9]+}}->{N{{[0-9]+}} N{{[0-9]+}}};
+// CHECK-DOT-DAG: }
+
+// CHECK-TINFO: nodes: 15
+// CHECK-TINFO: leaf nodes: 8
+// CHECK-TINFO: max. depth: 5
+// CHECK-TINFO: avg. depth: 4.2
diff --git a/test/Feature/ptree-dbs/duplicated_node.csv b/test/Feature/ptree-dbs/duplicated_node.csv
new file mode 100644
index 00000000..7882b911
--- /dev/null
+++ b/test/Feature/ptree-dbs/duplicated_node.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,2,62,1
+4,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/empty_db.csv b/test/Feature/ptree-dbs/empty_db.csv
new file mode 100644
index 00000000..4dac8a17
--- /dev/null
+++ b/test/Feature/ptree-dbs/empty_db.csv
@@ -0,0 +1 @@
+ID,stateID,leftID,rightID,asmLine,kind
diff --git a/test/Feature/ptree-dbs/invalid_btype.csv b/test/Feature/ptree-dbs/invalid_btype.csv
new file mode 100644
index 00000000..01ee428c
--- /dev/null
+++ b/test/Feature/ptree-dbs/invalid_btype.csv
@@ -0,0 +1,4 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,123
+2,0,0,0,61,36
+3,1,0,0,61,1
diff --git a/test/Feature/ptree-dbs/invalid_ttype.csv b/test/Feature/ptree-dbs/invalid_ttype.csv
new file mode 100644
index 00000000..0d185bee
--- /dev/null
+++ b/test/Feature/ptree-dbs/invalid_ttype.csv
@@ -0,0 +1,4 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,0,0,61,123
diff --git a/test/Feature/ptree-dbs/loop.csv b/test/Feature/ptree-dbs/loop.csv
new file mode 100644
index 00000000..4fc2b9f2
--- /dev/null
+++ b/test/Feature/ptree-dbs/loop.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,1,62,1
+4,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/missing_after_max.csv b/test/Feature/ptree-dbs/missing_after_max.csv
new file mode 100644
index 00000000..16e99a35
--- /dev/null
+++ b/test/Feature/ptree-dbs/missing_after_max.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,5,62,1
+4,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/missing_before_max.csv b/test/Feature/ptree-dbs/missing_before_max.csv
new file mode 100644
index 00000000..2131ea56
--- /dev/null
+++ b/test/Feature/ptree-dbs/missing_before_max.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,5,62,1
+5,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/node_id0.csv b/test/Feature/ptree-dbs/node_id0.csv
new file mode 100644
index 00000000..51a31e49
--- /dev/null
+++ b/test/Feature/ptree-dbs/node_id0.csv
@@ -0,0 +1,6 @@
+ID,stateID,leftID,rightID,asmLine,kind
+0,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,5,62,1
+4,1,0,0,63,80
+5,2,0,0,63,36
diff --git a/test/Feature/ptree-dbs/not_a.db b/test/Feature/ptree-dbs/not_a.db
new file mode 100644
index 00000000..d81cc071
--- /dev/null
+++ b/test/Feature/ptree-dbs/not_a.db
@@ -0,0 +1 @@
+42
diff --git a/test/lit.cfg b/test/lit.cfg
index cb47d3d4..8abf7012 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -116,6 +116,11 @@ config.substitutions.append(
   ('%libkleeruntest', config.libkleeruntest)
 )
 
+# Add a substition for sqlite3
+config.substitutions.append(
+  ('%sqlite3', os.path.abspath(config.sqlite3))
+)
+
 # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line
 # e.g. llvm-lit --param klee_opts=--help
 klee_extra_params = lit_config.params.get('klee_opts',"")
@@ -134,6 +139,7 @@ if len(kleaver_extra_params) != 0:
 # If a tool's name is a prefix of another, the longer name has
 # to come first, e.g., klee-replay should come before klee
 subs = [ ('%kleaver', 'kleaver', kleaver_extra_params),
+         ('%klee-ptree', 'klee-ptree', ''),
          ('%klee-replay', 'klee-replay', ''),
          ('%klee-stats', 'klee-stats', ''),
          ('%klee-zesti', 'klee-zesti', ''),
@@ -233,3 +239,6 @@ config.available_features.add('{}32bit-support'.format('' if config.have_32bit_s
 config.available_features.add('{}asan'.format('' if config.have_asan else 'not-'))
 config.available_features.add('{}ubsan'.format('' if config.have_ubsan else 'not-'))
 config.available_features.add('{}msan'.format('' if config.have_msan else 'not-'))
+
+# SQLite
+config.available_features.add('{}sqlite3'.format('' if config.have_sqlite3 else 'not-'))
diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in
index c7063057..d82b8a2c 100644
--- a/test/lit.site.cfg.in
+++ b/test/lit.site.cfg.in
@@ -26,6 +26,8 @@ config.cxx = "@NATIVE_CXX@"
 #       test/Concrete/CMakeLists.txt
 config.O0opt = "-O0 -Xclang -disable-O0-optnone"
 
+config.sqlite3 = "@SQLITE_CLI@"
+
 # Features
 config.enable_uclibc = True if @SUPPORT_KLEE_UCLIBC@ == 1 else False
 config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False
@@ -39,6 +41,7 @@ config.have_asan = True if @IS_ASAN_BUILD@ == 1 else False
 config.have_ubsan = True if @IS_UBSAN_BUILD@ == 1 else False
 config.have_msan = True if @IS_MSAN_BUILD@ == 1 else False
 config.have_32bit_support = True if @M32_SUPPORTED@ == 1 else False
+config.have_sqlite3 = True if "@SQLITE_CLI@".strip() != "" else False
 
 # Add sanitizer list
 config.environment['LSAN_OPTIONS'] = "suppressions=@KLEE_UTILS_DIR@/sanitizers/lsan.txt"
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
index b641885c..40089c40 100644
--- a/tools/CMakeLists.txt
+++ b/tools/CMakeLists.txt
@@ -10,6 +10,7 @@ add_subdirectory(ktest-gen)
 add_subdirectory(ktest-randgen)
 add_subdirectory(kleaver)
 add_subdirectory(klee)
+add_subdirectory(klee-ptree)
 add_subdirectory(klee-replay)
 add_subdirectory(klee-stats)
 add_subdirectory(klee-zesti)
diff --git a/tools/klee-ptree/CMakeLists.txt b/tools/klee-ptree/CMakeLists.txt
new file mode 100644
index 00000000..b5c3fa09
--- /dev/null
+++ b/tools/klee-ptree/CMakeLists.txt
@@ -0,0 +1,16 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+add_executable(klee-ptree main.cpp Tree.cpp DFSVisitor.cpp Printers.cpp)
+
+target_compile_features(klee-ptree PRIVATE cxx_std_17)
+target_include_directories(klee-ptree PRIVATE ${KLEE_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS})
+target_link_libraries(klee-ptree PUBLIC ${SQLite3_LIBRARIES})
+
+install(TARGETS klee-ptree DESTINATION bin)
diff --git a/tools/klee-ptree/DFSVisitor.cpp b/tools/klee-ptree/DFSVisitor.cpp
new file mode 100644
index 00000000..c87afc3e
--- /dev/null
+++ b/tools/klee-ptree/DFSVisitor.cpp
@@ -0,0 +1,46 @@
+//===-- DFSVisitor.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "DFSVisitor.h"
+
+#include <utility>
+
+DFSVisitor::DFSVisitor(const Tree &tree, callbackT cb_intermediate,
+                       callbackT cb_leaf) noexcept
+    : tree{tree},
+      cb_intermediate{std::move(cb_intermediate)}, cb_leaf{std::move(cb_leaf)} {
+  run();
+}
+
+void DFSVisitor::run() const noexcept {
+  // empty tree
+  if (tree.nodes.size() <= 1)
+    return;
+
+  std::vector<std::tuple<std::uint32_t, std::uint32_t>> stack{
+      {1, 1}}; // (id, depth)
+  while (!stack.empty()) {
+    std::uint32_t id, depth;
+    std::tie(id, depth) = stack.back();
+    stack.pop_back();
+    const auto &node = tree.nodes[id];
+
+    if (node.left || node.right) {
+      if (cb_intermediate)
+        cb_intermediate(id, node, depth);
+      if (node.right)
+        stack.emplace_back(node.right, depth + 1);
+      if (node.left)
+        stack.emplace_back(node.left, depth + 1);
+    } else {
+      if (cb_leaf)
+        cb_leaf(id, node, depth);
+    }
+  }
+}
diff --git a/tools/klee-ptree/DFSVisitor.h b/tools/klee-ptree/DFSVisitor.h
new file mode 100644
index 00000000..60d7b3bd
--- /dev/null
+++ b/tools/klee-ptree/DFSVisitor.h
@@ -0,0 +1,31 @@
+//===-- DFSVisitor.h --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include "Tree.h"
+
+#include <functional>
+
+/// @brief Traverses a process tree and calls registered callbacks for
+/// intermediate and leaf nodes (not the classical Visitor pattern).
+class DFSVisitor {
+  // void _(node ID, node, depth)
+  using callbackT = std::function<void(std::uint32_t, Node, std::uint32_t)>;
+
+  const Tree &tree;
+  callbackT cb_intermediate;
+  callbackT cb_leaf;
+  void run() const noexcept;
+
+public:
+  DFSVisitor(const Tree &tree, callbackT cb_intermediate,
+             callbackT cb_leaf) noexcept;
+  ~DFSVisitor() = default;
+};
diff --git a/tools/klee-ptree/Printers.cpp b/tools/klee-ptree/Printers.cpp
new file mode 100644
index 00000000..950d1b09
--- /dev/null
+++ b/tools/klee-ptree/Printers.cpp
@@ -0,0 +1,266 @@
+//===-- Printers.cpp --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Printers.h"
+
+#include "DFSVisitor.h"
+#include "klee/Core/BranchTypes.h"
+#include "klee/Core/TerminationTypes.h"
+
+#include <algorithm>
+#include <array>
+#include <cstdlib>
+#include <iostream>
+#include <map>
+#include <string>
+#include <string_view>
+#include <unordered_map>
+
+// branches
+
+void printBranches(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  std::unordered_map<BranchType, std::uint32_t> branchTypes;
+
+  DFSVisitor visitor(
+      tree,
+      [&branchTypes](std::uint32_t id, Node node, std::uint32_t depth) {
+        branchTypes[std::get<BranchType>(node.kind)]++;
+      },
+      nullptr);
+
+  // sort output
+  std::vector<std::pair<BranchType, std::uint32_t>> sortedBranchTypes(
+      branchTypes.begin(), branchTypes.end());
+  std::sort(sortedBranchTypes.begin(), sortedBranchTypes.end(),
+            [](const auto &lhs, const auto &rhs) {
+              return (lhs.second > rhs.second) ||
+                     (lhs.second == rhs.second && lhs.first < rhs.first);
+            });
+
+  std::cout << "branch type,count\n";
+  for (const auto &[branchType, count] : sortedBranchTypes)
+    std::cout << branchTypeNames[branchType] << ',' << count << '\n';
+}
+
+// depths
+
+struct DepthInfo {
+  std::vector<std::uint32_t> depths;
+  std::uint32_t maxDepth{0};
+  std::uint32_t noLeaves{0};
+  std::uint32_t noNodes{0};
+};
+
+DepthInfo getDepthInfo(const Tree &tree) {
+  DepthInfo I;
+
+  DFSVisitor visitor(
+      tree,
+      [&](std::uint32_t id, Node node, std::uint32_t depth) { ++I.noNodes; },
+      [&I](std::uint32_t id, Node node, std::uint32_t depth) {
+        ++I.noLeaves;
+        ++I.noNodes;
+        if (depth > I.maxDepth)
+          I.maxDepth = depth;
+        if (depth >= I.depths.size())
+          I.depths.resize(depth + 1, 0);
+        ++I.depths[depth];
+      });
+
+  return I;
+}
+
+void printDepths(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  const auto DI = getDepthInfo(tree);
+  std::cout << "depth,count\n";
+  for (size_t depth = 1; depth <= DI.maxDepth; ++depth) {
+    auto count = DI.depths[depth];
+    if (count)
+      std::cout << depth << ',' << count << '\n';
+  }
+}
+
+// dot
+
+std::array<std::string, 6> NodeColours = {"green", "orange",   "red",
+                                          "blue",  "darkblue", "darkgrey"};
+
+std::string_view terminationTypeColour(StateTerminationType type) {
+  // Exit
+  if (type == StateTerminationType::Exit)
+    return NodeColours[0];
+
+  // Early
+  if ((StateTerminationType::EXIT < type &&
+       type <= StateTerminationType::EARLY) ||
+      (StateTerminationType::EXECERR < type &&
+       type <= StateTerminationType::END)) {
+    return NodeColours[1];
+  }
+
+  // Program error
+  if (StateTerminationType::SOLVERERR < type &&
+      type <= StateTerminationType::PROGERR)
+    return NodeColours[2];
+
+  // User error
+  if (StateTerminationType::PROGERR < type &&
+      type <= StateTerminationType::USERERR)
+    return NodeColours[3];
+
+  // Execution/Solver error
+  if ((StateTerminationType::USERERR < type &&
+       type <= StateTerminationType::EXECERR) ||
+      (StateTerminationType::EARLY < type &&
+       type <= StateTerminationType::SOLVERERR))
+    return NodeColours[4];
+
+  return NodeColours[5];
+}
+
+void printIntermediateNode(std::uint32_t id, Node node, std::uint32_t depth) {
+  std::cout << 'N' << id << '[' << "tooltip=\""
+            << branchTypeNames[std::get<BranchType>(node.kind)] << "\\n"
+            << "node: " << id << "\\nstate: " << node.stateID
+            << "\\nasm: " << node.asmLine << "\"];\n";
+}
+
+void printLeafNode(std::uint32_t id, Node node, std::uint32_t depth) {
+  const auto terminationType = std::get<StateTerminationType>(node.kind);
+  const auto colour = terminationTypeColour(terminationType);
+  std::cout << 'N' << id << '[' << "tooltip=\""
+            << terminationTypeNames[terminationType] << "\\n"
+            << "node: " << id << "\\nstate: " << node.stateID
+            << "\\nasm: " << node.asmLine << "\",color=" << colour << "];\n";
+}
+
+void printEdges(std::uint32_t id, Node node, std::uint32_t depth) {
+  std::cout << 'N' << id << "->{";
+  if (node.left && node.right) {
+    std::cout << 'N' << node.left << " N" << node.right;
+  } else {
+    std::cout << 'N' << (node.left ? node.left : node.right);
+  }
+  std::cout << "};\n";
+}
+
+void printDOT(const Tree &tree) {
+  // header
+  // - style defaults to intermediate nodes
+  std::cout << "strict digraph PTree {\n"
+               "node[shape=point,width=0.15,color=darkgrey];\n"
+               "edge[color=darkgrey];\n\n";
+
+  // nodes
+  // - change colour for leaf nodes
+  // - attach branch and location info as tooltips
+  DFSVisitor nodeVisitor(tree, printIntermediateNode, printLeafNode);
+
+  // edges
+  DFSVisitor edgeVisitor(tree, printEdges, nullptr);
+
+  // footer
+  std::cout << '}' << std::endl;
+}
+
+// instructions
+
+struct Info {
+  std::uint32_t noBranches{0};
+  std::uint32_t noTerminations{0};
+  std::map<StateTerminationType, std::uint32_t> terminationTypes;
+};
+
+void printInstructions(const Tree &tree) {
+  std::map<std::uint32_t, Info> asmInfo;
+
+  DFSVisitor visitor(
+      tree,
+      [&asmInfo](std::uint32_t id, Node node, std::uint32_t depth) {
+        asmInfo[node.asmLine].noBranches++;
+      },
+      [&asmInfo](std::uint32_t id, Node node, std::uint32_t depth) {
+        auto &info = asmInfo[node.asmLine];
+        info.noTerminations++;
+        info.terminationTypes[std::get<StateTerminationType>(node.kind)]++;
+      });
+
+  std::cout << "asm line,branches,terminations,termination types\n";
+  for (const auto &[asmLine, info] : asmInfo) {
+    std::cout << asmLine << ',' << info.noBranches << ',' << info.noTerminations
+              << ',';
+    std::string sep{""};
+    for (const auto &[terminationType, count] : info.terminationTypes) {
+      std::cout << sep << terminationTypeNames[terminationType] << '(' << count
+                << ')';
+      sep = ";";
+    }
+    std::cout << '\n';
+  }
+}
+
+// terminations
+
+void printTerminations(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  std::map<StateTerminationType, std::uint32_t> terminations;
+
+  DFSVisitor visitor(
+      tree, nullptr,
+      [&terminations](std::uint32_t id, Node node, std::uint32_t depth) {
+        terminations[std::get<StateTerminationType>(node.kind)]++;
+      });
+
+  std::cout << "termination type,count\n";
+  for (const auto &[terminationType, count] : terminations)
+    std::cout << terminationTypeNames[terminationType] << ',' << count << '\n';
+}
+
+// tree info
+
+void printTreeInfo(const Tree &tree) {
+  if (tree.nodes.size() <= 1) {
+    std::cout << "Empty tree.\n";
+    return;
+  }
+
+  const auto DI = getDepthInfo(tree);
+
+  // determine average depth
+  std::uint64_t sum{0};
+  for (size_t depth = 1; depth <= DI.maxDepth; ++depth) {
+    auto count = DI.depths[depth];
+    if (count)
+      sum += count * depth;
+  }
+  double avgDepth = (double)sum / DI.noLeaves;
+
+  std::cout << "nodes: " << DI.noNodes << '\n'
+            << "leaf nodes: " << DI.noLeaves
+            << (DI.noNodes && (DI.noLeaves != DI.noNodes / 2 + 1)
+                    ? " (not a binary tree?!)"
+                    : "")
+            << '\n'
+            << "max. depth: " << DI.maxDepth << '\n'
+            << "avg. depth: " << std::setprecision(2) << avgDepth << '\n';
+}
diff --git a/tools/klee-ptree/Printers.h b/tools/klee-ptree/Printers.h
new file mode 100644
index 00000000..d20db4a1
--- /dev/null
+++ b/tools/klee-ptree/Printers.h
@@ -0,0 +1,30 @@
+//===-- Printers.h ----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include "Tree.h"
+
+/// print branch types in csv format
+void printBranches(const Tree &tree);
+
+/// print depths in csv format
+void printDepths(const Tree &tree);
+
+/// print tree in dot format
+void printDOT(const Tree &tree);
+
+/// print instruction information in csv format
+void printInstructions(const Tree &tree);
+
+/// print termination types in csv format
+void printTerminations(const Tree &tree);
+
+/// print tree/node information
+void printTreeInfo(const Tree &tree);
diff --git a/tools/klee-ptree/Tree.cpp b/tools/klee-ptree/Tree.cpp
new file mode 100644
index 00000000..20772600
--- /dev/null
+++ b/tools/klee-ptree/Tree.cpp
@@ -0,0 +1,208 @@
+//===-- Tree.cpp ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Tree.h"
+
+#include <sqlite3.h>
+
+#include <cassert>
+#include <cstdlib>
+#include <iostream>
+
+Tree::Tree(const std::filesystem::path &path) {
+  // open db
+  ::sqlite3 *db;
+  if (sqlite3_open_v2(path.c_str(), &db, SQLITE_OPEN_READONLY, nullptr) !=
+      SQLITE_OK) {
+    std::cerr << "Can't open process tree database: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // initialise prepared statement
+  ::sqlite3_stmt *readStmt;
+  std::string query{
+      "SELECT ID, stateID, leftID, rightID, asmLine, kind FROM nodes;"};
+  if (sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT,
+                         &readStmt, nullptr) != SQLITE_OK) {
+    std::cerr << "Can't prepare read statement: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  ::sqlite3_stmt *maxStmt;
+  query = "SELECT MAX(ID) FROM nodes;";
+  if (sqlite3_prepare_v3(db, query.c_str(), -1, SQLITE_PREPARE_PERSISTENT,
+                         &maxStmt, nullptr) != SQLITE_OK) {
+    std::cerr << "Can't prepare max statement: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // read max id
+  int rc;
+  std::uint64_t maxID;
+  if ((rc = sqlite3_step(maxStmt)) == SQLITE_ROW) {
+    maxID = static_cast<std::uint32_t>(sqlite3_column_int(maxStmt, 0));
+  } else {
+    std::cerr << "Can't read maximum ID: " << sqlite3_errmsg(db) << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // reserve space
+  nodes.resize(maxID + 1, {});
+
+  // read rows into vector
+  while ((rc = sqlite3_step(readStmt)) == SQLITE_ROW) {
+    const auto ID = static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 0));
+    const auto stateID =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 1));
+    const auto left =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 2));
+    const auto right =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 3));
+    const auto asmLine =
+        static_cast<std::uint32_t>(sqlite3_column_int(readStmt, 4));
+    const auto tmpKind =
+        static_cast<std::uint8_t>(sqlite3_column_int(readStmt, 5));
+
+    // sanity checks: valid indices
+    if (ID == 0) {
+      std::cerr << "PTree DB contains illegal node ID (0)" << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    if (left > maxID || right > maxID) {
+      std::cerr << "PTree DB contains references to non-existing nodes (> max. "
+                   "ID) in node "
+                << ID << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    if ((left == 0 && right != 0) || (left != 0 && right == 0)) {
+      std::cerr << "Warning: PTree DB contains ambiguous node (0 vs. non-0 "
+                   "children): "
+                << ID << std::endl;
+    }
+
+    // determine node kind (branch or leaf node)
+    decltype(Node::kind) kind;
+    if (left == 0 && right == 0) {
+      kind = static_cast<StateTerminationType>(tmpKind);
+    } else {
+      kind = static_cast<BranchType>(tmpKind);
+    }
+
+    // store children
+    nodes[ID] = {.left = left,
+                 .right = right,
+                 .stateID = stateID,
+                 .asmLine = asmLine,
+                 .kind = kind};
+  }
+
+  if (rc != SQLITE_DONE) {
+    std::cerr << "Error while reading database: " << sqlite3_errmsg(db)
+              << std::endl;
+    exit(EXIT_FAILURE);
+  }
+
+  // close db
+  sqlite3_finalize(maxStmt);
+  sqlite3_finalize(readStmt);
+  sqlite3_close(db);
+
+  // initialise global sets/maps and sanity check
+  initialiseValidTypes();
+  sanityCheck();
+  initialiseTypeNames();
+}
+
+void Tree::initialiseTypeNames() {
+// branch types
+#undef BTYPE
+#define BTYPE(Name, I) branchTypeNames[BranchType::Name] = #Name;
+  BRANCH_TYPES
+
+// termination types
+#undef TTYPE
+#define TTYPE(Name, I, S)                                                      \
+  terminationTypeNames[StateTerminationType::Name] = #Name;
+  TERMINATION_TYPES
+}
+
+void Tree::initialiseValidTypes() {
+// branch types
+#undef BTYPE
+#define BTYPE(Name, I) validBranchTypes.insert(BranchType::Name);
+  BRANCH_TYPES
+
+// termination types
+#undef TTYPE
+#define TTYPE(Name, I, S)                                                      \
+  validTerminationTypes.insert(StateTerminationType::Name);
+  TERMINATION_TYPES
+}
+
+void Tree::sanityCheck() {
+  if (nodes.size() <= 1) // [0] is unused
+    return;
+
+  std::vector<std::uint32_t> stack{1}; // root ID
+  std::unordered_set<std::uint32_t> visited;
+  while (!stack.empty()) {
+    const auto id = stack.back();
+    stack.pop_back();
+
+    if (!visited.insert(id).second) {
+      std::cerr << "PTree DB contains duplicate child reference or circular "
+                   "structure. Affected node: "
+                << id << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    const auto &node = nodes[id];
+
+    // default constructed "gap" in vector
+    if (!node.left && !node.right &&
+        std::holds_alternative<BranchType>(node.kind) &&
+        static_cast<std::uint8_t>(std::get<BranchType>(node.kind)) == 0u) {
+      std::cerr << "PTree DB references undefined node. Affected node: " << id
+                << std::endl;
+      exit(EXIT_FAILURE);
+    }
+
+    if (node.left || node.right) {
+      if (node.right)
+        stack.push_back(node.right);
+      if (node.left)
+        stack.push_back(node.left);
+      // valid branch types
+      assert(std::holds_alternative<BranchType>(node.kind));
+      const auto branchType = std::get<BranchType>(node.kind);
+      if (validBranchTypes.count(branchType) == 0) {
+        std::cerr << "PTree DB contains unknown branch type ("
+                  << (unsigned)static_cast<std::uint8_t>(branchType)
+                  << ") in node " << id << std::endl;
+        exit(EXIT_FAILURE);
+      }
+    } else {
+      // valid termination types
+      assert(std::holds_alternative<StateTerminationType>(node.kind));
+      const auto terminationType = std::get<StateTerminationType>(node.kind);
+      if (validTerminationTypes.count(terminationType) == 0 ||
+          terminationType == StateTerminationType::RUNNING) {
+        std::cerr << "PTree DB contains unknown termination type ("
+                  << (unsigned)static_cast<std::uint8_t>(terminationType)
+                  << ") in node " << id << std::endl;
+        exit(EXIT_FAILURE);
+      }
+    }
+  }
+}
diff --git a/tools/klee-ptree/Tree.h b/tools/klee-ptree/Tree.h
new file mode 100644
index 00000000..65b7baeb
--- /dev/null
+++ b/tools/klee-ptree/Tree.h
@@ -0,0 +1,53 @@
+//===-- Tree.h --------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#pragma once
+
+#include "klee/Core/BranchTypes.h"
+#include "klee/Core/TerminationTypes.h"
+
+#include <filesystem>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+#include <variant>
+#include <vector>
+
+inline std::unordered_set<BranchType> validBranchTypes;
+inline std::unordered_set<StateTerminationType> validTerminationTypes;
+inline std::unordered_map<BranchType, std::string> branchTypeNames;
+inline std::unordered_map<StateTerminationType, std::string>
+    terminationTypeNames;
+
+///@brief A Tree node representing a PTreeNode
+struct Node final {
+  std::uint32_t left{0};
+  std::uint32_t right{0};
+  std::uint32_t stateID{0};
+  std::uint32_t asmLine{0};
+  std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
+};
+
+///@brief An in-memory representation of a complete process tree
+class Tree final {
+  /// Creates branchTypeNames and terminationTypeNames maps
+  static void initialiseTypeNames();
+  /// Creates validBranchTypes and validTerminationTypes sets
+  static void initialiseValidTypes();
+  /// Checks tree properties (e.g. valid branch/termination types)
+  void sanityCheck();
+
+public:
+  /// sorted vector of Nodes default initialised with BranchType::NONE
+  std::vector<Node> nodes; // PTree node IDs start with 1!
+
+  /// Reads complete ptree.db into memory
+  explicit Tree(const std::filesystem::path &path);
+  ~Tree() = default;
+};
diff --git a/tools/klee-ptree/main.cpp b/tools/klee-ptree/main.cpp
new file mode 100644
index 00000000..96d2be75
--- /dev/null
+++ b/tools/klee-ptree/main.cpp
@@ -0,0 +1,68 @@
+//===-- main.cpp ------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <cstdlib>
+#include <filesystem>
+#include <iostream>
+
+#include "Printers.h"
+
+namespace fs = std::filesystem;
+
+void print_usage() {
+  std::cout << "Usage: klee-ptree <option> /path[/ptree.db]\n\n"
+               "Options:\n"
+               "\tbranches     -  print branch statistics in csv format\n"
+               "\tdepths       -  print depths statistics in csv format\n"
+               "\tinstructions -  print asm line summary in csv format\n"
+               "\tterminations -  print termination statistics in csv format\n"
+               "\ttree-dot     -  print tree in dot format\n"
+               "\ttree-info    -  print tree statistics"
+               "\n";
+}
+
+int main(int argc, char *argv[]) {
+  if (argc != 3) {
+    print_usage();
+    exit(EXIT_FAILURE);
+  }
+
+  // parse options
+  void (*action)(const Tree &);
+  std::string option(argv[1]);
+  if (option == "branches") {
+    action = printBranches;
+  } else if (option == "instructions") {
+    action = printInstructions;
+  } else if (option == "depths") {
+    action = printDepths;
+  } else if (option == "terminations") {
+    action = printTerminations;
+  } else if (option == "tree-dot") {
+    action = printDOT;
+  } else if (option == "tree-info") {
+    action = printTreeInfo;
+  } else {
+    print_usage();
+    exit(EXIT_FAILURE);
+  }
+
+  // create tree
+  fs::path path{argv[2]};
+  if (fs::is_directory(path))
+    path /= "ptree.db";
+  if (!fs::exists(path)) {
+    std::cerr << "Cannot open " << path << '\n';
+    exit(EXIT_FAILURE);
+  }
+  Tree tree(path);
+
+  // print results
+  action(tree);
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index a3062d24..ce231967 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1123,7 +1123,7 @@ int main(int argc, char **argv, char **envp) {
      {&ChecksCat,      &DebugCat,    &ExtCallsCat, &ExprCat,   &LinkCat,
       &MemoryCat,      &MergeCat,    &MiscCat,     &ModuleCat, &ReplayCat,
       &SearchCat,      &SeedingCat,  &SolvingCat,  &StartCat,  &StatsCat,
-      &TerminationCat, &TestCaseCat, &TestGenCat});
+      &TerminationCat, &TestCaseCat, &TestGenCat,  &PTreeCat});
 
   llvm::InitializeNativeTarget();
 
diff --git a/unittests/Searcher/CMakeLists.txt b/unittests/Searcher/CMakeLists.txt
index c35b407f..bad3504a 100644
--- a/unittests/Searcher/CMakeLists.txt
+++ b/unittests/Searcher/CMakeLists.txt
@@ -1,8 +1,8 @@
 add_klee_unit_test(SearcherTest
   SearcherTest.cpp)
-target_link_libraries(SearcherTest PRIVATE kleeCore)
+target_link_libraries(SearcherTest PRIVATE kleeCore ${SQLITE3_LIBRARIES})
 target_include_directories(SearcherTest BEFORE PRIVATE "${CMAKE_SOURCE_DIR}/lib")
 target_compile_options(SearcherTest PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
 target_compile_definitions(SearcherTest PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
 
-target_include_directories(SearcherTest PRIVATE ${KLEE_INCLUDE_DIRS})
\ No newline at end of file
+target_include_directories(SearcherTest PRIVATE ${KLEE_INCLUDE_DIRS} ${SQLITE3_INCLUDE_DIRS})
diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp
index 0a7c8797..fc0d30ac 100644
--- a/unittests/Searcher/SearcherTest.cpp
+++ b/unittests/Searcher/SearcherTest.cpp
@@ -24,11 +24,11 @@ namespace {
 TEST(SearcherTest, RandomPath) {
   // First state
   ExecutionState es;
-  PTree processTree(&es);
+  InMemoryPTree processTree(es);
   es.ptreeNode = processTree.root.getPointer();
 
   RNG rng;
-  RandomPathSearcher rp(processTree, rng);
+  RandomPathSearcher rp(&processTree, rng);
   EXPECT_TRUE(rp.empty());
 
   rp.update(nullptr, {&es}, {});
@@ -64,15 +64,15 @@ TEST(SearcherTest, RandomPath) {
 TEST(SearcherTest, TwoRandomPath) {
   // Root state
   ExecutionState root;
-  PTree processTree(&root);
+  InMemoryPTree processTree(root);
   root.ptreeNode = processTree.root.getPointer();
 
   ExecutionState es(root);
   processTree.attach(root.ptreeNode, &es, &root, BranchType::NONE);
 
   RNG rng, rng1;
-  RandomPathSearcher rp(processTree, rng);
-  RandomPathSearcher rp1(processTree, rng1);
+  RandomPathSearcher rp(&processTree, rng);
+  RandomPathSearcher rp1(&processTree, rng1);
   EXPECT_TRUE(rp.empty());
   EXPECT_TRUE(rp1.empty());
 
@@ -122,7 +122,7 @@ TEST(SearcherTest, TwoRandomPathDot) {
 
   // Root state
   ExecutionState root;
-  PTree processTree(&root);
+  InMemoryPTree processTree(root);
   root.ptreeNode = processTree.root.getPointer();
   rootPNode = root.ptreeNode;
 
@@ -132,8 +132,8 @@ TEST(SearcherTest, TwoRandomPathDot) {
   esParentPNode = es.ptreeNode;
 
   RNG rng;
-  RandomPathSearcher rp(processTree, rng);
-  RandomPathSearcher rp1(processTree, rng);
+  RandomPathSearcher rp(&processTree, rng);
+  RandomPathSearcher rp1(&processTree, rng);
 
   rp.update(nullptr, {&es}, {});
 
@@ -204,14 +204,14 @@ TEST(SearcherTest, TwoRandomPathDot) {
 TEST(SearcherDeathTest, TooManyRandomPaths) {
   // First state
   ExecutionState es;
-  PTree processTree(&es);
+  InMemoryPTree processTree(es);
   es.ptreeNode = processTree.root.getPointer();
   processTree.remove(es.ptreeNode); // Need to remove to avoid leaks
 
   RNG rng;
-  RandomPathSearcher rp(processTree, rng);
-  RandomPathSearcher rp1(processTree, rng);
-  RandomPathSearcher rp2(processTree, rng);
-  ASSERT_DEATH({ RandomPathSearcher rp3(processTree, rng); }, "");
+  RandomPathSearcher rp(&processTree, rng);
+  RandomPathSearcher rp1(&processTree, rng);
+  RandomPathSearcher rp2(&processTree, rng);
+  ASSERT_DEATH({ RandomPathSearcher rp3(&processTree, rng); }, "");
 }
 }