Renamed PTree to ExecutionTree (and similar)

27 files changed, 498 insertions, 457 deletions

diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h
index 152241c9..bee6e52a 100644
--- a/include/klee/Support/OptionCategories.h
+++ b/include/klee/Support/OptionCategories.h
@@ -29,7 +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 ExecTreeCat;
   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 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();
 
diff --git a/scripts/klee-control b/scripts/klee-control
index 0a918b42..e9d22db6 100755
--- a/scripts/klee-control
+++ b/scripts/klee-control
@@ -77,7 +77,7 @@ def main():
     if opts.dumpStates:
         execCmd(pid, "p dumpStates = 1", opts)        
     if opts.dumpTree:
-        execCmd(pid, "p dumpPTree = 1", opts)        
+        execCmd(pid, "p dumpExecutionTree = 1", opts)        
     if opts.stopForking:
         execCmd(pid, 'p stop_forking()', opts)    
     if opts.haltExecution:
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index ae038b80..a7d748c6 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-ptree klee-replay kleeRuntest ktest-gen ktest-randgen
+  DEPENDS klee kleaver klee-exec-tree klee-replay kleeRuntest ktest-gen ktest-randgen
   COMMENT "Running system tests"
   USES_TERMINAL
 )
diff --git a/test/Feature/KleeExecTreeBogus.test b/test/Feature/KleeExecTreeBogus.test
index 11fe87c8..5926d128 100644
--- a/test/Feature/KleeExecTreeBogus.test
+++ b/test/Feature/KleeExecTreeBogus.test
@@ -1,65 +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: not %klee-exec-tree tree-info %S/exec-tree-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
+CHECK-CORRUPT: Cannot 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/empty_db.csv nodes" 
+RUN: %klee-exec-tree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/duplicated_node.csv nodes" 
+RUN: not %klee-exec-tree 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
+CHECK-DUP: ExecutionTree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/invalid_btype.csv nodes" 
+RUN: not %klee-exec-tree 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
+CHECK-BTYPE: ExecutionTree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/invalid_ttype.csv nodes" 
+RUN: not %klee-exec-tree 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
+CHECK-TTYPE: ExecutionTree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/loop.csv nodes" 
+RUN: not %klee-exec-tree 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
+CHECK-LOOP: ExecutionTree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/missing_after_max.csv nodes" 
+RUN: not %klee-exec-tree 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
+CHECK-MISSA: ExecutionTree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/missing_before_max.csv nodes" 
+RUN: not %klee-exec-tree 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
+CHECK-MISSB: ExecutionTree 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: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/node_id0.csv nodes" 
+RUN: not %klee-exec-tree 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)
+CHECK-ID0: ExecutionTree DB contains illegal node ID (0)
 
 cleanup
 RUN rm -f %t.db
diff --git a/test/Feature/WriteExecutionTree.c b/test/Feature/WriteExecutionTree.c
index e7bf59ce..42f531a5 100644
--- a/test/Feature/WriteExecutionTree.c
+++ b/test/Feature/WriteExecutionTree.c
@@ -1,13 +1,13 @@
 // 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
+// RUN: %klee -write-exec-tree --output-dir=%t.klee-out %t.bc
+// RUN: %klee-exec-tree branches %t.klee-out/exec_tree.db | FileCheck --check-prefix=CHECK-BRANCH %s
+// RUN: %klee-exec-tree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s
+// RUN: %klee-exec-tree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s
+// RUN: %klee-exec-tree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s
+// RUN: %klee-exec-tree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s
+// RUN: %klee-exec-tree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s
+// RUN: not %klee-exec-tree dot %t.klee-out/exec-tree-doesnotexist.db
 
 #include "klee/klee.h"
 
