Renamed PTree to ExecutionTree (and similar)

12 files changed, 357 insertions, 318 deletions

diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 8df3e259..021c3ce7 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -13,14 +13,14 @@ add_library(kleeCore
   Context.cpp
   CoreStats.cpp
   ExecutionState.cpp
+  ExecutionTree.cpp
+  ExecutionTreeWriter.cpp
   Executor.cpp
   ExecutorUtil.cpp
   ExternalDispatcher.cpp
   ImpliedValue.cpp
   Memory.cpp
   MemoryManager.cpp
-  PTree.cpp
-  PTreeWriter.cpp
   Searcher.cpp
   SeedInfo.cpp
   SpecialFunctionHandler.cpp
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index dbe02fd9..20187166 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -32,10 +32,10 @@ namespace klee {
 class Array;
 class CallPathNode;
 struct Cell;
+class ExecutionTreeNode;
 struct KFunction;
 struct KInstruction;
 class MemoryObject;
-class PTreeNode;
 struct InstructionInfo;
 
 llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm);
@@ -207,9 +207,9 @@ public:
   /// @brief Set containing which lines in which files are covered by this state
   std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
 
-  /// @brief Pointer to the process tree of the current state
-  /// Copies of ExecutionState should not copy ptreeNode
-  PTreeNode *ptreeNode = nullptr;
+  /// @brief Pointer to the execution tree of the current state
+  /// Copies of ExecutionState should not copy executionTreeNode
+  ExecutionTreeNode *executionTreeNode = nullptr;
 
   /// @brief Ordered list of symbolics: used to generate test cases.
   //
diff --git a/lib/Core/ExecutionTree.cpp b/lib/Core/ExecutionTree.cpp
index c5b640d3..fb4913c7 100644
--- a/lib/Core/ExecutionTree.cpp
+++ b/lib/Core/ExecutionTree.cpp
@@ -1,4 +1,4 @@
-//===-- PTree.cpp ---------------------------------------------------------===//
+//===-- ExecutionTree.cpp -------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "PTree.h"
+#include "ExecutionTree.h"
 
 #include "ExecutionState.h"
 
@@ -23,100 +23,105 @@ using namespace klee;
 
 namespace klee {
 llvm::cl::OptionCategory
-    PTreeCat("Process tree related options",
-             "These options affect the process tree handling.");
+    ExecTreeCat("Execution tree related options",
+                "These options affect the execution tree handling.");
 }
 
 namespace {
-llvm::cl::opt<bool> CompressProcessTree(
-    "compress-process-tree",
-    llvm::cl::desc("Remove intermediate nodes in the process "
+llvm::cl::opt<bool> CompressExecutionTree(
+    "compress-execution-tree",
+    llvm::cl::desc("Remove intermediate nodes in the execution "
                    "tree whenever possible (default=false)"),
-    llvm::cl::init(false), llvm::cl::cat(PTreeCat));
+    llvm::cl::init(false), llvm::cl::cat(ExecTreeCat));
 
-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));
+llvm::cl::opt<bool> WriteExecutionTree(
+    "write-exec-tree", llvm::cl::init(false),
+    llvm::cl::desc("Write execution tree into exec_tree.db (default=false)"),
+    llvm::cl::cat(ExecTreeCat));
 } // namespace
 
-// PTreeNode
+// ExecutionTreeNode
 
-PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) noexcept
+ExecutionTreeNode::ExecutionTreeNode(ExecutionTreeNode *parent,
+                                     ExecutionState *state) noexcept
     : parent{parent}, left{nullptr}, right{nullptr}, state{state} {
-  state->ptreeNode = this;
+  state->executionTreeNode = this;
 }
 
-// AnnotatedPTreeNode
+// AnnotatedExecutionTreeNode
 
