diff --git a/backends/p4tools/modules/testgen/CMakeLists.txt b/backends/p4tools/modules/testgen/CMakeLists.txt
index d7ada862e9..16c06fe905 100644
--- a/backends/p4tools/modules/testgen/CMakeLists.txt
+++ b/backends/p4tools/modules/testgen/CMakeLists.txt
@@ -25,8 +25,7 @@ set(
   core/symbolic_executor/depth_first.cpp
   core/symbolic_executor/selected_branches.cpp
   core/symbolic_executor/random_backtrack.cpp
-  core/symbolic_executor/greedy_stmt_cov.cpp
-  core/symbolic_executor/max_stmt_cov.cpp
+  core/symbolic_executor/greedy_node_cov.cpp
   core/symbolic_executor/symbolic_executor.cpp
   core/target.cpp
 
diff --git a/backends/p4tools/modules/testgen/README.md b/backends/p4tools/modules/testgen/README.md
index 38f47e20b6..3acc04ae24 100644
--- a/backends/p4tools/modules/testgen/README.md
+++ b/backends/p4tools/modules/testgen/README.md
@@ -74,7 +74,7 @@ To access the possible options for `p4testgen` use `p4testgen --help`. To genera
 Where `ARCH` specifies the P4 architecture (e.g., v1model.p4) and `TARGET` represents the targeted network device (e.g., BMv2). Choosing `0` as the option for max-tests will cause P4Testgen to generate tests until it has exhausted all possible paths.
 
 ### Coverage
-P4Testgen is able to track the (source code) coverage of the program it is generating tests for. With each test, P4Testgen can emit the cumulative program coverage it has achieved so far. Test 1 may have covered 2 out 10 P4 statements, test 2 5 out of 10 P4 statements, and so on. To enable program coverage, P4Testgen provides the `--track-coverage [NODE_TYPE]` option where `NODE_TYPE` refers to a particular P4 source node. Currently, `STATEMENTS` for P4 program statements and `TABLE_ENTRIES` for constant P4 table entries are supported. Multiple uses of `--track-coverage` are possible.
+P4Testgen is able to track the (source code) coverage of the program it is generating tests for. With each test, P4Testgen can emit the cumulative program coverage it has achieved so far. Test 1 may have covered 2 out 10 P4 nodes, test 2 5 out of 10 P4 nodes, and so on. To enable program coverage, P4Testgen provides the `--track-coverage [NODE_TYPE]` option where `NODE_TYPE` refers to a particular P4 source node. Currently, `STATEMENTS` for P4 program statements and `TABLE_ENTRIES` for constant P4 table entries are supported. Multiple uses of `--track-coverage` are possible.
 
 The option `--stop-metric MAX_NODE_COVERAGE` makes P4Testgen stop once it has hit 100% coverage as determined by `--track-coverage`.
 
diff --git a/backends/p4tools/modules/testgen/benchmarks/test_coverage.py b/backends/p4tools/modules/testgen/benchmarks/test_coverage.py
index 2a87445a0a..921eeb0813 100644
--- a/backends/p4tools/modules/testgen/benchmarks/test_coverage.py
+++ b/backends/p4tools/modules/testgen/benchmarks/test_coverage.py
@@ -181,12 +181,12 @@ def parse_coverage_and_timestamps(test_files, parse_type):
                         datestr = datestr.replace("\n", "")
                     datestr = datestr.strip()
                     datestrs.append(datestr)
-                if "Current statement coverage:" in line:
+                if "Current node coverage:" in line:
                     if parse_type == "PROTOBUF":
-                        covstr = line.replace('metadata: "Current statement coverage: ', "")
+                        covstr = line.replace('metadata: "Current node coverage: ', "")
                         covstr = covstr.replace('"\n', "")
                     else:
-                        covstr = line.replace("# Current statement coverage: ", "")
+                        covstr = line.replace("# Current node coverage: ", "")
                     covstr = covstr.replace("\n", "")
                     cov_percentages.append(float(covstr))
     return cov_percentages, datestrs
@@ -230,15 +230,15 @@ def run_strategies_for_max_tests(options, test_args):
     testutils.exec_process(cmd, env=custom_env, capture_output=True, timeout=3600)
     end_timestamp = datetime.datetime.now()
 
-    statements_cov, timestamps = collect_data_from_folder(test_args.test_dir, options.test_backend)
-    if not statements_cov:
+    nodes_cov, timestamps = collect_data_from_folder(test_args.test_dir, options.test_backend)
+    if not nodes_cov:
         print("No errors found!")
         return [], [], []
     num_tests = len(timestamps)
-    final_cov = str(statements_cov[-1])
+    final_cov = str(nodes_cov[-1])
     time_needed = (end_timestamp - start_timestamp).total_seconds()
     print(
-        f"Pct Statements Covered: {final_cov} Number of tests: {num_tests} Time needed:"
+        f"Pct Nodes Covered: {final_cov} Number of tests: {num_tests} Time needed:"
         f" {time_needed}"
     )
 
@@ -252,7 +252,7 @@ def run_strategies_for_max_tests(options, test_args):
         perf["Percentage"]["step"],
         perf["Percentage"]["backend"],
     ]
-    return summarized_data, statements_cov, timestamps
+    return summarized_data, nodes_cov, timestamps
 
 
 def plot_coverage(out_dir, coverage_pairs):
@@ -362,15 +362,15 @@ def main(args, extra_args):
             test_args.extra_args = config[strategy]
             if options.extra_args:
                 test_args.extra_args += " " + " ".join(options.extra_args[1:])