@@ -61,7 +61,7 @@ int main(void) {
 // CHECK-TERM-DAG: User,2
 // CHECK-TERM-DAG: SilentExit,2
 
-// CHECK-DOT: strict digraph PTree {
+// CHECK-DOT: strict digraph ExecutionTree {
 // 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]+}}"];
diff --git a/test/lit.cfg b/test/lit.cfg
index 8abf7012..52869d34 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -139,7 +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-exec-tree', 'klee-exec-tree', ''),
          ('%klee-replay', 'klee-replay', ''),
          ('%klee-stats', 'klee-stats', ''),
          ('%klee-zesti', 'klee-zesti', ''),
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
index 40089c40..8c9128b4 100644
--- a/tools/CMakeLists.txt
+++ b/tools/CMakeLists.txt
@@ -10,7 +10,7 @@ add_subdirectory(ktest-gen)
 add_subdirectory(ktest-randgen)
 add_subdirectory(kleaver)
 add_subdirectory(klee)
-add_subdirectory(klee-ptree)
+add_subdirectory(klee-exec-tree)
 add_subdirectory(klee-replay)
 add_subdirectory(klee-stats)
 add_subdirectory(klee-zesti)
diff --git a/tools/klee-exec-tree/CMakeLists.txt b/tools/klee-exec-tree/CMakeLists.txt
index b5c3fa09..0c473d92 100644
--- a/tools/klee-exec-tree/CMakeLists.txt
+++ b/tools/klee-exec-tree/CMakeLists.txt
@@ -7,10 +7,10 @@
 #
 #===------------------------------------------------------------------------===#
 
-add_executable(klee-ptree main.cpp Tree.cpp DFSVisitor.cpp Printers.cpp)
+add_executable(klee-exec-tree 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})
+target_compile_features(klee-exec-tree PRIVATE cxx_std_17)
+target_include_directories(klee-exec-tree PRIVATE ${KLEE_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS})
+target_link_libraries(klee-exec-tree PUBLIC ${SQLite3_LIBRARIES})
 
-install(TARGETS klee-ptree DESTINATION bin)
+install(TARGETS klee-exec-tree DESTINATION bin)
diff --git a/tools/klee-exec-tree/DFSVisitor.h b/tools/klee-exec-tree/DFSVisitor.h
index 60d7b3bd..a61a3ff2 100644
--- a/tools/klee-exec-tree/DFSVisitor.h
+++ b/tools/klee-exec-tree/DFSVisitor.h
@@ -13,7 +13,7 @@
 
 #include <functional>
 