-AnnotatedPTreeNode::AnnotatedPTreeNode(PTreeNode *parent,
-                                       ExecutionState *state) noexcept
-    : PTreeNode(parent, state) {
+AnnotatedExecutionTreeNode::AnnotatedExecutionTreeNode(
+    ExecutionTreeNode *parent, ExecutionState *state) noexcept
+    : ExecutionTreeNode(parent, state) {
   id = nextID++;
 }
 
-// NoopPTree
+// NoopExecutionTree
 
-void NoopPTree::dump(llvm::raw_ostream &os) noexcept {
+void NoopExecutionTree::dump(llvm::raw_ostream &os) noexcept {
   os << "digraph G {\nTreeNotAvailable [shape=box]\n}";
 }
 
-// InMemoryPTree
+// InMemoryExecutionTree
 
-InMemoryPTree::InMemoryPTree(ExecutionState &initialState) noexcept {
-  root = PTreeNodePtr(createNode(nullptr, &initialState));
-  initialState.ptreeNode = root.getPointer();
+InMemoryExecutionTree::InMemoryExecutionTree(
+    ExecutionState &initialState) noexcept {
+  root = ExecutionTreeNodePtr(createNode(nullptr, &initialState));
+  initialState.executionTreeNode = root.getPointer();
 }
 
-PTreeNode *InMemoryPTree::createNode(PTreeNode *parent, ExecutionState *state) {
-  return new PTreeNode(parent, state);
+ExecutionTreeNode *InMemoryExecutionTree::createNode(ExecutionTreeNode *parent,
+                                                     ExecutionState *state) {
+  return new ExecutionTreeNode(parent, state);
 }
 
-void InMemoryPTree::attach(PTreeNode *node, ExecutionState *leftState,
-                           ExecutionState *rightState,
-                           BranchType reason) noexcept {
+void InMemoryExecutionTree::attach(ExecutionTreeNode *node,
+                                   ExecutionState *leftState,
+                                   ExecutionState *rightState,
+                                   BranchType reason) noexcept {
   assert(node && !node->left.getPointer() && !node->right.getPointer());
-  assert(node == rightState->ptreeNode &&
+  assert(node == rightState->executionTreeNode &&
          "Attach assumes the right state is the current state");
-  node->left = PTreeNodePtr(createNode(node, leftState));
+  node->left = ExecutionTreeNodePtr(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(createNode(node, rightState), currentNodeTag);
+  node->right =
+      ExecutionTreeNodePtr(createNode(node, rightState), currentNodeTag);
   updateBranchingNode(*node, reason);
   node->state = nullptr;
 }
 
-void InMemoryPTree::remove(PTreeNode *n) noexcept {
+void InMemoryExecutionTree::remove(ExecutionTreeNode *n) noexcept {
   assert(!n->left.getPointer() && !n->right.getPointer());
   updateTerminatingNode(*n);
   do {
-    PTreeNode *p = n->parent;
+    ExecutionTreeNode *p = n->parent;
     if (p) {
       if (n == p->left.getPointer()) {
-        p->left = PTreeNodePtr(nullptr);
+        p->left = ExecutionTreeNodePtr(nullptr);
       } else {
         assert(n == p->right.getPointer());
-        p->right = PTreeNodePtr(nullptr);
+        p->right = ExecutionTreeNodePtr(nullptr);
       }
     }
     delete n;
     n = p;
   } while (n && !n->left.getPointer() && !n->right.getPointer());
 
-  if (n && CompressProcessTree) {
-    // We're now at a node that has exactly one child; we've just deleted the
+  if (n && CompressExecutionTree) {
+    // We are now at a node that has exactly one child; we've just deleted the
     // other one. Eliminate the node and connect its child to the parent
     // directly (if it's not the root).
-    PTreeNodePtr child = n->left.getPointer() ? n->left : n->right;
-    PTreeNode *parent = n->parent;
+    ExecutionTreeNodePtr child = n->left.getPointer() ? n->left : n->right;
+    ExecutionTreeNode *parent = n->parent;
 
     child.getPointer()->parent = parent;
     if (!parent) {
-      // We're at the root.
+      // We are at the root
       root = child;
     } else {
       if (n == parent->left.getPointer()) {
@@ -131,7 +136,7 @@ void InMemoryPTree::remove(PTreeNode *n) noexcept {
   }
 }
 
-void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept {
+void InMemoryExecutionTree::dump(llvm::raw_ostream &os) noexcept {
   std::unique_ptr<ExprPPrinter> pp(ExprPPrinter::create(os));
   pp->setNewline("\\l");
   os << "digraph G {\n"
@@ -141,10 +146,10 @@ void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept {
      << "\tcenter = \"true\";\n"
      << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
      << "\tedge [arrowsize=.3]\n";
-  std::vector<const PTreeNode *> stack;
+  std::vector<const ExecutionTreeNode *> stack;
   stack.push_back(root.getPointer());
   while (!stack.empty()) {
-    const PTreeNode *n = stack.back();
+    const ExecutionTreeNode *n = stack.back();
     stack.pop_back();
     os << "\tn" << n << " [shape=diamond";
     if (n->state)
@@ -164,43 +169,46 @@ void InMemoryPTree::dump(llvm::raw_ostream &os) noexcept {
   os << "}\n";
 }
 
-std::uint8_t InMemoryPTree::getNextId() noexcept {
+std::uint8_t InMemoryExecutionTree::getNextId() noexcept {
   static_assert(PtrBitCount <= 8);
   std::uint8_t id = 1 << registeredIds++;
   if (registeredIds > PtrBitCount) {
-    klee_error("PTree cannot support more than %d RandomPathSearchers",
+    klee_error("ExecutionTree cannot support more than %d RandomPathSearchers",
                PtrBitCount);
   }
   return id;
 }
 
-// PersistentPTree
+// PersistentExecutionTree
 
-PersistentPTree::PersistentPTree(ExecutionState &initialState,
-                                 InterpreterHandler &ih) noexcept
-    : writer(ih.getOutputFilename("ptree.db")) {
-  root = PTreeNodePtr(createNode(nullptr, &initialState));
-  initialState.ptreeNode = root.getPointer();
+PersistentExecutionTree::PersistentExecutionTree(
+    ExecutionState &initialState, InterpreterHandler &ih) noexcept
+    : writer(ih.getOutputFilename("exec_tree.db")) {
+  root = ExecutionTreeNodePtr(createNode(nullptr, &initialState));
+  initialState.executionTreeNode = root.getPointer();
 }
 
-void PersistentPTree::dump(llvm::raw_ostream &os) noexcept {
+void PersistentExecutionTree::dump(llvm::raw_ostream &os) noexcept {
   writer.batchCommit(true);
-  InMemoryPTree::dump(os);
+  InMemoryExecutionTree::dump(os);
 }
 
-PTreeNode *PersistentPTree::createNode(PTreeNode *parent,
-                                       ExecutionState *state) {
-  return new AnnotatedPTreeNode(parent, state);
+ExecutionTreeNode *
+PersistentExecutionTree::createNode(ExecutionTreeNode *parent,
+                                    ExecutionState *state) {
+  return new AnnotatedExecutionTreeNode(parent, state);
 }
 
-void PersistentPTree::setTerminationType(ExecutionState &state,
-                                         StateTerminationType type) {
-  auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(state.ptreeNode);
+void PersistentExecutionTree::setTerminationType(ExecutionState &state,
+                                                 StateTerminationType type) {
+  auto *annotatedNode =
+      llvm::cast<AnnotatedExecutionTreeNode>(state.executionTreeNode);
   annotatedNode->kind = type;
 }
 
-void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) {
-  auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(&node);
+void PersistentExecutionTree::updateBranchingNode(ExecutionTreeNode &node,
+                                                  BranchType reason) {
+  auto *annotatedNode = llvm::cast<AnnotatedExecutionTreeNode>(&node);
   const auto &state = *node.state;
   const auto prevPC = state.prevPC;
   annotatedNode->asmLine =
@@ -209,9 +217,9 @@ void PersistentPTree::updateBranchingNode(PTreeNode &node, BranchType reason) {
   writer.write(*annotatedNode);
 }
 
-void PersistentPTree::updateTerminatingNode(PTreeNode &node) {
+void PersistentExecutionTree::updateTerminatingNode(ExecutionTreeNode &node) {
   assert(node.state);
-  auto *annotatedNode = llvm::cast<AnnotatedPTreeNode>(&node);
+  auto *annotatedNode = llvm::cast<AnnotatedExecutionTreeNode>(&node);
   const auto &state = *node.state;
   const auto prevPC = state.prevPC;
   annotatedNode->asmLine =
@@ -222,14 +230,14 @@ void PersistentPTree::updateTerminatingNode(PTreeNode &node) {
 
 // Factory
 
-std::unique_ptr<PTree> klee::createPTree(ExecutionState &initialState,
-                                         bool inMemory,
-                                         InterpreterHandler &ih) {
-  if (WritePTree)
-    return std::make_unique<PersistentPTree>(initialState, ih);
+std::unique_ptr<ExecutionTree>
+klee::createExecutionTree(ExecutionState &initialState, bool inMemory,
+                          InterpreterHandler &ih) {
+  if (WriteExecutionTree)
+    return std::make_unique<PersistentExecutionTree>(initialState, ih);
 
   if (inMemory)
-    return std::make_unique<InMemoryPTree>(initialState);
+    return std::make_unique<InMemoryExecutionTree>(initialState);
 
-  return std::make_unique<NoopPTree>();
+  return std::make_unique<NoopExecutionTree>();
 };
diff --git a/lib/Core/ExecutionTree.h b/lib/Core/ExecutionTree.h
index ab3f0433..cd28a85c 100644
--- a/lib/Core/ExecutionTree.h
+++ b/lib/Core/ExecutionTree.h
@@ -1,4 +1,4 @@
-//===-- PTree.h -------------------------------------------------*- C++ -*-===//
+//===-- ExecutionTree.h -----------------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,10 +7,10 @@
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef KLEE_PTREE_H
-#define KLEE_PTREE_H
+#ifndef KLEE_EXECUTION_TREE_H
+#define KLEE_EXECUTION_TREE_H
 
-#include "PTreeWriter.h"
+#include "ExecutionTreeWriter.h"
 #include "UserSearcher.h"
 #include "klee/Core/BranchTypes.h"
 #include "klee/Core/TerminationTypes.h"
@@ -26,40 +26,41 @@
 namespace klee {
 class ExecutionState;
 class Executor;
-class InMemoryPTree;
+class InMemoryExecutionTree;
 class InterpreterHandler;
-class PTreeNode;
+class ExecutionTreeNode;
 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. */
+/* ExecutionTreeNodePtr is used by the Random Path Searcher object to
+efficiently record which ExecutionTreeNode belongs to it. ExecutionTree is a
+global structure that captures all  states, whereas a Random Path Searcher might
+only care about a subset. The integer part of ExecutionTreeNodePtr is a bitmask
+(a "tag") of which Random Path Searchers ExecutionTreeNode belongs to. */
 constexpr std::uint8_t PtrBitCount = 3;
-using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
+using ExecutionTreeNodePtr =
+    llvm::PointerIntPair<ExecutionTreeNode *, PtrBitCount, uint8_t>;
 
-class PTreeNode {
+class ExecutionTreeNode {
 public:
   enum class NodeType : std::uint8_t { Basic, Annotated };
 
-  PTreeNode *parent{nullptr};
-  PTreeNodePtr left;
-  PTreeNodePtr right;
+  ExecutionTreeNode *parent{nullptr};
+  ExecutionTreeNodePtr left;
+  ExecutionTreeNodePtr 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;
+  ExecutionTreeNode(ExecutionTreeNode *parent, ExecutionState *state) noexcept;
+  virtual ~ExecutionTreeNode() = default;
+  ExecutionTreeNode(const ExecutionTreeNode &) = delete;
+  ExecutionTreeNode &operator=(ExecutionTreeNode const &) = delete;
+  ExecutionTreeNode(ExecutionTreeNode &&) = delete;
+  ExecutionTreeNode &operator=(ExecutionTreeNode &&) = delete;
 
   [[nodiscard]] virtual NodeType getType() const { return NodeType::Basic; }
-  static bool classof(const PTreeNode *N) { return true; }
+  static bool classof(const ExecutionTreeNode *N) { return true; }
 };
 
-class AnnotatedPTreeNode : public PTreeNode {
+class AnnotatedExecutionTreeNode : public ExecutionTreeNode {
   inline static std::uint32_t nextID{1};
 
 public:
@@ -68,112 +69,135 @@ public:
   std::uint32_t asmLine{0};
   std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
 
-  AnnotatedPTreeNode(PTreeNode *parent, ExecutionState *state) noexcept;
-  ~AnnotatedPTreeNode() override = default;
+  AnnotatedExecutionTreeNode(ExecutionTreeNode *parent,
+                             ExecutionState *state) noexcept;
+  ~AnnotatedExecutionTreeNode() override = default;
 
   [[nodiscard]] NodeType getType() const override { return NodeType::Annotated; }
-  static bool classof(const PTreeNode *N) {
+
+  static bool classof(const ExecutionTreeNode *N) {
     return N->getType() == NodeType::Annotated;
   }
 };
 
-class PTree {
+class ExecutionTree {
 public:
-  enum class PTreeType : std::uint8_t { Basic, Noop, InMemory, Persistent };
-
-  /// Branch from PTreeNode and attach states, convention: rightState is
+  enum class ExecutionTreeType : std::uint8_t {
+    Basic,
+    Noop,
+    InMemory,
+    Persistent
+  };
+
+  /// Branch from ExecutionTreeNode and attach states, convention: rightState is
   /// parent
-  virtual void attach(PTreeNode *node, ExecutionState *leftState,
+  virtual void attach(ExecutionTreeNode *node, ExecutionState *leftState,
                       ExecutionState *rightState, BranchType reason) = 0;
-  /// Dump process tree in .dot format into os (debug)
+  /// Dump execution 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;
+  virtual void remove(ExecutionTreeNode *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;
+  virtual ~ExecutionTree() = default;
+  ExecutionTree(ExecutionTree const &) = delete;
+  ExecutionTree &operator=(ExecutionTree const &) = delete;
+  ExecutionTree(ExecutionTree &&) = delete;
+  ExecutionTree &operator=(ExecutionTree &&) = delete;
 
-  [[nodiscard]] virtual PTreeType getType() const = 0;
-  static bool classof(const PTreeNode *N) { return true; }
+  [[nodiscard]] virtual ExecutionTreeType getType() const = 0;
+  static bool classof(const ExecutionTreeNode *N) { return true; }
 
 protected:
-  explicit PTree() noexcept = default;
+  explicit ExecutionTree() noexcept = default;
 };
 
-/// @brief A pseudo process tree that does not maintain any nodes.
-class NoopPTree final : public PTree {
+/// @brief A pseudo execution tree that does not maintain any nodes.
+class NoopExecutionTree final : public ExecutionTree {
 public:
-  NoopPTree() noexcept = default;
-  ~NoopPTree() override = default;
-  void attach(PTreeNode *node, ExecutionState *leftState,
-              ExecutionState *rightState,
-              BranchType reason) noexcept override{}
+  NoopExecutionTree() noexcept = default;
+  ~NoopExecutionTree() override = default;
+  void attach(ExecutionTreeNode *node, ExecutionState *leftState,
+              ExecutionState *rightState, BranchType reason) noexcept override {}
   void dump(llvm::raw_ostream &os) noexcept override;
-  void remove(PTreeNode *node) noexcept override{}
+  void remove(ExecutionTreeNode *node) noexcept override {}
 
-  [[nodiscard]] PTreeType getType() const override { return PTreeType::Noop; };
-  static bool classof(const PTree *T) { return T->getType() == PTreeType::Noop; }
+  [[nodiscard]] ExecutionTreeType getType() const override {
+    return ExecutionTreeType::Noop;
+  };
+
+  static bool classof(const ExecutionTree *T) {
+    return T->getType() == ExecutionTreeType::Noop;
+  }
 };
 
-/// @brief An in-memory process tree required by RandomPathSearcher
-class InMemoryPTree : public PTree {
+/// @brief An in-memory execution tree required by RandomPathSearcher
+class InMemoryExecutionTree : public ExecutionTree {
 public:
-  PTreeNodePtr root;
+  ExecutionTreeNodePtr 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){}
+  virtual ExecutionTreeNode *createNode(ExecutionTreeNode *parent,
+                                        ExecutionState *state);
+  virtual void updateBranchingNode(ExecutionTreeNode &node, BranchType reason) {}
+  virtual void updateTerminatingNode(ExecutionTreeNode &node) {}
 
 public:
-  InMemoryPTree() noexcept = default;
-  explicit InMemoryPTree(ExecutionState &initialState) noexcept;
-  ~InMemoryPTree() override = default;
+  InMemoryExecutionTree() noexcept = default;
+  explicit InMemoryExecutionTree(ExecutionState &initialState) noexcept;
+  ~InMemoryExecutionTree() override = default;
 
-  void attach(PTreeNode *node, ExecutionState *leftState,
+  void attach(ExecutionTreeNode *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;
+  void remove(ExecutionTreeNode *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);
+  [[nodiscard]] ExecutionTreeType getType() const override {
+    return ExecutionTreeType::InMemory;
+  };
+
+  static bool classof(const ExecutionTree *T) {
+    return (T->getType() == ExecutionTreeType::InMemory) ||
+           (T->getType() == ExecutionTreeType::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;
+/// @brief An in-memory execution tree that also writes its nodes into an SQLite
+/// database (exec_tree.db) with a ExecutionTreeWriter
+class PersistentExecutionTree : public InMemoryExecutionTree {
+  ExecutionTreeWriter writer;
 
-  PTreeNode *createNode(PTreeNode *parent, ExecutionState *state) override;
-  void updateBranchingNode(PTreeNode &node, BranchType reason) override;
-  void updateTerminatingNode(PTreeNode &node) override;
+  ExecutionTreeNode *createNode(ExecutionTreeNode *parent,
+                                ExecutionState *state) override;
+  void updateBranchingNode(ExecutionTreeNode &node, BranchType reason) override;
+  void updateTerminatingNode(ExecutionTreeNode &node) override;
 
 public:
-  explicit PersistentPTree(ExecutionState &initialState,
-                           InterpreterHandler &ih) noexcept;
-  ~PersistentPTree() override = default;
+  explicit PersistentExecutionTree(ExecutionState &initialState,
+                                   InterpreterHandler &ih) noexcept;
+  ~PersistentExecutionTree() 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; }
+  [[nodiscard]] ExecutionTreeType getType() const override {
+    return ExecutionTreeType::Persistent;
+  };
+
+  static bool classof(const ExecutionTree *T) {
+    return T->getType() == ExecutionTreeType::Persistent;
+  }
 };
 
-std::unique_ptr<PTree> createPTree(ExecutionState &initialState, bool inMemory,
-                                   InterpreterHandler &ih);
+std::unique_ptr<ExecutionTree> createExecutionTree(ExecutionState &initialState,
+                                                   bool inMemory,
+                                                   InterpreterHandler &ih);
 } // namespace klee
 
-#endif /* KLEE_PTREE_H */
+#endif /* KLEE_EXECUTION_TREE_H */
diff --git a/lib/Core/ExecutionTreeWriter.cpp b/lib/Core/ExecutionTreeWriter.cpp
index a8067a5d..10cd5c27 100644
--- a/lib/Core/ExecutionTreeWriter.cpp
+++ b/lib/Core/ExecutionTreeWriter.cpp
@@ -1,4 +1,4 @@
-//===-- PTreeWriter.cpp ---------------------------------------------------===//
+//===-- ExecutionTreeWriter.cpp -------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -7,9 +7,9 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "PTreeWriter.h"
+#include "ExecutionTreeWriter.h"
 
-#include "PTree.h"
+#include "ExecutionTree.h"
 #include "klee/Support/ErrorHandling.h"
 #include "klee/Support/OptionCategories.h"
 
@@ -18,9 +18,9 @@
 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));
+    llvm::cl::desc("Number of execution tree nodes to batch for writing, "
+                   "see --write-execution-tree (default=100)"),
+    llvm::cl::cat(klee::ExecTreeCat));
 } // namespace
 
 using namespace klee;
@@ -34,28 +34,29 @@ void prepare_statement(sqlite3 *db, const std::string &query, sqlite3_stmt **stm
   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]",
+    klee_warning("Execution tree database: cannot 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());
+    klee_error("Execution tree database: cannot prepare query: %s",
+               query.c_str());
   }
 }
 
-PTreeWriter::PTreeWriter(const std::string &dbPath) {
+ExecutionTreeWriter::ExecutionTreeWriter(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));
+    klee_error("Cannot create execution 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);
+    klee_warning("Execution tree database: cannot 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);
+    klee_warning("Execution tree database: cannot set option: %s", errMsg);
     sqlite3_free(errMsg);
   }
 
@@ -66,10 +67,10 @@ PTreeWriter::PTreeWriter(const std::string &dbPath) {
       "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);
+    klee_warning("Execution tree database: initialisation error: %s", zErr);
     sqlite3_free(zErr);
     sqlite3_close(db);
-    klee_error("Process tree database: initialisation error.");
+    klee_error("Execution tree database: initialisation error.");
   }
 
   // create prepared statements
@@ -85,16 +86,16 @@ PTreeWriter::PTreeWriter(const std::string &dbPath) {
 
   // begin transaction
   if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) {
-    klee_warning("Process tree database: can't begin transaction: %s",
+    klee_warning("Execution tree database: cannot begin transaction: %s",
                  sqlite3_errmsg(db));
   }
   if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) {
-    klee_warning("Process tree database: can't reset transaction: %s",
+    klee_warning("Execution tree database: cannot reset transaction: %s",
                  sqlite3_errmsg(db));
   }
 }
 
-PTreeWriter::~PTreeWriter() {
+ExecutionTreeWriter::~ExecutionTreeWriter() {
   batchCommit(!flushed);
 
   // finalize prepared statements
@@ -105,39 +106,39 @@ PTreeWriter::~PTreeWriter() {
   // commit
   if (sqlite3_exec(db, "END TRANSACTION", nullptr, nullptr, nullptr) !=
       SQLITE_OK) {
-    klee_warning("Process tree database: can't end transaction: %s",
+    klee_warning("Execution tree database: cannot end transaction: %s",
                  sqlite3_errmsg(db));
   }
 
   if (sqlite3_close(db) != SQLITE_OK) {
-    klee_warning("Process tree database: can't close database: %s",
+    klee_warning("Execution tree database: cannot close database: %s",
                  sqlite3_errmsg(db));
   }
 }
 
-void PTreeWriter::batchCommit(bool force) {
+void ExecutionTreeWriter::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",
+    klee_warning("Execution tree database: transaction commit error: %s",
                  sqlite3_errmsg(db));
   }
 
   if (sqlite3_reset(transactionCommitStmt) != SQLITE_OK) {
-    klee_warning("Process tree database: transaction reset error: %s",
+    klee_warning("Execution tree database: transaction reset error: %s",
                  sqlite3_errmsg(db));
   }
 
   if (sqlite3_step(transactionBeginStmt) != SQLITE_DONE) {
-    klee_warning("Process tree database: transaction begin error: %s",
+    klee_warning("Execution tree database: transaction begin error: %s",
                  sqlite3_errmsg(db));
   }
 
   if (sqlite3_reset(transactionBeginStmt) != SQLITE_OK) {
-    klee_warning("Process tree database: transaction reset error: %s",
+    klee_warning("Execution tree database: transaction reset error: %s",
                  sqlite3_errmsg(db));
   }
 
@@ -145,7 +146,7 @@ void PTreeWriter::batchCommit(bool force) {
   flushed = true;
 }
 
-void PTreeWriter::write(const AnnotatedPTreeNode &node) {
+void ExecutionTreeWriter::write(const AnnotatedExecutionTreeNode &node) {
   unsigned rc = 0;
 
   // bind values (SQLITE_OK is defined as 0 - just check success once at the
@@ -155,12 +156,12 @@ void PTreeWriter::write(const AnnotatedPTreeNode &node) {
   rc |= sqlite3_bind_int64(
       insertStmt, 3,
       node.left.getPointer()
-          ? (static_cast<AnnotatedPTreeNode *>(node.left.getPointer()))->id
+          ? (static_cast<AnnotatedExecutionTreeNode *>(node.left.getPointer()))->id
           : 0);
   rc |= sqlite3_bind_int64(
       insertStmt, 4,
       node.right.getPointer()
-          ? (static_cast<AnnotatedPTreeNode *>(node.right.getPointer()))->id
+          ? (static_cast<AnnotatedExecutionTreeNode *>(node.right.getPointer()))->id
           : 0);
   rc |= sqlite3_bind_int(insertStmt, 5, node.asmLine);
   std::uint8_t value{0};
@@ -170,25 +171,26 @@ void PTreeWriter::write(const AnnotatedPTreeNode &node) {
     value =
         static_cast<std::uint8_t>(std::get<StateTerminationType>(node.kind));
   } else {
-    assert(false && "PTreeWriter: Illegal node kind!");
+    assert(false && "ExecutionTreeWriter: 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",
+    klee_error("Execution tree database: cannot 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));
+    klee_warning(
+        "Execution tree database: cannot 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,
+    klee_warning("Execution tree database: error reset node: %u: %s", node.id,
                  sqlite3_errmsg(db));
   }
 
diff --git a/lib/Core/ExecutionTreeWriter.h b/lib/Core/ExecutionTreeWriter.h
index 12709116..d78ad0b1 100644
--- a/lib/Core/ExecutionTreeWriter.h
+++ b/lib/Core/ExecutionTreeWriter.h
@@ -1,4 +1,4 @@
-//===-- PTreeWriter.h -------------------------------------------*- C++ -*-===//
+//===-- ExecutionTreeWriter.h -----------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -15,11 +15,11 @@
 #include <string>
 
 namespace klee {
-class AnnotatedPTreeNode;
+class AnnotatedExecutionTreeNode;
 
-/// @brief Writes process tree nodes into an SQLite database
-class PTreeWriter {
-  friend class PersistentPTree;
+/// @brief Writes execution tree nodes into an SQLite database
+class ExecutionTreeWriter {
+  friend class PersistentExecutionTree;
 
   ::sqlite3 *db{nullptr};
   ::sqlite3_stmt *insertStmt{nullptr};
@@ -32,15 +32,15 @@ class PTreeWriter {
   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;
+  explicit ExecutionTreeWriter(const std::string &dbPath);
+  ~ExecutionTreeWriter();
+  ExecutionTreeWriter(const ExecutionTreeWriter &other) = delete;
+  ExecutionTreeWriter(ExecutionTreeWriter &&other) noexcept = delete;
+  ExecutionTreeWriter &operator=(const ExecutionTreeWriter &other) = delete;
+  ExecutionTreeWriter &operator=(ExecutionTreeWriter &&other) noexcept = delete;
 
   /// Write new node into database
-  void write(const AnnotatedPTreeNode &node);
+  void write(const AnnotatedExecutionTreeNode &node);
 };
 
 } // namespace klee
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 8f70540c..cf6ce777 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -13,12 +13,12 @@
 #include "Context.h"
 #include "CoreStats.h"
 #include "ExecutionState.h"
+#include "ExecutionTree.h"
 #include "ExternalDispatcher.h"
 #include "GetElementPtrTypeIterator.h"
 #include "ImpliedValue.h"
 #include "Memory.h"
 #include "MemoryManager.h"
-#include "PTree.h"
 #include "Searcher.h"
 #include "SeedInfo.h"
 #include "SpecialFunctionHandler.h"
@@ -469,8 +469,8 @@ cl::opt<bool> DebugCheckForImpliedValues(
 } // namespace
 
 // XXX hack
-extern "C" unsigned dumpStates, dumpPTree;
-unsigned dumpStates = 0, dumpPTree = 0;
+extern "C" unsigned dumpStates, dumpExecutionTree;
+unsigned dumpStates = 0, dumpExecutionTree = 0;
 
 Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
@@ -918,7 +918,7 @@ void Executor::branch(ExecutionState &state,
       ExecutionState *ns = es->branch();
       addedStates.push_back(ns);
       result.push_back(ns);
-      processTree->attach(es->ptreeNode, ns, es, reason);
+      executionTree->attach(es->executionTreeNode, ns, es, reason);
     }
   }
 
@@ -1189,7 +1189,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       }
     }
 
-    processTree->attach(current.ptreeNode, falseState, trueState, reason);
+    executionTree->attach(current.executionTreeNode, falseState, trueState, reason);
     stats::incBranchStat(reason, 1);
 
     if (pathWriter) {
@@ -3355,7 +3355,7 @@ void Executor::updateStates(ExecutionState *current) {
       seedMap.find(es);
     if (it3 != seedMap.end())
       seedMap.erase(it3);
-    processTree->remove(es->ptreeNode);
+    executionTree->remove(es->executionTreeNode);
     delete es;
   }
   removedStates.clear();
@@ -3522,7 +3522,8 @@ void Executor::run(ExecutionState &initialState) {
       executeInstruction(state, ki);
       timers.invoke();
       if (::dumpStates) dumpStates();
-      if (::dumpPTree) dumpPTree();
+      if (::dumpExecutionTree)
+        dumpExecutionTree();
       updateStates(&state);
 
       if ((stats::instructions % 1000) == 0) {
@@ -3571,7 +3572,8 @@ void Executor::run(ExecutionState &initialState) {
     executeInstruction(state, ki);
     timers.invoke();
     if (::dumpStates) dumpStates();
-    if (::dumpPTree) dumpPTree();
+    if (::dumpExecutionTree)
+      dumpExecutionTree();
 
     updateStates(&state);
 
@@ -3647,7 +3649,7 @@ void Executor::terminateState(ExecutionState &state,
   }
 
   interpreterHandler->incPathsExplored();
-  processTree->setTerminationType(state, reason);
+  executionTree->setTerminationType(state, reason);
 
   std::vector<ExecutionState *>::iterator it =
       std::find(addedStates.begin(), addedStates.end(), &state);
@@ -3662,7 +3664,7 @@ void Executor::terminateState(ExecutionState &state,
     if (it3 != seedMap.end())
       seedMap.erase(it3);
     addedStates.erase(it);
-    processTree->remove(state.ptreeNode);
+    executionTree->remove(state.executionTreeNode);
     delete &state;
   }
 }
@@ -4607,10 +4609,10 @@ void Executor::runFunctionAsMain(Function *f,
   
   initializeGlobals(*state);
 
-  processTree = createPTree(*state, userSearcherRequiresInMemoryPTree(),
-                            *interpreterHandler);
+  executionTree = createExecutionTree(
+      *state, userSearcherRequiresInMemoryExecutionTree(), *interpreterHandler);
   run(*state);
-  processTree = nullptr;
+  executionTree = nullptr;
 
   // hack to clear memory objects
   memory = nullptr;
@@ -4840,18 +4842,17 @@ int *Executor::getErrnoLocation(const ExecutionState &state) const {
 #endif
 }
 
-
-void Executor::dumpPTree() {
-  if (!::dumpPTree) return;
+void Executor::dumpExecutionTree() {
+  if (!::dumpExecutionTree)
+    return;
 
   char name[32];
-  snprintf(name, sizeof(name),"ptree%08d.dot", (int) stats::instructions);
+  snprintf(name, sizeof(name), "exec_tree%08d.dot", (int)stats::instructions);
   auto os = interpreterHandler->openOutputFile(name);
-  if (os) {
-    processTree->dump(*os);
-  }
+  if (os)
+    executionTree->dump(*os);
 
-  ::dumpPTree = 0;
+  ::dumpExecutionTree = 0;
 }
 
 void Executor::dumpStates() {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 3635de78..f7f84101 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -57,38 +57,36 @@ namespace llvm {
   class Value;
 }
 
-namespace klee {  
-  class Array;
-  struct Cell;
-  class ExecutionState;
-  class ExternalDispatcher;
-  class Expr;
-  class InstructionInfoTable;
-  class KCallable;
-  struct KFunction;
-  struct KInstruction;
-  class KInstIterator;
-  class KModule;
-  class MemoryManager;
-  class MemoryObject;
-  class ObjectState;
-  class PTree;
-  class Searcher;
-  class SeedInfo;
-  class SpecialFunctionHandler;
-  struct StackFrame;
-  class StatsTracker;
-  class TimingSolver;
-  class TreeStreamWriter;
-  class MergeHandler;
-  class MergingSearcher;
-  template<class T> class ref;
-
-
-
-  /// \todo Add a context object to keep track of data only live
-  /// during an instruction step. Should contain addedStates,
-  /// removedStates, and haltExecution, among others.
+namespace klee {
+class Array;
+struct Cell;
+class ExecutionState;
+class ExternalDispatcher;
+class Expr;
+class InstructionInfoTable;
+class KCallable;
+struct KFunction;
+struct KInstruction;
+class KInstIterator;
+class KModule;
+class MemoryManager;
+class MemoryObject;
+class ObjectState;
+class ExecutionTree;
+class Searcher;
+class SeedInfo;
+class SpecialFunctionHandler;
+struct StackFrame;
+class StatsTracker;
+class TimingSolver;
+class TreeStreamWriter;
+class MergeHandler;
+class MergingSearcher;
+template <class T> class ref;
+
+/// \todo Add a context object to keep track of data only live
+/// during an instruction step. Should contain addedStates,
+/// removedStates, and haltExecution, among others.
 
 class Executor : public Interpreter {
   friend class OwningSearcher;
@@ -117,7 +115,7 @@ private:
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;
   TimerGroup timers;
-  std::unique_ptr<PTree> processTree;
+  std::unique_ptr<ExecutionTree> executionTree;
 
   /// Used to track states that have been added during the current
   /// instructions step. 
@@ -501,7 +499,7 @@ private:
 
   /// Only for debug purposes; enable via debugger or klee-control
   void dumpStates();
-  void dumpPTree();
+  void dumpExecutionTree();
 
 public:
   Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts,
@@ -576,7 +574,7 @@ public:
   MergingSearcher *getMergingSearcher() const { return mergingSearcher; };
   void setMergingSearcher(MergingSearcher *ms) { mergingSearcher = ms; };
 };
-  
-} // End klee namespace
+
+} // namespace klee
 
 #endif /* KLEE_EXECUTOR_H */
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 1c57eb4e..e94511ea 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -11,9 +11,9 @@
 
 #include "CoreStats.h"
 #include "ExecutionState.h"
+#include "ExecutionTree.h"
 #include "Executor.h"
 #include "MergeHandler.h"
-#include "PTree.h"
 #include "StatsTracker.h"
 
 #include "klee/ADT/DiscretePDF.h"
@@ -261,18 +261,17 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) {
 #define IS_OUR_NODE_VALID(n)                                                   \
   (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
 
-RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng)
-    : processTree{processTree}, theRNG{rng},
-      idBitMask{
-          static_cast<uint8_t>(processTree ? processTree->getNextId() : 0)} {
-
-  assert(processTree);
+RandomPathSearcher::RandomPathSearcher(InMemoryExecutionTree *executionTree, RNG &rng)
+    : executionTree{executionTree}, theRNG{rng},
+      idBitMask{static_cast<uint8_t>(executionTree ? executionTree->getNextId() : 0)} {
+  assert(executionTree);
 };
 
 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(executionTree->root.getInt() & idBitMask &&
+         "Root should belong to the searcher");
+  ExecutionTreeNode *n = executionTree->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");
@@ -300,46 +299,47 @@ void RandomPathSearcher::update(ExecutionState *current,
                                 const std::vector<ExecutionState *> &removedStates) {
   // insert states
   for (auto es : addedStates) {
-    PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
-    PTreeNodePtr *childPtr;
+    ExecutionTreeNode *etnode = es->executionTreeNode, *parent = etnode->parent;
+    ExecutionTreeNodePtr *childPtr;
 
-    childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
-                                                              : &parent->right)
-                      : &processTree->root;
-    while (pnode && !IS_OUR_NODE_VALID(*childPtr)) {
+    childPtr = parent ? ((parent->left.getPointer() == etnode) ? &parent->left
+                                                               : &parent->right)
+                      : &executionTree->root;
+    while (etnode && !IS_OUR_NODE_VALID(*childPtr)) {
       childPtr->setInt(childPtr->getInt() | idBitMask);
-      pnode = parent;
-      if (pnode)
-        parent = pnode->parent;
+      etnode = parent;
+      if (etnode)
+        parent = etnode->parent;
 
       childPtr = parent
-                     ? ((parent->left.getPointer() == pnode) ? &parent->left
-                                                             : &parent->right)
-                     : &processTree->root;
+                     ? ((parent->left.getPointer() == etnode) ? &parent->left
+                                                              : &parent->right)
+                     : &executionTree->root;
     }
   }
 
   // remove states
   for (auto es : removedStates) {
-    PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
+    ExecutionTreeNode *etnode = es->executionTreeNode, *parent = etnode->parent;
 
-    while (pnode && !IS_OUR_NODE_VALID(pnode->left) &&
-           !IS_OUR_NODE_VALID(pnode->right)) {
+    while (etnode && !IS_OUR_NODE_VALID(etnode->left) &&
+           !IS_OUR_NODE_VALID(etnode->right)) {
       auto childPtr =
-          parent ? ((parent->left.getPointer() == pnode) ? &parent->left
-                                                         : &parent->right)
-                 : &processTree->root;
-      assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours");
+          parent ? ((parent->left.getPointer() == etnode) ? &parent->left
+                                                          : &parent->right)
+                 : &executionTree->root;
+      assert(IS_OUR_NODE_VALID(*childPtr) &&
+             "Removing executionTree child not ours");
       childPtr->setInt(childPtr->getInt() & ~idBitMask);
-      pnode = parent;
-      if (pnode)
-        parent = pnode->parent;
+      etnode = parent;
+      if (etnode)
+        parent = etnode->parent;
     }
   }
 }
 
 bool RandomPathSearcher::empty() {
-  return !IS_OUR_NODE_VALID(processTree->root);
+  return !IS_OUR_NODE_VALID(executionTree->root);
 }
 
 void RandomPathSearcher::printName(llvm::raw_ostream &os) {
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index ddd49264..36efe67a 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -11,7 +11,7 @@
 #define KLEE_SEARCHER_H
 
 #include "ExecutionState.h"
-#include "PTree.h"
+#include "ExecutionTree.h"
 #include "klee/ADT/RNG.h"
 #include "klee/System/Time.h"
 
@@ -89,10 +89,11 @@ namespace klee {
     void printName(llvm::raw_ostream &os) override;
   };
 
-  /// BFSSearcher implements breadth-first exploration. When KLEE branches multiple
-  /// times for a single instruction, all new states have the same depth. Keep in
-  /// mind that the process tree (PTree) is a binary tree and hence the depth of
-  /// a state in that tree and its branch depth during BFS are different.
+  /// BFSSearcher implements breadth-first exploration. When KLEE branches
+  /// multiple times for a single instruction, all new states have the same
+  /// depth. Keep in mind that the execution tree (ExecutionTree) is a binary
+  /// tree and hence the depth of a state in that tree and its branch depth
+  /// during BFS are different.
   class BFSSearcher final : public Searcher {
     std::deque<ExecutionState*> states;
 
@@ -156,32 +157,35 @@ namespace klee {
     void printName(llvm::raw_ostream &os) override;
   };
 
-  /// RandomPathSearcher performs a random walk of the PTree to select a state.
-  /// PTree is a global data structure, however, a searcher can sometimes only
-  /// select from a subset of all states (depending on the update calls).
+  /// RandomPathSearcher performs a random walk of the ExecutionTree to select a
+  /// state. ExecutionTree is a global data structure, however, a searcher can
+  /// sometimes only select from a subset of all states (depending on the update
+  /// calls).
   ///
-  /// To support this, RandomPathSearcher has a subgraph view of PTree, in that it
-  /// only walks the PTreeNodes that it "owns". Ownership is stored in the
-  /// getInt method of the PTreeNodePtr class (which hides it in the pointer itself).
+  /// To support this, RandomPathSearcher has a subgraph view of ExecutionTree,
+  /// in that it only walks the ExecutionTreeNodes that it "owns". Ownership is
+  /// stored in the getInt method of the ExecutionTreeNodePtr class (which hides
+  /// it in the pointer itself).
   ///
-  /// The current implementation of PTreeNodePtr supports only 3 instances of the
-  /// RandomPathSearcher. This is because the current PTreeNodePtr implementation
-  /// conforms to C++ and only steals the last 3 alignment bits. This restriction
-  /// could be relaxed slightly by an architecture-specific implementation of
-  /// PTreeNodePtr that also steals the top bits of the pointer.
+  /// The current implementation of ExecutionTreeNodePtr supports only 3
+  /// instances of the RandomPathSearcher. This is because the current
+  /// ExecutionTreeNodePtr implementation conforms to C++ and only steals the
+  /// last 3 alignment bits. This restriction could be relaxed slightly by an
+  /// architecture-specific implementation of ExecutionTreeNodePtr that also
+  /// steals the top bits of the pointer.
   ///
   /// The ownership bits are maintained in the update method.
   class RandomPathSearcher final : public Searcher {
-    InMemoryPTree *processTree;
+    InMemoryExecutionTree *executionTree;
     RNG &theRNG;
 
     // Unique bitmask of this searcher
     const uint8_t idBitMask;
 
   public:
-    /// \param processTree The process tree.
+    /// \param executionTree The execution tree.
     /// \param RNG A random number generator.
-    RandomPathSearcher(InMemoryPTree *processTree, RNG &rng);
+    RandomPathSearcher(InMemoryExecutionTree *executionTree, RNG &rng);
     ~RandomPathSearcher() override = default;
 
     ExecutionState &selectState() override;
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 735075f1..7e0fd31f 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -100,19 +100,20 @@ bool userSearcherRequiresMD2U() {
           std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
 }
 
-bool userSearcherRequiresInMemoryPTree() {
+bool userSearcherRequiresInMemoryExecutionTree() {
   return std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end();
 }
 
 } // namespace klee
 
-Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree *processTree) {
+Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng,
+                         InMemoryExecutionTree *executionTree) {
   Searcher *searcher = nullptr;
   switch (type) {
     case Searcher::DFS: searcher = new DFSSearcher(); break;
     case Searcher::BFS: searcher = new BFSSearcher(); break;
     case Searcher::RandomState: searcher = new RandomSearcher(rng); break;
-    case Searcher::RandomPath: searcher = new RandomPathSearcher(processTree, rng); break;
+    case Searcher::RandomPath: searcher = new RandomPathSearcher(executionTree, rng); break;
     case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew, rng); break;
     case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered, rng); break;
     case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth, rng); break;
@@ -126,15 +127,16 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, InMemoryPTree
 }
 
 Searcher *klee::constructUserSearcher(Executor &executor) {
-  auto *ptree = llvm::dyn_cast<InMemoryPTree>(executor.processTree.get());
-  Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, ptree);
+  auto *etree =
+      llvm::dyn_cast<InMemoryExecutionTree>(executor.executionTree.get());
+  Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, etree);
 
   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, ptree));
+      s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, etree));
 
     searcher = new InterleavedSearcher(s);
   }
diff --git a/lib/Core/UserSearcher.h b/lib/Core/UserSearcher.h
index fe75eb6d..af582455 100644
--- a/lib/Core/UserSearcher.h
+++ b/lib/Core/UserSearcher.h
@@ -16,7 +16,7 @@ namespace klee {
 
   // XXX gross, should be on demand?
   bool userSearcherRequiresMD2U();
-  bool userSearcherRequiresInMemoryPTree();
+  bool userSearcherRequiresInMemoryExecutionTree();
 
   void initializeSearchOptions();