12 files changed, 582 insertions, 114 deletions

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();