-/// @brief Traverses a process tree and calls registered callbacks for
+/// @brief Traverses an execution tree and calls registered callbacks for
 /// intermediate and leaf nodes (not the classical Visitor pattern).
 class DFSVisitor {
   // void _(node ID, node, depth)
diff --git a/tools/klee-exec-tree/Printers.cpp b/tools/klee-exec-tree/Printers.cpp
index 950d1b09..70a84017 100644
--- a/tools/klee-exec-tree/Printers.cpp
+++ b/tools/klee-exec-tree/Printers.cpp
@@ -163,7 +163,7 @@ void printEdges(std::uint32_t id, Node node, std::uint32_t depth) {
 void printDOT(const Tree &tree) {
   // header
   // - style defaults to intermediate nodes
-  std::cout << "strict digraph PTree {\n"
+  std::cout << "strict digraph ExecutionTree {\n"
                "node[shape=point,width=0.15,color=darkgrey];\n"
                "edge[color=darkgrey];\n\n";
 
diff --git a/tools/klee-exec-tree/Tree.cpp b/tools/klee-exec-tree/Tree.cpp
index 20772600..42b03ba2 100644
--- a/tools/klee-exec-tree/Tree.cpp
+++ b/tools/klee-exec-tree/Tree.cpp
@@ -20,7 +20,7 @@ Tree::Tree(const std::filesystem::path &path) {
   ::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::cerr << "Cannot open execution tree database: " << sqlite3_errmsg(db)
               << std::endl;
     exit(EXIT_FAILURE);
   }
@@ -31,7 +31,7 @@ Tree::Tree(const std::filesystem::path &path) {
       "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::cerr << "Cannot prepare read statement: " << sqlite3_errmsg(db)
               << std::endl;
     exit(EXIT_FAILURE);
   }
@@ -40,7 +40,7 @@ Tree::Tree(const std::filesystem::path &path) {
   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::cerr << "Cannot prepare max statement: " << sqlite3_errmsg(db)
               << std::endl;
     exit(EXIT_FAILURE);
   }
@@ -51,7 +51,7 @@ Tree::Tree(const std::filesystem::path &path) {
   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;
+    std::cerr << "Cannot read maximum ID: " << sqlite3_errmsg(db) << std::endl;
     exit(EXIT_FAILURE);
   }
 
@@ -74,20 +74,20 @@ Tree::Tree(const std::filesystem::path &path) {
 
     // sanity checks: valid indices
     if (ID == 0) {
-      std::cerr << "PTree DB contains illegal node ID (0)" << std::endl;
+      std::cerr << "ExecutionTree 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 "
+      std::cerr << "ExecutionTree 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): "
+      std::cerr << "Warning: ExecutionTree DB contains ambiguous node "
+                   "(0 vs. non-0 children): "
                 << ID << std::endl;
     }
 
@@ -161,9 +161,10 @@ void Tree::sanityCheck() {
     stack.pop_back();
 
     if (!visited.insert(id).second) {
-      std::cerr << "PTree DB contains duplicate child reference or circular "
-                   "structure. Affected node: "
-                << id << std::endl;
+      std::cerr
+          << "ExecutionTree DB contains duplicate child reference or circular "
+             "structure. Affected node: "
+          << id << std::endl;
       exit(EXIT_FAILURE);
     }
 
@@ -173,8 +174,8 @@ void Tree::sanityCheck() {
     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;
+      std::cerr << "ExecutionTree DB references undefined node. Affected node: "
+                << id << std::endl;
       exit(EXIT_FAILURE);
     }
 
@@ -187,7 +188,7 @@ void Tree::sanityCheck() {
       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 ("
+        std::cerr << "ExecutionTree DB contains unknown branch type ("
                   << (unsigned)static_cast<std::uint8_t>(branchType)
                   << ") in node " << id << std::endl;
         exit(EXIT_FAILURE);
@@ -198,7 +199,7 @@ void Tree::sanityCheck() {
       const auto terminationType = std::get<StateTerminationType>(node.kind);
       if (validTerminationTypes.count(terminationType) == 0 ||
           terminationType == StateTerminationType::RUNNING) {
-        std::cerr << "PTree DB contains unknown termination type ("
+        std::cerr << "ExecutionTree 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-exec-tree/Tree.h b/tools/klee-exec-tree/Tree.h
index 65b7baeb..40e04389 100644
--- a/tools/klee-exec-tree/Tree.h
+++ b/tools/klee-exec-tree/Tree.h
@@ -25,7 +25,7 @@ inline std::unordered_map<BranchType, std::string> branchTypeNames;
 inline std::unordered_map<StateTerminationType, std::string>
     terminationTypeNames;
 
-///@brief A Tree node representing a PTreeNode
+///@brief A Tree node representing an ExecutionTreeNode
 struct Node final {
   std::uint32_t left{0};
   std::uint32_t right{0};
@@ -34,7 +34,7 @@ struct Node final {
   std::variant<BranchType, StateTerminationType> kind{BranchType::NONE};
 };
 
-///@brief An in-memory representation of a complete process tree
+///@brief An in-memory representation of a complete execution tree
 class Tree final {
   /// Creates branchTypeNames and terminationTypeNames maps
   static void initialiseTypeNames();
@@ -45,9 +45,9 @@ class Tree final {
 
 public:
   /// sorted vector of Nodes default initialised with BranchType::NONE
-  std::vector<Node> nodes; // PTree node IDs start with 1!
+  std::vector<Node> nodes; // ExecutionTree node IDs start with 1!
 
-  /// Reads complete ptree.db into memory
+  /// Reads complete exec-tree.db into memory
   explicit Tree(const std::filesystem::path &path);
   ~Tree() = default;
 };
diff --git a/tools/klee-exec-tree/main.cpp b/tools/klee-exec-tree/main.cpp
index 96d2be75..efe28d04 100644
--- a/tools/klee-exec-tree/main.cpp
+++ b/tools/klee-exec-tree/main.cpp
@@ -16,7 +16,7 @@
 namespace fs = std::filesystem;
 
 void print_usage() {
-  std::cout << "Usage: klee-ptree <option> /path[/ptree.db]\n\n"
+  std::cout << "Usage: klee-exec-tree <option> /path[/exec_tree.db]\n\n"
                "Options:\n"
                "\tbranches     -  print branch statistics in csv format\n"
                "\tdepths       -  print depths statistics in csv format\n"
@@ -56,7 +56,7 @@ int main(int argc, char *argv[]) {
   // create tree
   fs::path path{argv[2]};
   if (fs::is_directory(path))
-    path /= "ptree.db";
+    path /= "exec_tree.db";
   if (!fs::exists(path)) {
     std::cerr << "Cannot open " << path << '\n';
     exit(EXIT_FAILURE);
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index ce231967..febeb47f 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1120,11 +1120,10 @@ int main(int argc, char **argv, char **envp) {
   atexit(llvm_shutdown); // Call llvm_shutdown() on exit
 
   KCommandLine::KeepOnlyCategories(
-     {&ChecksCat,      &DebugCat,    &ExtCallsCat, &ExprCat,   &LinkCat,
-      &MemoryCat,      &MergeCat,    &MiscCat,     &ModuleCat, &ReplayCat,
-      &SearchCat,      &SeedingCat,  &SolvingCat,  &StartCat,  &StatsCat,
-      &TerminationCat, &TestCaseCat, &TestGenCat,  &PTreeCat});
-
+     {&ChecksCat,      &DebugCat,    &ExtCallsCat, &ExprCat,     &LinkCat,
+      &MemoryCat,      &MergeCat,    &MiscCat,     &ModuleCat,   &ReplayCat,
+      &SearchCat,      &SeedingCat,  &SolvingCat,  &StartCat,    &StatsCat,
+      &TerminationCat, &TestCaseCat, &TestGenCat,  &ExecTreeCat, &ExecTreeCat});
   llvm::InitializeNativeTarget();
 
   parseArguments(argc, argv);
diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp
index f9089615..8b3ba7df 100644
--- a/unittests/Searcher/SearcherTest.cpp
+++ b/unittests/Searcher/SearcherTest.cpp
@@ -10,10 +10,10 @@
 
 #include "gtest/gtest.h"
 
-#include "klee/ADT/RNG.h"
 #include "Core/ExecutionState.h"
-#include "Core/PTree.h"
+#include "Core/ExecutionTree.h"
 #include "Core/Searcher.h"
+#include "klee/ADT/RNG.h"
 
 #include "llvm/Support/raw_ostream.h"
 
@@ -24,10 +24,10 @@ namespace {
 TEST(SearcherTest, RandomPath) {
   // First state
   ExecutionState es;
-  InMemoryPTree processTree(es);
+  InMemoryExecutionTree executionTree(es);
 
   RNG rng;
-  RandomPathSearcher rp(&processTree, rng);
+  RandomPathSearcher rp(&executionTree, rng);
   EXPECT_TRUE(rp.empty());
 
   rp.update(nullptr, {&es}, {});
@@ -36,7 +36,8 @@ TEST(SearcherTest, RandomPath) {
 
   // Two states
   ExecutionState es1(es);
-  processTree.attach(es.ptreeNode, &es1, &es, BranchType::Conditional);
+  executionTree.attach(es.executionTreeNode, &es1, &es,
+                       BranchType::Conditional);
   rp.update(&es, {&es1}, {});
 
   // Random path seed dependant
@@ -50,27 +51,28 @@ TEST(SearcherTest, RandomPath) {
   }
 
   rp.update(&es, {&es1}, {&es});
-  processTree.remove(es.ptreeNode);
+  executionTree.remove(es.executionTreeNode);
   for (int i = 0; i < 100; i++) {
     EXPECT_EQ(&rp.selectState(), &es1);
   }
 
   rp.update(&es1, {}, {&es1});
-  processTree.remove(es1.ptreeNode);
+  executionTree.remove(es1.executionTreeNode);
   EXPECT_TRUE(rp.empty());
 }
 
 TEST(SearcherTest, TwoRandomPath) {
   // Root state
   ExecutionState root;
-  InMemoryPTree processTree(root);
+  InMemoryExecutionTree executionTree(root);
 
   ExecutionState es(root);
-  processTree.attach(root.ptreeNode, &es, &root, BranchType::Conditional);
+  executionTree.attach(root.executionTreeNode, &es, &root,
+                       BranchType::Conditional);
 
   RNG rng, rng1;
-  RandomPathSearcher rp(&processTree, rng);
-  RandomPathSearcher rp1(&processTree, rng1);
+  RandomPathSearcher rp(&executionTree, rng);
+  RandomPathSearcher rp1(&executionTree, rng1);
   EXPECT_TRUE(rp.empty());
   EXPECT_TRUE(rp1.empty());
 
@@ -81,7 +83,8 @@ TEST(SearcherTest, TwoRandomPath) {
 
   // Two states
   ExecutionState es1(es);
-  processTree.attach(es.ptreeNode, &es1, &es, BranchType::Conditional);
+  executionTree.attach(es.executionTreeNode, &es1, &es,
+                       BranchType::Conditional);
 
   rp.update(&es, {}, {});
   rp1.update(nullptr, {&es1}, {});
@@ -101,49 +104,50 @@ TEST(SearcherTest, TwoRandomPath) {
   }
 
   rp1.update(&es, {}, {&es});
-  processTree.remove(es.ptreeNode);
+  executionTree.remove(es.executionTreeNode);
   EXPECT_TRUE(rp1.empty());
   EXPECT_EQ(&rp.selectState(), &es1);
 
   rp.update(&es1, {}, {&es1});
-  processTree.remove(es1.ptreeNode);
+  executionTree.remove(es1.executionTreeNode);
   EXPECT_TRUE(rp.empty());
   EXPECT_TRUE(rp1.empty());
 
-  processTree.remove(root.ptreeNode);
+  executionTree.remove(root.executionTreeNode);
 }
 
 TEST(SearcherTest, TwoRandomPathDot) {
-  std::stringstream modelPTreeDot;
-  PTreeNode *rootPNode, *rightLeafPNode, *esParentPNode, *es1LeafPNode,
-      *esLeafPNode;
+  std::stringstream modelExecutionTreeDot;
+  ExecutionTreeNode *rootExecutionTreeNode, *rightLeafExecutionTreeNode,
+      *esParentExecutionTreeNode, *es1LeafExecutionTreeNode,
+      *esLeafExecutionTreeNode;
 
   // Root state
   ExecutionState root;
-  InMemoryPTree processTree(root);
-  rootPNode = root.ptreeNode;
+  InMemoryExecutionTree executionTree(root);
+  rootExecutionTreeNode = root.executionTreeNode;
 
   ExecutionState es(root);
-  processTree.attach(root.ptreeNode, &es, &root, BranchType::NONE);
-  rightLeafPNode = root.ptreeNode;
-  esParentPNode = es.ptreeNode;
+  executionTree.attach(root.executionTreeNode, &es, &root, BranchType::NONE);
+  rightLeafExecutionTreeNode = root.executionTreeNode;
+  esParentExecutionTreeNode = es.executionTreeNode;
 
   RNG rng;
-  RandomPathSearcher rp(&processTree, rng);
-  RandomPathSearcher rp1(&processTree, rng);
+  RandomPathSearcher rp(&executionTree, rng);
+  RandomPathSearcher rp1(&executionTree, rng);
 
   rp.update(nullptr, {&es}, {});
 
   ExecutionState es1(es);
-  processTree.attach(es.ptreeNode, &es1, &es, BranchType::NONE);
-  esLeafPNode = es.ptreeNode;
-  es1LeafPNode = es1.ptreeNode;
+  executionTree.attach(es.executionTreeNode, &es1, &es, BranchType::NONE);
+  esLeafExecutionTreeNode = es.executionTreeNode;
+  es1LeafExecutionTreeNode = es1.executionTreeNode;
 
   rp.update(&es, {}, {});
   rp1.update(nullptr, {&es1}, {});
 
-  // Compare PTree to model PTree
-  modelPTreeDot
+  // Compare ExecutionTree to model ExecutionTree
+  modelExecutionTreeDot
       << "digraph G {\n"
       << "\tsize=\"10,7.5\";\n"
       << "\tratio=fill;\n"
@@ -151,30 +155,29 @@ TEST(SearcherTest, TwoRandomPathDot) {
       << "\tcenter = \"true\";\n"
       << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
       << "\tedge [arrowsize=.3]\n"
-      << "\tn" << rootPNode << " [shape=diamond];\n"
-      << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b011];\n"
-      << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n"
-      << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n"
-      << "\tn" << esParentPNode << " [shape=diamond];\n"
-      << "\tn" << esParentPNode << " -> n" << es1LeafPNode
-      << " [label=0b010];\n"
-      << "\tn" << esParentPNode << " -> n" << esLeafPNode << " [label=0b001];\n"
-      << "\tn" << esLeafPNode << " [shape=diamond,fillcolor=green];\n"
-      << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << rootExecutionTreeNode << " [shape=diamond];\n"
+      << "\tn" << rootExecutionTreeNode << " -> n" << esParentExecutionTreeNode << " [label=0b011];\n"
+      << "\tn" << rootExecutionTreeNode << " -> n" << rightLeafExecutionTreeNode << " [label=0b000];\n"
+      << "\tn" << rightLeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << esParentExecutionTreeNode << " [shape=diamond];\n"
+      << "\tn" << esParentExecutionTreeNode << " -> n" << es1LeafExecutionTreeNode << " [label=0b010];\n"
+      << "\tn" << esParentExecutionTreeNode << " -> n" << esLeafExecutionTreeNode << " [label=0b001];\n"
+      << "\tn" << esLeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << es1LeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n"
       << "}\n";
-  std::string pTreeDot;
-  llvm::raw_string_ostream pTreeDotStream(pTreeDot);
-  processTree.dump(pTreeDotStream);
-  EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str());
+  std::string executionTreeDot;
+  llvm::raw_string_ostream executionTreeDotStream(executionTreeDot);
+  executionTree.dump(executionTreeDotStream);
+  EXPECT_EQ(modelExecutionTreeDot.str(), executionTreeDotStream.str());
 
   rp.update(&es, {&es1}, {&es});
   rp1.update(nullptr, {&es}, {&es1});
 
   rp1.update(&es, {}, {&es});
-  processTree.remove(es.ptreeNode);
+  executionTree.remove(es.executionTreeNode);
 
-  modelPTreeDot.str("");
-  modelPTreeDot
+  modelExecutionTreeDot.str("");
+  modelExecutionTreeDot
       << "digraph G {\n"
       << "\tsize=\"10,7.5\";\n"
       << "\tratio=fill;\n"
@@ -182,33 +185,32 @@ TEST(SearcherTest, TwoRandomPathDot) {
       << "\tcenter = \"true\";\n"
       << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
       << "\tedge [arrowsize=.3]\n"
-      << "\tn" << rootPNode << " [shape=diamond];\n"
-      << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b001];\n"
-      << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n"
-      << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n"
-      << "\tn" << esParentPNode << " [shape=diamond];\n"
-      << "\tn" << esParentPNode << " -> n" << es1LeafPNode
-      << " [label=0b001];\n"
-      << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << rootExecutionTreeNode << " [shape=diamond];\n"
+      << "\tn" << rootExecutionTreeNode << " -> n" << esParentExecutionTreeNode << " [label=0b001];\n"
+      << "\tn" << rootExecutionTreeNode << " -> n" << rightLeafExecutionTreeNode << " [label=0b000];\n"
+      << "\tn" << rightLeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << esParentExecutionTreeNode << " [shape=diamond];\n"
+      << "\tn" << esParentExecutionTreeNode << " -> n" << es1LeafExecutionTreeNode << " [label=0b001];\n"
+      << "\tn" << es1LeafExecutionTreeNode << " [shape=diamond,fillcolor=green];\n"
       << "}\n";
 
-  pTreeDot = "";
-  processTree.dump(pTreeDotStream);
-  EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str());
-  processTree.remove(es1.ptreeNode);
-  processTree.remove(root.ptreeNode);
+  executionTreeDot = "";
+  executionTree.dump(executionTreeDotStream);
+  EXPECT_EQ(modelExecutionTreeDot.str(), executionTreeDotStream.str());
+  executionTree.remove(es1.executionTreeNode);
+  executionTree.remove(root.executionTreeNode);
 }
 
 TEST(SearcherDeathTest, TooManyRandomPaths) {
   // First state
   ExecutionState es;
-  InMemoryPTree processTree(es);
-  processTree.remove(es.ptreeNode); // Need to remove to avoid leaks
+  InMemoryExecutionTree executionTree(es);
+  executionTree.remove(es.executionTreeNode); // 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(&executionTree, rng);
+  RandomPathSearcher rp1(&executionTree, rng);
+  RandomPathSearcher rp2(&executionTree, rng);
+  ASSERT_DEATH({ RandomPathSearcher rp3(&executionTree, rng); }, "");
 }
 }