-            summarized_data, statements_cov, timestamps = run_strategies_for_max_tests(
+            summarized_data, nodes_cov, timestamps = run_strategies_for_max_tests(
                 options, test_args
             )
             data_row.extend(summarized_data)
             summary_frame.loc[len(summary_frame)] = data_row
-            coverage_pairs[str(seed)] = statements_cov
+            coverage_pairs[str(seed)] = nodes_cov
             sub_frame = pd.DataFrame()
-            sub_frame["Seed"] = [seed] * len(statements_cov)
-            sub_frame["Coverage"] = statements_cov
+            sub_frame["Seed"] = [seed] * len(nodes_cov)
+            sub_frame["Coverage"] = nodes_cov
             sub_frame["Time"] = convert_timestamps_to_timedelta(timestamps)
             sub_frame["Time"] = sub_frame["Time"] / pd.Timedelta(milliseconds=1)
 
diff --git a/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp
index b5cd8dab2f..0701afc407 100644
--- a/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp
@@ -232,7 +232,7 @@ bool CmdStepper::preorder(const IR::IfStatement *ifStatement) {
         nextState.replaceTopBody(&cmds);
 
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(state);
@@ -250,7 +250,7 @@ bool CmdStepper::preorder(const IR::IfStatement *ifStatement) {
         nextState.replaceTopBody((ifStatement->ifFalse == nullptr) ? new IR::BlockStatement()
                                                                    : ifStatement->ifFalse);
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(state);
@@ -554,7 +554,7 @@ bool CmdStepper::preorder(const IR::SwitchStatement *switchStatement) {
         for (const auto *switchCase : switchStatement->cases) {
             if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
                 // Some path selection strategies depend on looking ahead and collecting potential
-                // statements. If that is the case, apply the CoverableNodesScanner visitor.
+                // nodes. If that is the case, apply the CoverableNodesScanner visitor.
                 auto collector = CoverableNodesScanner(state);
                 collector.updateNodeCoverage(switchCase->statement, coveredNodes);
             }
diff --git a/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp
index ee3b48b96f..5498eb6420 100644
--- a/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp
@@ -234,7 +234,7 @@ bool ExprStepper::preorder(const IR::Mux *mux) {
 
         auto &nextState = state.clone();
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(state);
@@ -386,7 +386,7 @@ bool ExprStepper::preorder(const IR::SelectExpression *selectExpression) {
         const auto *decl = state.findDecl(selectCase->state)->getNode();
         nextState.replaceTopBody(Continuation::Return(decl));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(state);
diff --git a/backends/p4tools/modules/testgen/core/small_step/small_step.cpp b/backends/p4tools/modules/testgen/core/small_step/small_step.cpp
index c727ddc8fc..b035fcb4bf 100644
--- a/backends/p4tools/modules/testgen/core/small_step/small_step.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/small_step.cpp
@@ -50,10 +50,10 @@ SmallStepEvaluator::Branch::Branch(std::optional<const Constraint *> c,
 
 SmallStepEvaluator::Branch::Branch(std::optional<const Constraint *> c,
                                    const ExecutionState &prevState, ExecutionState &nextState,
-                                   P4::Coverage::CoverageSet potentialStatements)
+                                   P4::Coverage::CoverageSet potentialNodes)
     : constraint(IR::getBoolLiteral(true)),
       nextState(nextState),
-      potentialStatements(std::move(potentialStatements)) {
+      potentialNodes(std::move(potentialNodes)) {
     if (c) {
         // Evaluate the branch constraint in the current state of symbolic environment.
         // Substitutes all variables to their symbolic value (expression on the program's initial
diff --git a/backends/p4tools/modules/testgen/core/small_step/small_step.h b/backends/p4tools/modules/testgen/core/small_step/small_step.h
index 4ee38896ad..d9e081d4fa 100644
--- a/backends/p4tools/modules/testgen/core/small_step/small_step.h
+++ b/backends/p4tools/modules/testgen/core/small_step/small_step.h
@@ -30,7 +30,7 @@ class SmallStepEvaluator {
 
         ExecutionStateReference nextState;
 
-        P4::Coverage::CoverageSet potentialStatements;
+        P4::Coverage::CoverageSet potentialNodes;
 
         /// Simple branch without any constraint.
         explicit Branch(ExecutionState &nextState);
@@ -43,7 +43,7 @@ class SmallStepEvaluator {
         /// Branch constrained by a condition. prevState is the state in which the condition
         /// is later evaluated.
         Branch(std::optional<const Constraint *> c, const ExecutionState &prevState,
-               ExecutionState &nextState, P4::Coverage::CoverageSet potentialStatements);
+               ExecutionState &nextState, P4::Coverage::CoverageSet potentialNodes);
     };
 
     using Result = std::vector<Branch> *;
diff --git a/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
index 840cf566d6..da6162382f 100644
--- a/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
@@ -220,7 +220,7 @@ const IR::Expression *TableStepper::evalTableConstEntries() {
         nextState.set(getTableHitVar(table), IR::getBoolLiteral(true));
         nextState.set(getTableReachedVar(table), IR::getBoolLiteral(true));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(stepper->state);
@@ -314,7 +314,7 @@ void TableStepper::setTableDefaultEntries(
         replacements.emplace_back(
             new IR::MethodCallStatement(Util::SourceInfo(), synthesizedAction));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(stepper->state);
@@ -389,7 +389,7 @@ void TableStepper::evalTableControlEntries(
         replacements.emplace_back(
             new IR::MethodCallStatement(Util::SourceInfo(), synthesizedAction));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(stepper->state);
@@ -546,7 +546,7 @@ void TableStepper::addDefaultAction(std::optional<const IR::Expression *> tableM
     nextState.add(*new TraceEvents::Generic(tableStream.str()));
     replacements.emplace_back(new IR::MethodCallStatement(Util::SourceInfo(), tableAction));
     // Some path selection strategies depend on looking ahead and collecting potential
-    // statements.
+    // nodes.
     P4::Coverage::CoverageSet coveredNodes;
     if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
         auto collector = CoverableNodesScanner(stepper->state);
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.cpp b/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.cpp
similarity index 87%
rename from backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.cpp
rename to backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.cpp
index 772ce90f81..7378494fb8 100644
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.cpp
+++ b/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.cpp
@@ -1,4 +1,4 @@
-#include "backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.h"
+#include "backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.h"
 
 #include <cstddef>
 #include <functional>
@@ -18,26 +18,26 @@
 
 namespace P4Tools::P4Testgen {
 
-GreedyStmtSelection::GreedyStmtSelection(AbstractSolver &solver, const ProgramInfo &programInfo)
+GreedyNodeSelection::GreedyNodeSelection(AbstractSolver &solver, const ProgramInfo &programInfo)
     : SymbolicExecutor(solver, programInfo) {}
 
-std::optional<SymbolicExecutor::Branch> GreedyStmtSelection::popPotentialBranch(
-    const P4::Coverage::CoverageSet &coveredStatements,
+std::optional<SymbolicExecutor::Branch> GreedyNodeSelection::popPotentialBranch(
+    const P4::Coverage::CoverageSet &coveredNodes,
     std::vector<SymbolicExecutor::Branch> &candidateBranches) {
     for (size_t idx = 0; idx < candidateBranches.size(); ++idx) {
         auto branch = candidateBranches.at(idx);
-        // First check all the potential set of statements we can cover by looking ahead.
-        for (const auto &stmt : branch.potentialStatements) {
-            if (coveredStatements.count(stmt) == 0U) {
+        // First check all the potential set of nodes we can cover by looking ahead.
+        for (const auto &stmt : branch.potentialNodes) {
+            if (coveredNodes.count(stmt) == 0U) {
                 candidateBranches[idx] = candidateBranches.back();
                 candidateBranches.pop_back();
                 return branch;
             }
         }
-        // If we did not find anything, check whether this state covers any new statements
+        // If we did not find anything, check whether this state covers any new nodes
         // already.
         for (const auto &stmt : branch.nextState.get().getVisited()) {
-            if (coveredStatements.count(stmt) == 0U) {
+            if (coveredNodes.count(stmt) == 0U) {
                 candidateBranches[idx] = candidateBranches.back();
                 candidateBranches.pop_back();
                 return branch;
@@ -47,7 +47,7 @@ std::optional<SymbolicExecutor::Branch> GreedyStmtSelection::popPotentialBranch(
     return std::nullopt;
 }
 
-std::optional<ExecutionStateReference> GreedyStmtSelection::pickSuccessor(StepResult successors) {
+std::optional<ExecutionStateReference> GreedyNodeSelection::pickSuccessor(StepResult successors) {
     if (successors->empty()) {
         return std::nullopt;
     }
@@ -60,7 +60,7 @@ std::optional<ExecutionStateReference> GreedyStmtSelection::pickSuccessor(StepRe
     // Only perform a greedy search if we are still producing tests consistently.
     // This guard is necessary to avoid getting caught in parser loops.
     if (stepsWithoutTest < MAX_STEPS_WITHOUT_TEST) {
-        // Try to find a branch that covers new statements.
+        // Try to find a branch that covers new nodes.
         auto branch = popPotentialBranch(getVisitedNodes(), *successors);
         // If we succeed, pick the branch and add the remainder to the list of
         // potential branches.
@@ -78,7 +78,7 @@ std::optional<ExecutionStateReference> GreedyStmtSelection::pickSuccessor(StepRe
     return nextState;
 }
 
-void GreedyStmtSelection::runImpl(const Callback &callBack,
+void GreedyNodeSelection::runImpl(const Callback &callBack,
                                   ExecutionStateReference executionState) {
     while (true) {
         try {
@@ -130,7 +130,7 @@ void GreedyStmtSelection::runImpl(const Callback &callBack,
         unexploredBranches.insert(unexploredBranches.end(), potentialBranches.begin(),
                                   potentialBranches.end());
         potentialBranches.clear();
-        // If we did not find any new statements, fall back to random.
+        // If we did not find any new nodes, fall back to random.
         executionState = popRandomBranch(unexploredBranches).nextState;
     }
 }
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.h b/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.h
similarity index 78%
rename from backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.h
rename to backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.h
index d2e417b778..be8d06cebc 100644
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.h
+++ b/backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.h
@@ -1,5 +1,5 @@
-#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_GREEDY_STMT_COV_H_
-#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_GREEDY_STMT_COV_H_
+#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_GREEDY_NODE_COV_H_
+#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_GREEDY_NODE_COV_H_
 
 #include <cstdint>
 #include <optional>
@@ -14,14 +14,14 @@
 namespace P4Tools::P4Testgen {
 
 /// Greedy path selection strategy, which, at branch points, picks the first execution state which
-/// has covered or potentially will cover program statements which have not been visited yet.
-/// Potential statements are computed using the CoverableNodesScanner visitor, which collects
-/// statements in the top-level statement of the execution state. These statements are latent
+/// has covered or potentially will cover program nodes which have not been visited yet.
+/// Potential nodes are computed using the CoverableNodesScanner visitor, which collects
+/// nodes in the top-level statement of the execution state. These nodes are latent
 /// because execution is not guaranteed. They may be guarded by an if condition or select
 /// expression. If the strategy does not find a new statement, it falls back to
 /// random. Similarly, if the strategy cycles without a test for a specific threshold, it will
 /// fall back to random. This is to prevent getting caught in a parser cycle.
-class GreedyStmtSelection : public SymbolicExecutor {
+class GreedyNodeSelection : public SymbolicExecutor {
  public:
     /// Executes the P4 program along a randomly chosen path. When the program terminates, the
     /// given callback is invoked. If the callback returns true, then the executor terminates.
@@ -29,7 +29,7 @@ class GreedyStmtSelection : public SymbolicExecutor {
     void runImpl(const Callback &callBack, ExecutionStateReference state) override;
 
     /// Constructor for this strategy, considering inheritance
-    GreedyStmtSelection(AbstractSolver &solver, const ProgramInfo &programInfo);
+    GreedyNodeSelection(AbstractSolver &solver, const ProgramInfo &programInfo);
 
  private:
     /// This variable keeps track of how many branch decisions we have made without producing a
@@ -40,7 +40,7 @@ class GreedyStmtSelection : public SymbolicExecutor {
     /// The maximum number of steps without generating a test before falling back to random.
     static const uint64_t MAX_STEPS_WITHOUT_TEST = 1000;
 
-    /// Branches which have the potential to cover new statements in the program.
+    /// Branches which have the potential to cover new nodes in the program.
     /// Each element on this vector represents a set of alternative choices that could have been
     /// made along the current execution path.
     ///
@@ -56,27 +56,27 @@ class GreedyStmtSelection : public SymbolicExecutor {
     /// Invariants:
     ///   - Each element of this vector is non-empty.
     ///   - Each element's path constraints are satisfiable.
-    ///   - There are no statements associated with the element's execution state that are
+    ///   - There are no nodes associated with the element's execution state that are
     ///   uncovered.
     std::vector<Branch> unexploredBranches;
 
     /// Iterate over all the input branches in @param candidateBranches and try to find a branch
-    /// which contains statements that are not in @param coveredStatements yet. Return the first
+    /// which contains nodes that are not in @param coverednodes yet. Return the first
     /// branch that was found and remove that branch from the container of @param candidateBranches.
     /// Return none, if no branch was found.
     static std::optional<SymbolicExecutor::Branch> popPotentialBranch(
-        const P4::Coverage::CoverageSet &coveredStatements,
+        const P4::Coverage::CoverageSet &coverednodes,
         std::vector<SymbolicExecutor::Branch> &candidateBranches);
 
     /// Try to pick a successor from the list of given successors. This involves three steps.
     /// 1. Filter out all the successors with unsatisfiable path conditions. If no successors are
     /// left, return false.
-    /// 2. If there are successors left, try to find a successor that covers new statements. Set the
+    /// 2. If there are successors left, try to find a successor that covers new nodes. Set the
     /// nextState as this successors state.
-    /// 3. If no successor with new statements was found set a random successor.
+    /// 3. If no successor with new nodes was found set a random successor.
     [[nodiscard]] std::optional<ExecutionStateReference> pickSuccessor(StepResult successors);
 };
 
 }  // namespace P4Tools::P4Testgen
 
-#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_GREEDY_STMT_COV_H_ */
+#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_GREEDY_NODE_COV_H_ */
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.cpp b/backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.cpp
deleted file mode 100644
index f02f1c3734..0000000000
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.cpp
+++ /dev/null
@@ -1,245 +0,0 @@
-#include "backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.h"
-
-#include <ctime>
-#include <functional>
-#include <map>
-#include <optional>
-#include <vector>
-
-#include "backends/p4tools/common/lib/util.h"
-#include "ir/ir.h"
-#include "lib/error.h"
-#include "lib/solver.h"
-#include "lib/source_file.h"
-
-#include "backends/p4tools/modules/testgen/core/program_info.h"
-#include "backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h"
-#include "backends/p4tools/modules/testgen/lib/exceptions.h"
-#include "backends/p4tools/modules/testgen/lib/execution_state.h"
-#include "backends/p4tools/modules/testgen/options.h"
-
-namespace P4Tools::P4Testgen {
-
-void RandomMaxStmtCoverage::runImpl(const Callback &callBack,
-                                    ExecutionStateReference executionState) {
-    // Loop until we reach terminate, or until there are no more
-    // branches to produce tests.
-    while (true) {
-        try {
-            if (executionState.get().isTerminal()) {
-                // We've reached the end of the program. Call back and (if desired) end execution.
-                bool terminate = handleTerminalState(callBack, executionState);
-                uint64_t coverage = visitedNodes.size();
-                // We set the coverage saddle track accordingly.
-                if (coverage == coverageSaddleTrack.first) {
-                    coverageSaddleTrack =
-                        std::make_pair(coverage, (coverageSaddleTrack.second + 1));
-                } else {
-                    coverageSaddleTrack = std::make_pair(coverage, 1);
-                }
-                if (terminate) {
-                    return;
-                }
-            } else {
-                // Take a step in the program, choose a random branch, and continue execution. If
-                // branch selection fails, fall through to the roll-back code below. To help reduce
-                // calls into the solver, only guarantee viability of the selected branch if more
-                // than one branch was produced.
-                // State successors are accompanied by branch constrain which should be evaluated
-                // in the state before the step was taken - we copy the current symbolic state.
-                StepResult successors = step(executionState);
-                bool guaranteeViability = successors->size() > 1;
-                ExecutionState *next = chooseBranch(*successors, guaranteeViability);
-                if (next != nullptr) {
-                    executionState = *next;
-                    continue;
-                }
-            }
-        } catch (TestgenUnimplemented &e) {
-            // If strict is enabled, bubble the exception up.
-            if (TestgenOptions::get().strict) {
-                throw;
-            }
-            // Otherwise we try to roll back as we typically do.
-            ::warning("Path encountered unimplemented feature. Message: %1%\n", e.what());
-        }
-        // Roll back to a previous branch and continue execution from there, but if there are no
-        // more branches to explore, finish execution. Not all branches are viable, so we loop
-        // until either we run out of unexplored branches or we find a viable branch.
-        while (true) {
-            // If the buffer and unexploredBranches itself are empty, there's nothing left to
-            // explore.
-            if (unexploredBranches.empty() && bufferUnexploredBranches.empty()) {
-                return;
-            }
-
-            bool guaranteeViability = true;
-            ExecutionState *next = nullptr;
-            if (unexploredBranches.empty() && !bufferUnexploredBranches.empty()) {
-                // If we don't have enough entires, then we just invoke the
-                // regular maxCoverage logic, i.e. we select the branches with
-                // higher number of unique non-visited statements.
-                auto successors = bufferUnexploredBranches.rbegin()->second;
-                // Remove the map entry accordingly.
-                auto coverageKey = bufferUnexploredBranches.rbegin()->first;
-                bufferUnexploredBranches.erase(coverageKey);
-                next = chooseBranch(successors, guaranteeViability);
-            } else {
-                // If we are stuck in a saddle point for too long,
-                // trust in the lookahead and take the higher ranks.
-                if (coverageSaddleTrack.second >= (2 * saddlePoint)) {
-                    // Empty unexploredBranches.
-                    updateBufferRankings();
-                    // Merge the contents of unexploredBranches in the buffer, then
-                    // empty it.
-                    for (auto &localBranches : unexploredBranches) {
-                        sortBranchesByCoverage(localBranches);
-                    }
-                    unexploredBranches.clear();
-                    // We set the coverage counter to the saddle point,
-                    // so we can combine it with random exploration.
-                    uint64_t coverage = visitedNodes.size();
-                    coverageSaddleTrack = std::make_pair(coverage, saddlePoint);
-                    // Get the highest rank in the map in terms of non-
-                    // visited statements.
-                    auto successors = bufferUnexploredBranches.rbegin()->second;
-                    // Remove the map entry accordingly.
-                    auto coverageKey = bufferUnexploredBranches.rbegin()->first;
-                    bufferUnexploredBranches.erase(coverageKey);
-                    next = chooseBranch(successors, guaranteeViability);
-                } else if (coverageSaddleTrack.second >= saddlePoint) {
-                    // Invoke random access iff we reach a saddle point.
-                    updateBufferRankings();
-                    // Merge the contents of unexploredBranches in the buffer, then
-                    // empty it.
-                    for (auto &localBranches : unexploredBranches) {
-                        sortBranchesByCoverage(localBranches);
-                    }
-                    unexploredBranches.clear();
-                    auto successorsKey = getRandomUnexploredMapEntry();
-                    auto successors = bufferUnexploredBranches.at(successorsKey);
-                    // Remove the map entry accordingly.
-                    bufferUnexploredBranches.erase(successorsKey);
-                    next = chooseBranch(successors, guaranteeViability);
-                } else {
-                    // Otherwise, just get the first element.
-                    auto successors = unexploredBranches.front();
-                    unexploredBranches.pop_front();
-                    next = chooseBranch(successors, guaranteeViability);
-                }
-            }
-            if (next != nullptr) {
-                executionState = *next;
-                break;
-            }
-        }
-    }
-}
-
-uint64_t RandomMaxStmtCoverage::getRandomUnexploredMapEntry() {
-    // Collect all the keys and select a random one.
-    std::vector<uint64_t> unexploredCoverageKeys;
-    unexploredCoverageKeys.reserve(bufferUnexploredBranches.size());
-    for (auto const &unexplored : bufferUnexploredBranches) {
-        unexploredCoverageKeys.push_back(unexplored.first);
-    }
-    size_t unexploredRange = unexploredCoverageKeys.size() - 1;
-    uint64_t exploreLevels = Utils::getRandInt(unexploredRange);
-    uint64_t coverageKey = unexploredCoverageKeys.at(exploreLevels);
-
-    return coverageKey;
-}
-
-void RandomMaxStmtCoverage::updateBufferRankings() {
-    // Collect all the keys
-    std::vector<uint64_t> unexploredCoverageKeys;
-    unexploredCoverageKeys.reserve(bufferUnexploredBranches.size());
-    for (auto const &unexplored : bufferUnexploredBranches) {
-        unexploredCoverageKeys.push_back(unexplored.first);
-    }
-    for (auto &coverageKey : unexploredCoverageKeys) {
-        auto localBranches = bufferUnexploredBranches.at(coverageKey);
-        bufferUnexploredBranches.erase(coverageKey);
-        sortBranchesByCoverage(localBranches);
-    }
-}
-
-void RandomMaxStmtCoverage::sortBranchesByCoverage(std::vector<Branch> &branches) {
-    // Transfers branches to rankedBranches and sorts them by coverage
-    for (const auto &localBranch : branches) {
-        // Calculate coverage for each branch:
-        uint64_t lookAheadCoverage = 0;
-        for (const auto &stmt : localBranch.potentialStatements) {
-            // We need to take into account the set of visitedNodes.
-            // We also need to ensure the statement is in allStatements.
-            if (visitedNodes.count(stmt) == 0U && stmt->getSourceInfo().isValid()) {
-                lookAheadCoverage++;
-            }
-        }
-        auto coverage = lookAheadCoverage + visitedNodes.size();
-
-        // If there's no element in bufferUnexploredBranches with the particular coverage
-        // we calculate, we'll insert a new key at bufferUnexploredBranches.
-        auto rankedBranches = bufferUnexploredBranches.find(coverage);
-        if (rankedBranches != bufferUnexploredBranches.end()) {
-            auto &localBranches = rankedBranches->second;
-            localBranches.push_back(localBranch);
-            bufferUnexploredBranches.emplace(coverage, localBranches);
-        } else {
-            std::vector<Branch> localBranches;
-            localBranches.push_back(localBranch);
-            bufferUnexploredBranches.insert(std::make_pair(coverage, localBranches));
-        }
-    }
-
-    // Clear branches and reinsert information from rankedBranches.
-    branches.clear();
-}
-
-ExecutionState *RandomMaxStmtCoverage::chooseBranch(std::vector<Branch> &branches,
-                                                    bool guaranteeViability) {
-    while (true) {
-        // Fail if we've run out of ranked branches.
-        if (branches.empty()) {
-            return nullptr;
-        }
-
-        // Pick and remove a branch randomly.
-        // All branches in this vector will have the same coverage.
-        auto branch = popRandomBranch(branches);
-
-        // Do not bother invoking the solver for a trivial case.
-        // In either case (true or false), we do not need to add the assertion and check.
-        if (const auto *boolLiteral = branch.constraint->to<IR::BoolLiteral>()) {
-            guaranteeViability = false;
-            if (!boolLiteral->value) {
-                continue;
-            }
-        }
-
-        if (guaranteeViability) {
-            // Check the consistency of the path constraints asserted so far.
-            auto solverResult = solver.checkSat(branch.nextState.get().getPathConstraint());
-            if (solverResult == std::nullopt) {
-                ::warning("Solver timed out");
-            }
-            if (solverResult == std::nullopt || !solverResult.value()) {
-                // Solver timed out or path constraints were not satisfiable. Need to choose a
-                // different branch. Roll back our branch selection and try again.
-                continue;
-            }
-        }
-        // Push the new set of branches if the remaining vector is not empty.
-        if (!branches.empty()) {
-            unexploredBranches.push_back(branches);
-        }
-
-        return &branch.nextState.get();
-    }
-}
-
-RandomMaxStmtCoverage::RandomMaxStmtCoverage(AbstractSolver &solver, const ProgramInfo &programInfo,
-                                             uint64_t saddlePoint)
-    : SymbolicExecutor(solver, programInfo), saddlePoint(saddlePoint) {}
-
-}  // namespace P4Tools::P4Testgen
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.h b/backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.h
deleted file mode 100644
index 7033c2be12..0000000000
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.h
+++ /dev/null
@@ -1,86 +0,0 @@
-#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_MAX_STMT_COV_H_
-#define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_MAX_STMT_COV_H_
-
-#include <cstdint>
-#include <list>
-#include <utility>
-#include <vector>
-
-#include "lib/ordered_map.h"
-#include "lib/solver.h"
-
-#include "backends/p4tools/modules/testgen/core/program_info.h"
-#include "backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h"
-#include "backends/p4tools/modules/testgen/lib/execution_state.h"
-
-namespace P4Tools::P4Testgen {
-
-/// Strategy that combines the incremental max coverage ("look-ahead") at the
-/// with random exploration. We rely on a sorted map containing rankings of unique
-/// non-visited statements and a vector, acting as a DFS, to direct a path to a
-/// terminating state. We keep track of coverage, and once we reach a saddle point,
-/// we pick a random branch. If we continue in the saddle point after for too long
-// i.e. 2* the saddle point, we try to stick with the highest ranked branches.
-class RandomMaxStmtCoverage : public SymbolicExecutor {
- public:
-    /// Executes the P4 program along a randomly chosen path. When the program terminates, the
-    /// given callback is invoked. If the callback returns true, then the executor terminates.
-    /// Otherwise, execution of the P4 program continues on a different random path.
-    void runImpl(const Callback &callBack, ExecutionStateReference executionState) override;
-
-    /// Constructor for this strategy, considering inheritance.
-    RandomMaxStmtCoverage(AbstractSolver &solver, const ProgramInfo &programInfo,
-                          uint64_t saddlePoint);
-
- protected:
-    // Saddle point indicates when we get stuck into a coverage and decides to take
-    // a random branch. Set by the user.
-    uint64_t saddlePoint;
-
-    // Explores other options in the bufferUnexploredBranches map with smaller visitedStatements.
-    // It randomly picks a key with a non-max number of unique non-visited statements to explore.
-    // Invoked when we reach the saddle point.
-    uint64_t getRandomUnexploredMapEntry();
-
-    // A vector buffering the unexplored branches and directing it to a terminal state.
-    std::list<std::vector<Branch>> unexploredBranches;
-
-    // First element is the number of non-visited statements, second element is the count
-    // of generated tests.
-    std::pair<uint64_t, uint64_t> coverageSaddleTrack = std::make_pair(0, 0);
-
-    // Buffer of unexploredBranches. It saves the unexplored branches,
-    // so we can restore them if getRandomUnexploredMapEntry finishes a path
-    // in unexploredBranches.
-    ordered_map<uint64_t, std::vector<Branch>> bufferUnexploredBranches;
-
-    /// Chooses a branch to take, sets the current execution state to be that branch, and asserts
-    /// the corresponding path constraint to the solver.
-    ///
-    /// If @arg guaranteeViability is true, then the cumulative path condition is guaranteed to be
-    /// satisfiable after taking into account the path constraint associated with the chosen
-    /// branch. Any unviable branches encountered during branch selection are discarded.
-    ///
-    /// Branch selection fails if the given set of branches is empty. It also fails if @arg
-    /// guaranteeViability is true, but none of the given branches are viable.
-    ///
-    /// On success, the remaining branches to explore are pushed onto the stack of unexplored
-    /// branches, and the solver's state before the branch selection is saved with a `push`
-    /// operation. This happens even if the set of remaining branches is empty. On failure, the
-    /// stack of unexplored branches and the solver's state will be unchanged.
-    ///
-    /// @returns next execution state to be examined on success, nullptr on failure.
-    ExecutionState *chooseBranch(std::vector<Branch> &branches, bool guaranteeViability);
-
-    /// Invoked in chooseBranch to sort the branches vector according to non-visited
-    /// states. It stores and ranks the branches from unexploredBranches.
-    void sortBranchesByCoverage(std::vector<Branch> &branches);
-
-    // Every time we take a random branch, we have to update the map according to the
-    // new rankings of non-visited statements.
-    void updateBufferRankings();
-};
-
-}  // namespace P4Tools::P4Testgen
-
-#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SYMBOLIC_EXECUTOR_MAX_STMT_COV_H_ */
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h b/backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h
index 5ac2518200..c5300c2235 100644
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h
+++ b/backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h
@@ -9,12 +9,10 @@ enum class PathSelectionPolicy {
     DepthFirst,
     RandomBacktrack,
     GreedyStmtCoverage,
-    RandomMaxStmtCoverage,
 };
 
 inline bool requiresLookahead(PathSelectionPolicy &pathSelectionPolicy) {
-    static const std::set LOOKAHEAD_STRATEGYIES = {PathSelectionPolicy::GreedyStmtCoverage,
-                                                   PathSelectionPolicy::RandomMaxStmtCoverage};
+    static const std::set LOOKAHEAD_STRATEGYIES = {PathSelectionPolicy::GreedyStmtCoverage};
     return LOOKAHEAD_STRATEGYIES.find(pathSelectionPolicy) != LOOKAHEAD_STRATEGYIES.end();
 }
 
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/random_backtrack.h b/backends/p4tools/modules/testgen/core/symbolic_executor/random_backtrack.h
index 3b8d2d98d3..88905a227a 100644
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/random_backtrack.h
+++ b/backends/p4tools/modules/testgen/core/symbolic_executor/random_backtrack.h
@@ -32,16 +32,16 @@ class RandomBacktrack : public SymbolicExecutor {
     /// Invariants:
     ///   - Each element of this vector is non-empty.
     ///   - Each element's path constraints are satisfiable.
-    ///   - There are no statements associated with the element's execution state that are
+    ///   - There are no nodes associated with the element's execution state that are
     ///   uncovered.
     std::vector<Branch> unexploredBranches;
 
     /// Try to pick a successor from the list of given successors. This involves three steps.
     /// 1. Filter out all the successors with unsatisfiable path conditions. If no successors are
     /// left, return false.
-    /// 2. If there are successors left, try to find a successor that covers new statements. Set the
+    /// 2. If there are successors left, try to find a successor that covers new nodes. Set the
     /// nextState as this successors state.
-    /// 3. If no successor with new statements was found set a random successor.
+    /// 3. If no successor with new nodes was found set a random successor.
     [[nodiscard]] std::optional<ExecutionStateReference> pickSuccessor(StepResult successors);
 };
 
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.cpp b/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.cpp
index 9ab231f766..ba1280f0c6 100644
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.cpp
+++ b/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.cpp
@@ -81,7 +81,6 @@ bool SymbolicExecutor::evaluateBranch(const SymbolicExecutor::Branch &branch,
 
 SymbolicExecutor::Branch SymbolicExecutor::popRandomBranch(
     std::vector<SymbolicExecutor::Branch> &candidateBranches) {
-    // If we did not find any new statements, fall back to random.
     auto branchIdx = Utils::getRandInt(candidateBranches.size() - 1);
     auto branch = candidateBranches[branchIdx];
     candidateBranches[branchIdx] = candidateBranches.back();
diff --git a/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h b/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h
index c3aab8e35f..3dc22c05a9 100644
--- a/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h
+++ b/backends/p4tools/modules/testgen/core/symbolic_executor/symbolic_executor.h
@@ -54,7 +54,7 @@ class SymbolicExecutor {
     /// Getter to access visitedNodes.
     const P4::Coverage::CoverageSet &getVisitedNodes();
 
-    /// Update the set of visited statements.
+    /// Update the set of visited nodes.
     void updateVisitedNodes(const P4::Coverage::CoverageSet &newNodes);
 
  protected:
@@ -64,10 +64,10 @@ class SymbolicExecutor {
     /// The SMT solver backing this executor.
     AbstractSolver &solver;
 
-    /// Set of all statements, to be retrieved from programInfo.
+    /// Set of all nodes, to be retrieved from programInfo.
     const P4::Coverage::CoverageSet &coverableNodes;
 
-    /// Set of all statements executed in any testcase that has been outputted.
+    /// Set of all nodes executed in any testcase that has been outputted.
     P4::Coverage::CoverageSet visitedNodes;
 
     /// Handles processing at the end of a P4 program.
diff --git a/backends/p4tools/modules/testgen/lib/execution_state.h b/backends/p4tools/modules/testgen/lib/execution_state.h
index c7288435c9..e7c7f681dc 100644
--- a/backends/p4tools/modules/testgen/lib/execution_state.h
+++ b/backends/p4tools/modules/testgen/lib/execution_state.h
@@ -125,7 +125,7 @@ class ExecutionState : public AbstractExecutionState {
     /// List of branch decisions leading into this state.
     std::vector<uint64_t> selectedBranches;
 
-    /// State that is needed to track reachability of statements given a query.
+    /// State that is needed to track reachability of nodes given a query.
     ReachabilityEngineState *reachabilityEngineState = nullptr;
 
     /// The number of individual packet variables that have been created in this state.
@@ -169,7 +169,7 @@ class ExecutionState : public AbstractExecutionState {
     /// Checks whether the node has been visited in this state.
     void markVisited(const IR::Node *node);
 
-    /// @returns list of all statements visited before reaching this state.
+    /// @returns list of all nodes visited before reaching this state.
     [[nodiscard]] const P4::Coverage::CoverageSet &getVisited() const;
 
     /// Sets the symbolic value of the given state variable to the given value. Constant folding
diff --git a/backends/p4tools/modules/testgen/lib/final_state.h b/backends/p4tools/modules/testgen/lib/final_state.h
index ee0dade573..ca939936d9 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.h
+++ b/backends/p4tools/modules/testgen/lib/final_state.h
@@ -71,7 +71,7 @@ class FinalState {
     /// @returns the computed traces of this final state.
     [[nodiscard]] const std::vector<std::reference_wrapper<const TraceEvent>> *getTraces() const;
 
-    /// @returns the list of visited statements of this state.
+    /// @returns the list of visited nodes of this state.
     [[nodiscard]] const P4::Coverage::CoverageSet &getVisited() const;
 };
 
diff --git a/backends/p4tools/modules/testgen/lib/logging.h b/backends/p4tools/modules/testgen/lib/logging.h
index 1e0d04ad48..43ba6a7515 100644
--- a/backends/p4tools/modules/testgen/lib/logging.h
+++ b/backends/p4tools/modules/testgen/lib/logging.h
@@ -16,7 +16,7 @@ void printTraces(const std::string &fmt, Arguments &&...args) {
 }
 
 /// Helper functions that prints strings associated with basic test generation information., for
-/// example the covered statements or tests number.
+/// example the covered nodes or tests number.
 template <typename... Arguments>
 void printInfo(const std::string &fmt, Arguments &&...args) {
     printFeature("test_info", 4, fmt, std::forward<Arguments>(args)...);
@@ -26,7 +26,7 @@ void printInfo(const std::string &fmt, Arguments &&...args) {
 void enableTraceLogging();
 
 /// Enable the printing of basic test case generation information, for example the covered
-/// statements or test number.
+/// nodes or test number.
 void enableInformationLogging();
 
 /// Enable printing of the individual program node steps of the interpreter.
diff --git a/backends/p4tools/modules/testgen/lib/test_backend.cpp b/backends/p4tools/modules/testgen/lib/test_backend.cpp
index 010cb010d7..4304819d35 100644
--- a/backends/p4tools/modules/testgen/lib/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/lib/test_backend.cpp
@@ -110,7 +110,7 @@ bool TestBackEnd::run(const FinalState &state) {
         }
         const auto *testSpec = createTestSpec(executionState, &finalModel, testInfo);
 
-        // Commit an update to the visited statements.
+        // Commit an update to the visited nodes.
         // Only do this once we are sure we are generating a test.
         symbex.updateVisitedNodes(replacedState.getVisited());
         const P4::Coverage::CoverageSet &visitedNodes = symbex.getVisitedNodes();
diff --git a/backends/p4tools/modules/testgen/options.cpp b/backends/p4tools/modules/testgen/options.cpp
index 26108cc863..de7ff443e9 100644
--- a/backends/p4tools/modules/testgen/options.cpp
+++ b/backends/p4tools/modules/testgen/options.cpp
@@ -188,7 +188,7 @@ TestgenOptions::TestgenOptions()
             }
             return true;
         },
-        "List of the selected branches which should be chosen for selection.");
+        "[EXPERIMENTAL] List of the selected branches which should be chosen for selection.");
 
     registerOption(
         "--track-branches", nullptr,
@@ -203,8 +203,8 @@ TestgenOptions::TestgenOptions()
             }
             return true;
         },
-        "Track the branches that are chosen in the symbolic executor. This can be used for "
-        "deterministic replay.");
+        "[EXPERIMENTAL] Track the branches that are chosen in the symbolic executor. This can be "
+        "used for deterministic replay.");
 
     registerOption(
         "--with-output-packet", nullptr,
@@ -229,7 +229,6 @@ TestgenOptions::TestgenOptions()
                 {"DEPTH_FIRST", PathSelectionPolicy::DepthFirst},
                 {"RANDOM_BACKTRACK", PathSelectionPolicy::RandomBacktrack},
                 {"GREEDY_STATEMENT_SEARCH", PathSelectionPolicy::GreedyStmtCoverage},
-                {"RANDOM_STATEMENT_SEARCH", PathSelectionPolicy::RandomMaxStmtCoverage},
             };
             auto selectionString = cstring(arg).toUpper();
             auto it = PATH_SELECTION_OPTIONS.find(selectionString);
@@ -250,7 +249,7 @@ TestgenOptions::TestgenOptions()
             return false;
         },
         "Selects a specific path selection strategy for test generation. Options are: "
-        "DEPTH_FIRST, RANDOM_BACKTRACK, GREEDY_STATEMENT_SEARCH, and RANDOM_STATEMENT_SEARCH. "
+        "DEPTH_FIRST, RANDOM_BACKTRACK, and GREEDY_STATEMENT_SEARCH. "
         "Defaults to DEPTH_FIRST.");
 
     registerOption(
@@ -283,29 +282,6 @@ TestgenOptions::TestgenOptions()
         "options are possible: Currently supported: STATEMENTS, TABLE_ENTRIES "
         "Defaults to no coverage.");
 
-    registerOption(
-        "--saddle-point", "saddlePoint",
-        [this](const char *arg) {
-            int64_t saddlePointTmp = 0;
-            try {
-                // Unfortunately, we can not use std::stoul because negative inputs are okay
-                // according to the C++ standard.
-                saddlePointTmp = std::stoll(arg);
-                if (saddlePointTmp <= 1) {
-                    throw std::invalid_argument("Invalid input.");
-                }
-            } catch (std::invalid_argument &) {
-                ::error(
-                    "Invalid input value %1% for --saddle-point. Expected an integer greater than "
-                    "1.",
-                    arg);
-                return false;
-            }
-            saddlePoint = saddlePointTmp;
-            return true;
-        },
-        "Threshold to invoke multiPop on RANDOM_STATEMENT_SEARCH.");
-
     registerOption(
         "--print-traces", nullptr,
         [](const char *) {
@@ -346,8 +322,8 @@ TestgenOptions::TestgenOptions()
             dcg = true;
             return true;
         },
-        R"(Build a DCG for input graph. This control flow graph directed cyclic graph can be used
-        for statement reachability analysis.)");
+        "[EXPERIMENTAL] Build a DCG for input graph. This control flow graph directed cyclic graph "
+        "can be used for statement reachability analysis.");
 
     registerOption(
         "--pattern", "pattern",
diff --git a/backends/p4tools/modules/testgen/options.h b/backends/p4tools/modules/testgen/options.h
index 61232c3de4..bcd0c04257 100644
--- a/backends/p4tools/modules/testgen/options.h
+++ b/backends/p4tools/modules/testgen/options.h
@@ -31,12 +31,6 @@ class TestgenOptions : public AbstractP4cToolOptions {
     // listed in @var SUPPORTED_STOP_METRICS.
     cstring stopMetric;
 
-    /// To be used with randomAccessMaxCoverage. It specifies after how many
-    /// tests (saddle point) we should randomly explore the program and pick
-    /// a random branch ranked by how many unique non-visited statements it
-    /// has.
-    uint64_t saddlePoint = 5;
-
     /// @returns the singleton instance of this class.
     static TestgenOptions &get();
 
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp
index b84ac24861..e307e8c20d 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp
@@ -84,8 +84,8 @@ std::string Metadata::getTestCaseTemplate() {
 seed: {{ default(seed, "none") }}
 # Test timestamp.
 data: {{timestamp}}
-# Percentage of statements covered at the time of this test.
-statement_coverage: {{coverage}}
+# Percentage of nodes covered at the time of this test.
+node_coverage: {{coverage}}
 
 # Trace associated with this test.
 #
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp
index 5d66663657..6cc9a5ab30 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp
@@ -260,7 +260,7 @@ metadata: "Date generated: {{timestamp}}"
 ## if length(selected_branches) > 0
 metadata: "{{selected_branches}}"
 ## endif
-metadata: "Current statement coverage: {{coverage}}"
+metadata: "Current node coverage: {{coverage}}"
 
 ## for trace_item in trace
 traces: "{{trace_item}}"
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.cpp
index 3beda4fd96..70364a38a0 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.cpp
@@ -329,7 +329,7 @@ class Test{{test_id}}(AbstractTest):
     # {{selected_branches}}
 ## endif
     '''
-    # Current statement coverage: {{coverage}}
+    # Current node coverage: {{coverage}}
 ## for trace_item in trace
     {{trace_item}}
 ##endfor
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp
index 97b9f3d979..85794db9ee 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp
@@ -216,7 +216,7 @@ std::string STF::getTestCaseTemplate() {
 ## if length(selected_branches) > 0
     # {{selected_branches}}
 ## endif
-# Current statement coverage: {{coverage}}
+# Current node coverage: {{coverage}}
 # Traces
 ## for trace_item in trace
 # {{trace_item}}
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
index 50166cb5b0..af7438fe39 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
@@ -163,7 +163,7 @@ void Bmv2V1ModelTableStepper::evalTableActionProfile(
         replacements.emplace_back(
             new IR::MethodCallStatement(Util::SourceInfo(), synthesizedAction));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(*state);
@@ -257,7 +257,7 @@ void Bmv2V1ModelTableStepper::evalTableActionSelector(
         replacements.emplace_back(
             new IR::MethodCallStatement(Util::SourceInfo(), synthesizedAction));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(*state);
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp b/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp
index 091ab42cf9..23cf5aea1e 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp
@@ -199,7 +199,7 @@ std::string STF::getTestCaseTemplate() {
 ## if length(selected_branches) > 0
     # {{selected_branches}}
 ## endif
-# Current statement coverage: {{coverage}}
+# Current node coverage: {{coverage}}
 # Traces
 ## for trace_item in trace
 # {{trace_item}}
diff --git a/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp b/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp
index 58a4a922f5..841569a1b2 100644
--- a/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp
@@ -84,8 +84,8 @@ std::string Metadata::getTestCaseTemplate() {
 seed: {{ default(seed, "none") }}
 # Test timestamp.
 data: {{timestamp}}
-# Percentage of statements covered at the time of this test.
-statement_coverage: {{coverage}}
+# Percentage of nodes covered at the time of this test.
+node_coverage: {{coverage}}
 
 # Trace associated with this test.
 #
diff --git a/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp b/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
index 5fa128959b..2505e113b8 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
@@ -154,7 +154,7 @@ void SharedPnaTableStepper::evalTableActionProfile(
         replacements.emplace_back(
             new IR::MethodCallStatement(Util::SourceInfo(), synthesizedAction));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(*state);
@@ -248,7 +248,7 @@ void SharedPnaTableStepper::evalTableActionSelector(
         replacements.emplace_back(
             new IR::MethodCallStatement(Util::SourceInfo(), synthesizedAction));
         // Some path selection strategies depend on looking ahead and collecting potential
-        // statements. If that is the case, apply the CoverableNodesScanner visitor.
+        // nodes. If that is the case, apply the CoverableNodesScanner visitor.
         P4::Coverage::CoverageSet coveredNodes;
         if (requiresLookahead(TestgenOptions::get().pathSelectionPolicy)) {
             auto collector = CoverableNodesScanner(*state);
diff --git a/backends/p4tools/modules/testgen/testgen.cpp b/backends/p4tools/modules/testgen/testgen.cpp
index 3d9d15b97c..6154e50d07 100644
--- a/backends/p4tools/modules/testgen/testgen.cpp
+++ b/backends/p4tools/modules/testgen/testgen.cpp
@@ -16,8 +16,7 @@
 
 #include "backends/p4tools/modules/testgen/core/program_info.h"
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/depth_first.h"
-#include "backends/p4tools/modules/testgen/core/symbolic_executor/greedy_stmt_cov.h"
-#include "backends/p4tools/modules/testgen/core/symbolic_executor/max_stmt_cov.h"
+#include "backends/p4tools/modules/testgen/core/symbolic_executor/greedy_node_cov.h"
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h"
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/random_backtrack.h"
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/selected_branches.h"
@@ -40,14 +39,11 @@ SymbolicExecutor *pickExecutionEngine(const TestgenOptions &testgenOptions,
                                       const ProgramInfo *programInfo, AbstractSolver &solver) {
     const auto &pathSelectionPolicy = testgenOptions.pathSelectionPolicy;
     if (pathSelectionPolicy == PathSelectionPolicy::GreedyStmtCoverage) {
-        return new GreedyStmtSelection(solver, *programInfo);
+        return new GreedyNodeSelection(solver, *programInfo);
     }
     if (pathSelectionPolicy == PathSelectionPolicy::RandomBacktrack) {
         return new RandomBacktrack(solver, *programInfo);
     }
-    if (pathSelectionPolicy == PathSelectionPolicy::RandomMaxStmtCoverage) {
-        return new RandomMaxStmtCoverage(solver, *programInfo, testgenOptions.saddlePoint);
-    }
     if (!testgenOptions.selectedBranches.empty()) {
         std::string selectedBranchesStr = testgenOptions.selectedBranches;
         return new SelectedBranches(solver, *programInfo, selectedBranchesStr);