From ca2e3832105b464dbcd4cce53fa49e2418e4fec7 Mon Sep 17 00:00:00 2001
From: fruffy-bfn <fabian.ruffy@intel.com>
Date: Fri, 9 Jun 2023 22:33:25 +0200
Subject: [PATCH] [P4Testgen] Remove complete from the model, make it part of
 the evaluation step instead.  (#4015)

* Remove complete from the model.

* Execution state refactoring.

* Remove createSymbolicVariable entirely and replace it with the static getSymbolicVariable.

---------

Co-authored-by: fruffy <fruffy@nyu.edu>
---
 backends/p4tools/common/lib/model.cpp         | 65 ++++++-----------
 backends/p4tools/common/lib/model.h           | 45 ++++--------
 backends/p4tools/common/lib/symbolic_env.cpp  | 10 +--
 backends/p4tools/common/lib/symbolic_env.h    |  3 -
 backends/p4tools/common/lib/taint.cpp         |  4 +-
 backends/p4tools/common/lib/taint.h           |  2 +-
 backends/p4tools/common/lib/trace_event.cpp   |  6 +-
 backends/p4tools/common/lib/trace_event.h     |  5 +-
 .../p4tools/common/lib/trace_event_types.cpp  | 39 +++-------
 .../p4tools/common/lib/trace_event_types.h    | 18 ++---
 backends/p4tools/common/lib/variables.cpp     |  6 +-
 backends/p4tools/common/lib/variables.h       |  3 +-
 .../core/small_step/abstract_stepper.cpp      |  3 +-
 .../testgen/core/small_step/table_stepper.cpp | 32 +++++----
 .../testgen/core/small_step/table_stepper.h   |  6 +-
 .../p4tools/modules/testgen/lib/concolic.cpp  | 14 ++--
 .../p4tools/modules/testgen/lib/concolic.h    | 12 ++--
 .../modules/testgen/lib/execution_state.cpp   | 71 ++++++++++---------
 .../modules/testgen/lib/execution_state.h     | 55 +++++++-------
 .../modules/testgen/lib/final_state.cpp       | 18 ++---
 .../modules/testgen/lib/test_backend.cpp      | 12 ++--
 .../p4tools/modules/testgen/lib/test_object.h |  2 +-
 .../p4tools/modules/testgen/lib/test_spec.cpp | 42 +++++------
 .../p4tools/modules/testgen/lib/test_spec.h   | 16 ++---
 .../testgen/targets/bmv2/cmd_stepper.cpp      |  3 +-
 .../modules/testgen/targets/bmv2/concolic.cpp |  9 +--
 .../testgen/targets/bmv2/expr_stepper.cpp     |  6 +-
 .../targets/bmv2/p4_asserts_parser.cpp        |  5 +-
 .../targets/bmv2/p4_refers_to_parser.cpp      |  4 +-
 .../testgen/targets/bmv2/table_stepper.cpp    | 35 ++++-----
 .../testgen/targets/bmv2/table_stepper.h      |  3 +-
 .../testgen/targets/bmv2/test_backend.cpp     | 19 +++--
 .../testgen/targets/bmv2/test_spec.cpp        | 52 ++++++++------
 .../modules/testgen/targets/bmv2/test_spec.h  | 28 +++++---
 .../testgen/targets/ebpf/table_stepper.cpp    |  7 --
 .../testgen/targets/ebpf/table_stepper.h      |  5 --
 .../testgen/targets/ebpf/test/P4Tests.cmake   |  1 -
 .../testgen/targets/ebpf/test_backend.cpp     |  9 ++-
 .../targets/pna/dpdk/table_stepper.cpp        |  8 ---
 .../testgen/targets/pna/dpdk/table_stepper.h  |  6 --
 .../targets/pna/shared_table_stepper.cpp      | 35 ++++-----
 .../targets/pna/shared_table_stepper.h        |  3 +-
 .../testgen/targets/pna/test_backend.cpp      | 15 ++--
 .../modules/testgen/targets/pna/test_spec.cpp | 43 ++++++-----
 .../modules/testgen/targets/pna/test_spec.h   | 19 +++--
 .../modules/testgen/test/gtest_utils.cpp      |  2 +-
 .../small-step/p4_asserts_parser_test.cpp     | 22 +++---
 .../modules/testgen/test/small-step/util.h    |  6 +-
 48 files changed, 377 insertions(+), 457 deletions(-)

diff --git a/backends/p4tools/common/lib/model.cpp b/backends/p4tools/common/lib/model.cpp
index 18de05ff1a..01ba8d17f6 100644
--- a/backends/p4tools/common/lib/model.cpp
+++ b/backends/p4tools/common/lib/model.cpp
@@ -16,65 +16,40 @@
 
 namespace P4Tools {
 
-Model::SubstVisitor::SubstVisitor(const Model &model) : self(model) {}
+Model::SubstVisitor::SubstVisitor(const Model &model, bool doComplete)
+    : self(model), doComplete(doComplete) {}
 
 const IR::Literal *Model::SubstVisitor::preorder(IR::StateVariable *var) {
     BUG("At this point all state variables should have been resolved. Encountered %1%.", var);
 }
 
 const IR::Literal *Model::SubstVisitor::preorder(IR::SymbolicVariable *var) {
-    BUG_CHECK(self.symbolicMap.find(var) != self.symbolicMap.end(),
-              "Variable not bound in model: %1%", var);
+    auto varIt = self.symbolicMap.find(var);
+    if (varIt == self.symbolicMap.end()) {
+        if (doComplete) {
+            return IR::getDefaultValue(var->type, var->srcInfo, true)->checkedTo<IR::Literal>();
+        }
+        BUG("Variable not bound in model: %1%", var);
+    }
     prune();
-    return self.symbolicMap.at(var)->checkedTo<IR::Literal>();
+    return varIt->second->checkedTo<IR::Literal>();
 }
 
 const IR::Literal *Model::SubstVisitor::preorder(IR::TaintExpression *var) {
     return IR::getDefaultValue(var->type, var->getSourceInfo())->checkedTo<IR::Literal>();
 }
 
-Model::CompleteVisitor::CompleteVisitor(Model &model) : self(model) {}
-
-bool Model::CompleteVisitor::preorder(const IR::SymbolicVariable *var) {
-    if (self.symbolicMap.find(var) == self.symbolicMap.end()) {
-        LOG_FEATURE("common", 5,
-                    "***** Did not find a binding for " << var << ". Autocompleting." << std::endl);
-        const auto *type = var->type;
-        self.symbolicMap.emplace(var, IR::getDefaultValue(type, var->getSourceInfo()));
-    }
-    return false;
-}
-
-bool Model::CompleteVisitor::preorder(const IR::StateVariable *var) {
-    BUG("At this point all state variables should have been resolved. Encountered %1%.", var);
-}
-
-void Model::complete(const IR::Expression *expr) { expr->apply(CompleteVisitor(*this)); }
-
-void Model::complete(const SymbolicSet &inputSet) {
-    auto completionVisitor = CompleteVisitor(*this);
-    for (const auto &var : inputSet) {
-        var->apply(completionVisitor);
-    }
-}
-
-void Model::complete(const SymbolicMapType &inputMap) {
-    for (const auto &inputTuple : inputMap) {
-        const auto *expr = inputTuple.second;
-        expr->apply(CompleteVisitor(*this));
-    }
-}
-
 const IR::StructExpression *Model::evaluateStructExpr(const IR::StructExpression *structExpr,
+                                                      bool doComplete,
                                                       ExpressionMap *resolvedExpressions) const {
     auto *resolvedStructExpr =
         new IR::StructExpression(structExpr->srcInfo, structExpr->type, structExpr->structType, {});
     for (const auto *namedExpr : structExpr->components) {
         const IR::Expression *resolvedExpr = nullptr;
         if (const auto *subStructExpr = namedExpr->expression->to<IR::StructExpression>()) {
-            resolvedExpr = evaluateStructExpr(subStructExpr, resolvedExpressions);
+            resolvedExpr = evaluateStructExpr(subStructExpr, doComplete, resolvedExpressions);
         } else {
-            resolvedExpr = evaluate(namedExpr->expression, resolvedExpressions);
+            resolvedExpr = evaluate(namedExpr->expression, doComplete, resolvedExpressions);
         }
         resolvedStructExpr->components.push_back(
             new IR::NamedExpression(namedExpr->srcInfo, namedExpr->name, resolvedExpr));
@@ -83,23 +58,24 @@ const IR::StructExpression *Model::evaluateStructExpr(const IR::StructExpression
 }
 
 const IR::ListExpression *Model::evaluateListExpr(const IR::ListExpression *listExpr,
+                                                  bool doComplete,
                                                   ExpressionMap *resolvedExpressions) const {
     auto *resolvedListExpr = new IR::ListExpression(listExpr->srcInfo, listExpr->type, {});
     for (const auto *expr : listExpr->components) {
         const IR::Expression *resolvedExpr = nullptr;
         if (const auto *subStructExpr = expr->to<IR::ListExpression>()) {
-            resolvedExpr = evaluateListExpr(subStructExpr, resolvedExpressions);
+            resolvedExpr = evaluateListExpr(subStructExpr, doComplete, resolvedExpressions);
         } else {
-            resolvedExpr = evaluate(expr, resolvedExpressions);
+            resolvedExpr = evaluate(expr, doComplete, resolvedExpressions);
         }
         resolvedListExpr->components.push_back(resolvedExpr);
     }
     return resolvedListExpr;
 }
 
-const IR::Literal *Model::evaluate(const IR::Expression *expr,
+const IR::Literal *Model::evaluate(const IR::Expression *expr, bool doComplete,
                                    ExpressionMap *resolvedExpressions) const {
-    const auto *substituted = expr->apply(SubstVisitor(*this));
+    const auto *substituted = expr->apply(SubstVisitor(*this, doComplete));
     const auto *evaluated = P4::optimizeExpression(substituted);
     const auto *literal = evaluated->checkedTo<IR::Literal>();
     // Add the variable to the resolvedExpressions list, if the list is not null.
@@ -109,12 +85,13 @@ const IR::Literal *Model::evaluate(const IR::Expression *expr,
     return literal;
 }
 
-Model *Model::evaluate(const SymbolicMapType &inputMap, ExpressionMap *resolvedExpressions) const {
+Model *Model::evaluate(const SymbolicMapType &inputMap, bool doComplete,
+                       ExpressionMap *resolvedExpressions) const {
     auto *result = new Model(*this);
     for (const auto &inputTuple : inputMap) {
         const auto &name = inputTuple.first;
         const auto *expr = inputTuple.second;
-        (*result)[name] = evaluate(expr, resolvedExpressions);
+        (*result)[name] = evaluate(expr, doComplete, resolvedExpressions);
     }
     return result;
 }
diff --git a/backends/p4tools/common/lib/model.h b/backends/p4tools/common/lib/model.h
index 79eadf03ee..de75585b4e 100644
--- a/backends/p4tools/common/lib/model.h
+++ b/backends/p4tools/common/lib/model.h
@@ -31,24 +31,17 @@ class Model : public SymbolicMapType {
     class SubstVisitor : public Transform {
         const Model &self;
 
+        /// If doComplete is true, the visitor will not throw an error if a variable does not have a
+        /// substitution and instead assign a random or zero value (depending on whether there is a
+        /// seed) to the variable..
+        bool doComplete;
+
      public:
         const IR::Literal *preorder(IR::StateVariable *var) override;
         const IR::Literal *preorder(IR::SymbolicVariable *var) override;
         const IR::Literal *preorder(IR::TaintExpression *var) override;
 
-        explicit SubstVisitor(const Model &model);
-    };
-
-    // @see SubstVisitor. Does not fail if a variable is not part of the model.
-    /// Instead, it completes the variable and adds it to the symbolic map.
-    class CompleteVisitor : public Inspector {
-        Model &self;
-
-     public:
-        bool preorder(const IR::SymbolicVariable *var) override;
-        bool preorder(const IR::StateVariable *var) override;
-
-        explicit CompleteVisitor(Model &model);
+        explicit SubstVisitor(const Model &model, bool doComplete);
     };
 
  public:
@@ -64,37 +57,23 @@ class Model : public SymbolicMapType {
     Model &operator=(Model &&) = default;
     ~Model() = default;
 
-    /// Completes the model with the variables in the given expression. A variable needs to be
-    /// completed if it is not present in the model computed by the solver that produced the
-    /// model. This typically happens when a variable is not needed to solve a set of
-    /// constraints.
-    void complete(const IR::Expression *expr);
-
-    /// Completes the model with the variables in the given list of expressions. A variable needs to
-    /// be completed if it is not present in the model computed by the solver that produced the
-    /// model. This typically happens when a variable is not needed to solve a set of constraints.
-    void complete(const SymbolicMapType &inputMap);
-
-    /// Adds the given set of variables to the model (if they do not exist already).
-    /// If the variable does not exist, it is initialized to a default value.
-    void complete(const SymbolicSet &inputSet);
-
     /// Evaluates a P4 expression in the context of this model.
     ///
     /// A BUG occurs if the given expression refers to a variable that is not bound by this model.
     /// If the input list @param resolvedExpressions is not null, we also collect the resolved value
     /// of this expression.
-    const IR::Literal *evaluate(const IR::Expression *expr,
+    const IR::Literal *evaluate(const IR::Expression *expr, bool doComplete,
                                 ExpressionMap *resolvedExpressions = nullptr) const;
 
     // Evaluates a P4 StructExpression in the context of this model. Recursively calls into
     // @evaluate and substitutes all members of this list with a Value type.
     const IR::StructExpression *evaluateStructExpr(const IR::StructExpression *structExpr,
+                                                   bool doComplete,
                                                    ExpressionMap *resolvedExpressions) const;
 
     // Evaluates a P4 ListExpression in the context of this model. Recursively calls into @evaluate
     // and substitutes all members of this list with a Value type.
-    const IR::ListExpression *evaluateListExpr(const IR::ListExpression *listExpr,
+    const IR::ListExpression *evaluateListExpr(const IR::ListExpression *listExpr, bool doComplete,
                                                ExpressionMap *resolvedExpressions) const;
 
     /// Evaluates a collection of P4 expressions in the context of this model by calling @evaluate
@@ -106,11 +85,11 @@ class Model : public SymbolicMapType {
     /// of all the variables we have resolved within this expression.
     template <template <class...> class Collection>
     std::vector<const IR::Literal *> evaluateAll(
-        const Collection<const IR::Expression *> *exprs,
+        const Collection<const IR::Expression *> *exprs, bool doComplete,
         ExpressionMap *resolvedExpressions = nullptr) const {
         std::vector<const IR::Literal *> result(exprs->size());
         for (const auto *expr : *exprs) {
-            result.push_back(evaluate(expr, resolvedExpressions));
+            result.push_back(evaluate(expr, doComplete, resolvedExpressions));
         }
         return result;
     }
@@ -121,7 +100,7 @@ class Model : public SymbolicMapType {
     /// variable that is not bound by this model. If the input list @param resolvedExpressions is
     /// not null, we also collect the bound values of all the variables we have resolved within this
     /// expression.
-    Model *evaluate(const SymbolicMapType &inputMap,
+    Model *evaluate(const SymbolicMapType &inputMap, bool doComplete,
                     ExpressionMap *resolvedExpressions = nullptr) const;
 
     /// Tries to retrieve @param var from the model.
diff --git a/backends/p4tools/common/lib/symbolic_env.cpp b/backends/p4tools/common/lib/symbolic_env.cpp
index d7ee83f8fb..6646054f5a 100644
--- a/backends/p4tools/common/lib/symbolic_env.cpp
+++ b/backends/p4tools/common/lib/symbolic_env.cpp
@@ -31,17 +31,9 @@ void SymbolicEnv::set(const IR::StateVariable &var, const IR::Expression *value)
     map[var] = P4::optimizeExpression(value);
 }
 
-Model *SymbolicEnv::complete(const Model &model) const {
-    // Produce a new model based on the input model
-    // Add the variables contained in this environment and try to complete them.
-    auto *newModel = new Model(model);
-    newModel->complete(map);
-    return newModel;
-}
-
 Model *SymbolicEnv::evaluate(const Model &model) const {
     // Produce a new model based on the input model
-    return model.evaluate(map);
+    return model.evaluate(map, true);
 }
 
 const IR::Expression *SymbolicEnv::subst(const IR::Expression *expr) const {
diff --git a/backends/p4tools/common/lib/symbolic_env.h b/backends/p4tools/common/lib/symbolic_env.h
index 8d9b6e66bc..5c1f434008 100644
--- a/backends/p4tools/common/lib/symbolic_env.h
+++ b/backends/p4tools/common/lib/symbolic_env.h
@@ -26,9 +26,6 @@ class SymbolicEnv {
     /// done on the given value before updating the symbolic state.
     void set(const IR::StateVariable &var, const IR::Expression *value);
 
-    /// Completes the model with all variables referenced in the symbolic environment.
-    [[nodiscard]] Model *complete(const Model &model) const;
-
     /// Evaluates this symbolic environment in the context of the given model.
     ///
     /// A BUG occurs if any symbolic value in this environment refers to a variable that is not
diff --git a/backends/p4tools/common/lib/taint.cpp b/backends/p4tools/common/lib/taint.cpp
index 7fa7cbe81d..03c176aff6 100644
--- a/backends/p4tools/common/lib/taint.cpp
+++ b/backends/p4tools/common/lib/taint.cpp
@@ -274,14 +274,14 @@ class MaskBuilder : public Transform {
     MaskBuilder() { visitDagOnce = false; }
 };
 
-const IR::Literal *Taint::buildTaintMask(const SymbolicMapType &varMap, const Model *completedModel,
+const IR::Literal *Taint::buildTaintMask(const SymbolicMapType &varMap, const Model *evaluatedModel,
                                          const IR::Expression *programPacket) {
     // First propagate taint and simplify the packet.
     const auto *taintedPacket = programPacket->apply(TaintPropagator(varMap));
     // Then create the mask based on the remaining expressions.
     const auto *mask = taintedPacket->apply(MaskBuilder());
     // Produce the evaluated literal. The hex expression should only have 0 or f.
-    return completedModel->evaluate(mask);
+    return evaluatedModel->evaluate(mask, false);
 }
 
 const IR::Expression *Taint::propagateTaint(const SymbolicMapType &varMap,
diff --git a/backends/p4tools/common/lib/taint.h b/backends/p4tools/common/lib/taint.h
index d763d0bdd9..db9f82afb2 100644
--- a/backends/p4tools/common/lib/taint.h
+++ b/backends/p4tools/common/lib/taint.h
@@ -24,7 +24,7 @@ class Taint {
     /// @returns the mask for the corresponding program packet, indicating bits of the expression
     /// which are not tainted.
     static const IR::Literal *buildTaintMask(const SymbolicMapType &varMap,
-                                             const Model *completedModel,
+                                             const Model *evaluatedModel,
                                              const IR::Expression *programPacket);
 };
 
diff --git a/backends/p4tools/common/lib/trace_event.cpp b/backends/p4tools/common/lib/trace_event.cpp
index 00e0d036e0..d36baba023 100644
--- a/backends/p4tools/common/lib/trace_event.cpp
+++ b/backends/p4tools/common/lib/trace_event.cpp
@@ -11,10 +11,10 @@ TraceEvent::TraceEvent() = default;
 
 const TraceEvent *TraceEvent::subst(const SymbolicEnv & /*env*/) const { return this; }
 
-void TraceEvent::complete(Model * /*model*/) const {}
-
 const TraceEvent *TraceEvent::apply(Transform & /*visitor*/) const { return this; }
 
-const TraceEvent *TraceEvent::evaluate(const Model & /*model*/) const { return this; }
+const TraceEvent *TraceEvent::evaluate(const Model & /*model*/, bool /*doComplete*/) const {
+    return this;
+}
 
 }  // namespace P4Tools
diff --git a/backends/p4tools/common/lib/trace_event.h b/backends/p4tools/common/lib/trace_event.h
index 742bd9021a..c44eed1743 100644
--- a/backends/p4tools/common/lib/trace_event.h
+++ b/backends/p4tools/common/lib/trace_event.h
@@ -27,12 +27,9 @@ class TraceEvent : public ICastable {
     /// Applies the given IR transform to the expressions in this trace event.
     virtual const TraceEvent *apply(Transform &visitor) const;
 
-    /// Completes a model with the variables used in this trace event.
-    virtual void complete(Model *model) const;
-
     /// Evaluates expressions in the body of this trace event for their concrete value in the given
     /// model. A BUG occurs if there are any variables that are unbound by the given model.
-    [[nodiscard]] virtual const TraceEvent *evaluate(const Model &model) const;
+    [[nodiscard]] virtual const TraceEvent *evaluate(const Model &model, bool doComplete) const;
 
  protected:
     /// Prints this trace event to the given ostream.
diff --git a/backends/p4tools/common/lib/trace_event_types.cpp b/backends/p4tools/common/lib/trace_event_types.cpp
index 910469ab03..7fed3207aa 100644
--- a/backends/p4tools/common/lib/trace_event_types.cpp
+++ b/backends/p4tools/common/lib/trace_event_types.cpp
@@ -38,13 +38,11 @@ const Expression *Expression::apply(Transform &visitor) const {
     return new Expression(value->apply(visitor), label);
 }
 
-void Expression::complete(Model *model) const { model->complete(value); }
-
-const Expression *Expression::evaluate(const Model &model) const {
+const Expression *Expression::evaluate(const Model &model, bool doComplete) const {
     if (Taint::hasTaint(model, value)) {
         return new Expression(&Taint::TAINTED_STRING_LITERAL, label);
     }
-    return new Expression(model.evaluate(value), label);
+    return new Expression(model.evaluate(value, doComplete), label);
 }
 
 void Expression::print(std::ostream &os) const {
@@ -72,14 +70,13 @@ const IfStatementCondition *IfStatementCondition::apply(Transform &visitor) cons
     return traceEvent;
 }
 
-void IfStatementCondition::complete(Model *model) const { model->complete(postEvalCond); }
-
-const IfStatementCondition *IfStatementCondition::evaluate(const Model &model) const {
+const IfStatementCondition *IfStatementCondition::evaluate(const Model &model,
+                                                           bool doComplete) const {
     const IR::Literal *evaluatedPostVal = nullptr;
     if (Taint::hasTaint(model, postEvalCond)) {
         evaluatedPostVal = &Taint::TAINTED_STRING_LITERAL;
     } else {
-        evaluatedPostVal = model.evaluate(postEvalCond);
+        evaluatedPostVal = model.evaluate(postEvalCond, doComplete);
     }
     auto *traceEvent = new IfStatementCondition(evaluatedPostVal);
     traceEvent->setPreEvalCond(postEvalCond);
@@ -133,20 +130,14 @@ const ExtractSuccess *ExtractSuccess::apply(Transform &visitor) const {
     return new ExtractSuccess(extractedHeader, offset, condition, applyFields);
 }
 
-void ExtractSuccess::complete(Model *model) const {
-    for (const auto &field : fields) {
-        model->complete(field.second);
-    }
-}
-
-const ExtractSuccess *ExtractSuccess::evaluate(const Model &model) const {
+const ExtractSuccess *ExtractSuccess::evaluate(const Model &model, bool doComplete) const {
     std::vector<std::pair<IR::StateVariable, const IR::Expression *>> applyFields;
     applyFields.reserve(fields.size());
     for (const auto &field : fields) {
         if (Taint::hasTaint(model, field.second)) {
             applyFields.emplace_back(field.first, &Taint::TAINTED_STRING_LITERAL);
         } else {
-            applyFields.emplace_back(field.first, model.evaluate(field.second));
+            applyFields.emplace_back(field.first, model.evaluate(field.second, doComplete));
         }
     }
     return new ExtractSuccess(extractedHeader, offset, condition, applyFields);
@@ -210,20 +201,14 @@ const Emit *Emit::apply(Transform &visitor) const {
     return new Emit(emitHeader, applyFields);
 }
 
-void Emit::complete(Model *model) const {
-    for (const auto &field : fields) {
-        model->complete(field.second);
-    }
-}
-
-const Emit *Emit::evaluate(const Model &model) const {
+const Emit *Emit::evaluate(const Model &model, bool doComplete) const {
     std::vector<std::pair<IR::StateVariable, const IR::Expression *>> applyFields;
     applyFields.reserve(fields.size());
     for (const auto &field : fields) {
         if (Taint::hasTaint(model, field.second)) {
             applyFields.emplace_back(field.first, &Taint::TAINTED_STRING_LITERAL);
         } else {
-            applyFields.emplace_back(field.first, model.evaluate(field.second));
+            applyFields.emplace_back(field.first, model.evaluate(field.second, doComplete));
         }
     }
     return new Emit(emitHeader, applyFields);
@@ -254,13 +239,11 @@ const Packet *Packet::apply(Transform &visitor) const {
     return new Packet(direction, packetValue->apply(visitor));
 }
 
-void Packet::complete(Model *model) const { model->complete(packetValue); }
-
-const Packet *Packet::evaluate(const Model &model) const {
+const Packet *Packet::evaluate(const Model &model, bool doComplete) const {
     if (Taint::hasTaint(model, packetValue)) {
         return new Packet(direction, &Taint::TAINTED_STRING_LITERAL);
     }
-    return new Packet(direction, model.evaluate(packetValue));
+    return new Packet(direction, model.evaluate(packetValue, doComplete));
 }
 
 void Packet::print(std::ostream &os) const {
diff --git a/backends/p4tools/common/lib/trace_event_types.h b/backends/p4tools/common/lib/trace_event_types.h
index 6b3ad62d76..10fe545e38 100644
--- a/backends/p4tools/common/lib/trace_event_types.h
+++ b/backends/p4tools/common/lib/trace_event_types.h
@@ -47,8 +47,7 @@ class Expression : public Generic {
  public:
     [[nodiscard]] const Expression *subst(const SymbolicEnv &env) const override;
     const Expression *apply(Transform &visitor) const override;
-    void complete(Model *model) const override;
-    [[nodiscard]] const Expression *evaluate(const Model &model) const override;
+    [[nodiscard]] const Expression *evaluate(const Model &model, bool doComplete) const override;
 
     explicit Expression(const IR::Expression *value, cstring label);
     ~Expression() override = default;
@@ -76,8 +75,8 @@ class IfStatementCondition : public TraceEvent {
  public:
     [[nodiscard]] const IfStatementCondition *subst(const SymbolicEnv &env) const override;
     const IfStatementCondition *apply(Transform &visitor) const override;
-    void complete(Model *model) const override;
-    [[nodiscard]] const IfStatementCondition *evaluate(const Model &model) const override;
+    [[nodiscard]] const IfStatementCondition *evaluate(const Model &model,
+                                                       bool doComplete) const override;
 
     explicit IfStatementCondition(const IR::Expression *cond);
 
@@ -109,8 +108,8 @@ class ExtractSuccess : public TraceEvent {
  public:
     [[nodiscard]] const ExtractSuccess *subst(const SymbolicEnv &env) const override;
     const ExtractSuccess *apply(Transform &visitor) const override;
-    void complete(Model *model) const override;
-    [[nodiscard]] const ExtractSuccess *evaluate(const Model &model) const override;
+    [[nodiscard]] const ExtractSuccess *evaluate(const Model &model,
+                                                 bool doComplete) const override;
 
     /// @returns the extracted header label stored in this class.
     [[nodiscard]] const IR::Expression *getExtractedHeader() const;
@@ -179,8 +178,7 @@ class Emit : public TraceEvent {
  public:
     [[nodiscard]] const Emit *subst(const SymbolicEnv &env) const override;
     const Emit *apply(Transform &visitor) const override;
-    void complete(Model *model) const override;
-    [[nodiscard]] const Emit *evaluate(const Model &model) const override;
+    [[nodiscard]] const Emit *evaluate(const Model &model, bool doComplete) const override;
 
     Emit(const IR::Expression *emitHeader,
          std::vector<std::pair<IR::StateVariable, const IR::Expression *>> fields);
@@ -211,9 +209,7 @@ class Packet : public TraceEvent {
 
     const Packet *apply(Transform &visitor) const override;
 
-    void complete(Model *model) const override;
-
-    [[nodiscard]] const Packet *evaluate(const Model &model) const override;
+    [[nodiscard]] const Packet *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] const Packet *subst(const SymbolicEnv &env) const override;
 
diff --git a/backends/p4tools/common/lib/variables.cpp b/backends/p4tools/common/lib/variables.cpp
index b4075ff767..beb3635717 100644
--- a/backends/p4tools/common/lib/variables.cpp
+++ b/backends/p4tools/common/lib/variables.cpp
@@ -18,11 +18,9 @@ const IR::StateVariable &getStateVariable(const IR::Type *type, cstring name) {
     return *new IR::StateVariable(new IR::Member(type, &VAR_PREFIX, name));
 }
 
-const IR::SymbolicVariable *getSymbolicVariable(const IR::Type *type, int incarnation,
-                                                cstring name) {
+const IR::SymbolicVariable *getSymbolicVariable(const IR::Type *type, cstring name) {
     // TODO: Is caching worth it here?
-    auto symbolicName = name + "_" + std::to_string(incarnation);
-    return new IR::SymbolicVariable(type, symbolicName);
+    return new IR::SymbolicVariable(type, name);
 }
 
 IR::StateVariable getHeaderValidity(const IR::Expression *headerRef) {
diff --git a/backends/p4tools/common/lib/variables.h b/backends/p4tools/common/lib/variables.h
index 254dd30ba1..93afa2caf8 100644
--- a/backends/p4tools/common/lib/variables.h
+++ b/backends/p4tools/common/lib/variables.h
@@ -24,8 +24,7 @@ const IR::StateVariable &getStateVariable(const IR::Type *type, cstring name);
 ///
 /// A BUG occurs if this was previously called with the same @name and @incarnation, but with a
 /// different @type.
-const IR::SymbolicVariable *getSymbolicVariable(const IR::Type *type, int incarnation,
-                                                cstring name);
+const IR::SymbolicVariable *getSymbolicVariable(const IR::Type *type, cstring name);
 
 /// @see ToolsVariables::getSymbolicVariable.
 /// This function is used to generated variables caused by undefined behavior. This is merely a
diff --git a/backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp
index 7a5693c2b9..8769146552 100644
--- a/backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp
@@ -341,8 +341,7 @@ const IR::Literal *AbstractStepper::evaluateExpression(
     const IR::Literal *result = nullptr;
     if (solverResult != std::nullopt && *solverResult) {
         auto model = Model(solver.getSymbolicMapping());
-        model.complete(expr);
-        result = model.evaluate(expr);
+        result = model.evaluate(expr, true);
     }
     return result;
 }
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 1552a74d8f..aa1e2c9ce9 100644
--- a/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
@@ -81,12 +81,12 @@ const IR::StateVariable &TableStepper::getTableReachedVar(const IR::P4Table *tab
 }
 
 const IR::Expression *TableStepper::computeTargetMatchType(
-    ExecutionState &nextState, const TableUtils::KeyProperties &keyProperties,
-    TableMatchMap *matches, const IR::Expression *hitCondition) {
+    const TableUtils::KeyProperties &keyProperties, TableMatchMap *matches,
+    const IR::Expression *hitCondition) {
     const IR::Expression *keyExpr = keyProperties.key->expression;
     // Create a new variable constant that corresponds to the key expression.
     cstring keyName = properties.tableName + "_key_" + keyProperties.name;
-    const auto *ctrlPlaneKey = nextState.createSymbolicVariable(keyExpr->type, keyName);
+    const auto *ctrlPlaneKey = ToolsVariables::getSymbolicVariable(keyExpr->type, keyName);
 
     if (keyProperties.matchType == P4Constants::MATCH_KIND_EXACT) {
         hitCondition = new IR::LAnd(hitCondition, new IR::Equ(keyExpr, ctrlPlaneKey));
@@ -101,7 +101,7 @@ const IR::Expression *TableStepper::computeTargetMatchType(
             ternaryMask = IR::getConstant(keyExpr->type, 0);
             keyExpr = ternaryMask;
         } else {
-            ternaryMask = nextState.createSymbolicVariable(keyExpr->type, maskName);
+            ternaryMask = ToolsVariables::getSymbolicVariable(keyExpr->type, maskName);
         }
         matches->emplace(keyProperties.name,
                          new Ternary(keyProperties.key, ctrlPlaneKey, ternaryMask));
@@ -112,7 +112,8 @@ const IR::Expression *TableStepper::computeTargetMatchType(
         const auto *keyType = keyExpr->type->checkedTo<IR::Type_Bits>();
         auto keyWidth = keyType->width_bits();
         cstring maskName = properties.tableName + "_lpm_prefix_" + keyProperties.name;
-        const IR::Expression *maskVar = nextState.createSymbolicVariable(keyExpr->type, maskName);
+        const IR::Expression *maskVar =
+            ToolsVariables::getSymbolicVariable(keyExpr->type, maskName);
         // The maxReturn is the maximum vale for the given bit width. This value is shifted by
         // the mask variable to create a mask (and with that, a prefix).
         auto maxReturn = IR::getMaxBvVal(keyWidth);
@@ -139,10 +140,10 @@ const IR::Expression *TableStepper::computeTargetMatchType(
     TESTGEN_UNIMPLEMENTED("Match type %s not implemented for table keys.", keyProperties.matchType);
 }
 
-const IR::Expression *TableStepper::computeHit(ExecutionState &nextState, TableMatchMap *matches) {
+const IR::Expression *TableStepper::computeHit(TableMatchMap *matches) {
     const IR::Expression *hitCondition = IR::getBoolLiteral(!properties.resolvedKeys.empty());
     for (auto keyProperties : properties.resolvedKeys) {
-        hitCondition = computeTargetMatchType(nextState, keyProperties, matches, hitCondition);
+        hitCondition = computeTargetMatchType(keyProperties, matches, hitCondition);
     }
     return hitCondition;
 }
@@ -285,7 +286,7 @@ void TableStepper::setTableDefaultEntries(
             // Getting the unique name is needed to avoid generating duplicate arguments.
             cstring paramName =
                 properties.tableName + "_arg_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, paramName);
+            const auto &actionArg = ToolsVariables::getSymbolicVariable(parameter->type, paramName);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
             // Note how we use the control plane name for the parameter here.
@@ -334,18 +335,19 @@ void TableStepper::evalTableControlEntries(
     const auto *key = table->getKey();
     BUG_CHECK(key != nullptr, "An empty key list should have been handled earlier.");
 
+    // First, we compute the hit condition to trigger this particular action call.
+    TableMatchMap matches;
+    const auto *hitCondition = computeHit(&matches);
+
+    // Now we iterate over all table actions and create a path per table action.
     for (const auto *action : tableActionList) {
+        // Create an execution state per action.
+        auto &nextState = stepper->state.clone();
         // Grab the path from the method call.
         const auto *tableAction = action->expression->checkedTo<IR::MethodCallExpression>();
         // Try to find the action declaration corresponding to the path reference in the table.
         const auto *actionType = stepper->state.getP4Action(tableAction);
 
-        auto &nextState = stepper->state.clone();
-
-        // First, we compute the hit condition to trigger this particular action call.
-        TableMatchMap matches;
-        const auto *hitCondition = computeHit(nextState, &matches);
-
         // We get the control plane name of the action we are calling.
         cstring actionName = actionType->controlPlaneName();
         // Synthesize arguments for the call based on the action parameters.
@@ -359,7 +361,7 @@ void TableStepper::evalTableControlEntries(
             // Getting the unique name is needed to avoid generating duplicate arguments.
             cstring paramName =
                 properties.tableName + "_arg_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, paramName);
+            const auto &actionArg = ToolsVariables::getSymbolicVariable(parameter->type, paramName);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
             // Note how we use the control plane name for the parameter here.
diff --git a/backends/p4tools/modules/testgen/core/small_step/table_stepper.h b/backends/p4tools/modules/testgen/core/small_step/table_stepper.h
index f79ed0c646..48fc752b48 100644
--- a/backends/p4tools/modules/testgen/core/small_step/table_stepper.h
+++ b/backends/p4tools/modules/testgen/core/small_step/table_stepper.h
@@ -91,14 +91,14 @@ class TableStepper {
     /// these do not match it steps through the default implementation. If it does not match either,
     /// a P4C_UNIMPLEMENTED is thrown.
     virtual const IR::Expression *computeTargetMatchType(
-        ExecutionState &nextState, const TableUtils::KeyProperties &keyProperties,
-        TableMatchMap *matches, const IR::Expression *hitCondition);
+        const TableUtils::KeyProperties &keyProperties, TableMatchMap *matches,
+        const IR::Expression *hitCondition);
 
     /// A helper function that computes whether a control-plane/table-key hits or not. This does not
     /// handle constant entries, it is specialized for control plane entries.
     /// The function also tracks the list of field matches created to achieve a  hit. We later use
     /// this to insert table entries using the STF/PTF framework.
-    const IR::Expression *computeHit(ExecutionState &nextState, TableMatchMap *matches);
+    const IR::Expression *computeHit(TableMatchMap *matches);
 
     /// Collects properties that may be set per table. Target back end may have different semantics
     /// for table execution that need to be collect before evaluation the table.
diff --git a/backends/p4tools/modules/testgen/lib/concolic.cpp b/backends/p4tools/modules/testgen/lib/concolic.cpp
index 7910612916..5cbbd94934 100644
--- a/backends/p4tools/modules/testgen/lib/concolic.cpp
+++ b/backends/p4tools/modules/testgen/lib/concolic.cpp
@@ -38,7 +38,7 @@ bool ConcolicMethodImpls::matches(const std::vector<cstring> &paramNames,
 }
 
 bool ConcolicMethodImpls::exec(cstring concolicMethodName, const IR::ConcolicVariable *var,
-                               const ExecutionState &state, const Model &completedModel,
+                               const ExecutionState &state, const Model &evaluatedModel,
                                ConcolicVariableMap *resolvedConcolicVariables) const {
     if (impls.count(concolicMethodName) == 0) {
         return false;
@@ -66,7 +66,7 @@ bool ConcolicMethodImpls::exec(cstring concolicMethodName, const IR::ConcolicVar
     if (!matchingImpl) {
         return false;
     }
-    (*matchingImpl)(concolicMethodName, var, state, completedModel, resolvedConcolicVariables);
+    (*matchingImpl)(concolicMethodName, var, state, evaluatedModel, resolvedConcolicVariables);
     return true;
 }
 
@@ -98,7 +98,7 @@ bool ConcolicResolver::preorder(const IR::ConcolicVariable *var) {
     // Convert the concolic member variable to a state variable.
     auto concolicReplacment = resolvedConcolicVariables.find(*var);
     if (concolicReplacment == resolvedConcolicVariables.end()) {
-        bool found = concolicMethodImpls.exec(concolicMethodName, var, state, completedModel,
+        bool found = concolicMethodImpls.exec(concolicMethodName, var, state, evaluatedModel,
                                               &resolvedConcolicVariables);
         BUG_CHECK(found, "Unknown or unimplemented concolic method: %1%", concolicMethodName);
     }
@@ -109,17 +109,17 @@ const ConcolicVariableMap *ConcolicResolver::getResolvedConcolicVariables() cons
     return &resolvedConcolicVariables;
 }
 
-ConcolicResolver::ConcolicResolver(const Model &completedModel, const ExecutionState &state,
+ConcolicResolver::ConcolicResolver(const Model &evaluatedModel, const ExecutionState &state,
                                    const ConcolicMethodImpls &concolicMethodImpls)
-    : state(state), completedModel(completedModel), concolicMethodImpls(concolicMethodImpls) {
+    : state(state), evaluatedModel(evaluatedModel), concolicMethodImpls(concolicMethodImpls) {
     visitDagOnce = false;
 }
 
-ConcolicResolver::ConcolicResolver(const Model &completedModel, const ExecutionState &state,
+ConcolicResolver::ConcolicResolver(const Model &evaluatedModel, const ExecutionState &state,
                                    const ConcolicMethodImpls &concolicMethodImpls,
                                    ConcolicVariableMap resolvedConcolicVariables)
     : state(state),
-      completedModel(completedModel),
+      evaluatedModel(evaluatedModel),
       resolvedConcolicVariables(std::move(resolvedConcolicVariables)),
       concolicMethodImpls(concolicMethodImpls) {
     visitDagOnce = false;
diff --git a/backends/p4tools/modules/testgen/lib/concolic.h b/backends/p4tools/modules/testgen/lib/concolic.h
index 2bfd68722e..f7040cab2b 100644
--- a/backends/p4tools/modules/testgen/lib/concolic.h
+++ b/backends/p4tools/modules/testgen/lib/concolic.h
@@ -34,7 +34,7 @@ class ConcolicMethodImpls {
  private:
     using MethodImpl = std::function<void(
         cstring concolicMethodName, const IR::ConcolicVariable *var, const ExecutionState &state,
-        const Model &completedModel, ConcolicVariableMap *resolvedConcolicVariables)>;
+        const Model &evaluatedModel, ConcolicVariableMap *resolvedConcolicVariables)>;
 
     ordered_map<cstring, ordered_map<uint, std::list<std::pair<std::vector<cstring>, MethodImpl>>>>
         impls;
@@ -48,7 +48,7 @@ class ConcolicMethodImpls {
     explicit ConcolicMethodImpls(const ImplList &implList);
 
     bool exec(cstring concolicMethodName, const IR::ConcolicVariable *var,
-              const ExecutionState &state, const Model &completedModel,
+              const ExecutionState &state, const Model &evaluatedModel,
               ConcolicVariableMap *resolvedConcolicVariables) const;
 
     void add(const ImplList &implList);
@@ -56,10 +56,10 @@ class ConcolicMethodImpls {
 
 class ConcolicResolver : public Inspector {
  public:
-    explicit ConcolicResolver(const Model &completedModel, const ExecutionState &state,
+    explicit ConcolicResolver(const Model &evaluatedModel, const ExecutionState &state,
                               const ConcolicMethodImpls &concolicMethodImpls);
 
-    ConcolicResolver(const Model &completedModel, const ExecutionState &state,
+    ConcolicResolver(const Model &evaluatedModel, const ExecutionState &state,
                      const ConcolicMethodImpls &concolicMethodImpls,
                      ConcolicVariableMap resolvedConcolicVariables);
 
@@ -71,8 +71,8 @@ class ConcolicResolver : public Inspector {
     /// Execution state may be used by concolic implementations to access specific state.
     const ExecutionState &state;
 
-    /// The completed model is queried to produce a (random) assignment for concolic inputs.
-    const Model &completedModel;
+    /// The evaluated model is queried to produce a (random) assignment for concolic inputs.
+    const Model &evaluatedModel;
 
     /// A map of the concolic variables and the assertion associated with the variable. These
     /// assertions are used to add constraints to the solver.
diff --git a/backends/p4tools/modules/testgen/lib/execution_state.cpp b/backends/p4tools/modules/testgen/lib/execution_state.cpp
index 22ec38733b..c1cb389824 100644
--- a/backends/p4tools/modules/testgen/lib/execution_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/execution_state.cpp
@@ -40,13 +40,32 @@ namespace P4Tools::P4Testgen {
  *  Constructors
  * ============================================================================================= */
 
+ExecutionState::StackFrame::StackFrame(Continuation normalContinuation,
+                                       const NamespaceContext *namespaces)
+    : StackFrame(std::move(normalContinuation), {}, namespaces) {}
+
+ExecutionState::StackFrame::StackFrame(Continuation normalContinuation,
+                                       ExceptionHandlers exceptionHandlers,
+                                       const NamespaceContext *namespaces)
+    : normalContinuation(std::move(normalContinuation)),
+      exceptionHandlers(std::move(exceptionHandlers)),
+      namespaces(namespaces) {}
+
+const Continuation &ExecutionState::StackFrame::getContinuation() const {
+    return normalContinuation;
+}
+
+const ExecutionState::StackFrame::ExceptionHandlers &
+ExecutionState::StackFrame::getExceptionHandlers() const {
+    return exceptionHandlers;
+}
+
+const NamespaceContext *ExecutionState::StackFrame::getNameSpaces() const { return namespaces; }
+
 ExecutionState::ExecutionState(const IR::P4Program *program)
     : AbstractExecutionState(program),
       body({program}),
       stack(*(new std::stack<std::reference_wrapper<const StackFrame>>())) {
-    // Insert the default symbolic variables of the execution state.
-    // This also makes the symbolic variables present in the state explicit.
-    allocatedSymbolicVariables.insert(getInputPacketSizeVar());
     env.set(&PacketVars::INPUT_PACKET_LABEL, IR::getConstant(IR::getBitType(0), 0));
     env.set(&PacketVars::PACKET_BUFFER_LABEL, IR::getConstant(IR::getBitType(0), 0));
     // We also add the taint property and set it to false.
@@ -65,9 +84,6 @@ ExecutionState::ExecutionState(const IR::P4Program *program)
 
 ExecutionState::ExecutionState(Continuation::Body body)
     : body(std::move(body)), stack(*(new std::stack<std::reference_wrapper<const StackFrame>>())) {
-    // Insert the default symbolic variables of the execution state.
-    // This also makes the symbolic variables present in the state explicit.
-    allocatedSymbolicVariables.insert(getInputPacketSizeVar());
     // We also add the taint property and set it to false.
     setProperty("inUndefinedState", false);
     // Drop is initialized to false, too.
@@ -269,19 +285,19 @@ void ExecutionState::popContinuation(std::optional<const IR::Node *> argument_op
     auto frame = stack.top();
     stack.pop();
 
-    auto newBody = frame.get().normalContinuation.apply(argument_opt);
+    auto newBody = frame.get().getContinuation().apply(argument_opt);
     replaceBody(newBody);
-    setNamespaceContext(frame.get().namespaces);
+    setNamespaceContext(frame.get().getNameSpaces());
 }
 
 void ExecutionState::handleException(Continuation::Exception e) {
     while (!stack.empty()) {
         auto frame = stack.top();
-        if (frame.get().exceptionHandlers.count(e) > 0) {
-            auto k = frame.get().exceptionHandlers.at(e);
+        if (frame.get().getExceptionHandlers().count(e) > 0) {
+            auto k = frame.get().getExceptionHandlers().at(e);
             auto newBody = k.apply(std::nullopt);
             replaceBody(newBody);
-            setNamespaceContext(frame.get().namespaces);
+            setNamespaceContext(frame.get().getNameSpaces());
             return;
         }
         stack.pop();
@@ -317,7 +333,7 @@ void ExecutionState::pushPathConstraint(const IR::Expression *e) { pathConstrain
 void ExecutionState::pushBranchDecision(uint64_t bIdx) { selectedBranches.push_back(bIdx); }
 
 const IR::SymbolicVariable *ExecutionState::getInputPacketSizeVar() {
-    return ToolsVariables::getSymbolicVariable(&PacketVars::PACKET_SIZE_VAR_TYPE, 0,
+    return ToolsVariables::getSymbolicVariable(&PacketVars::PACKET_SIZE_VAR_TYPE,
                                                "*packetLen_bits");
 }
 
@@ -369,8 +385,7 @@ const IR::Expression *ExecutionState::peekPacketBuffer(int amount) {
     if (diff > 0) {
         // We need to enlarge the input packet by the amount we are exceeding the buffer.
         // TODO: How should we perform accounting here?
-        const IR::Expression *newVar = createSymbolicVariable(IR::getBitType(diff), "pktVar",
-                                                              allocatedSymbolicVariables.size());
+        const IR::Expression *newVar = createPacketVariable(IR::getBitType(diff));
         appendToInputPacket(newVar);
         // If the buffer was not empty, append the data we have consumed to the newly generated
         // content and reset the buffer.
@@ -412,8 +427,7 @@ const IR::Expression *ExecutionState::slicePacketBuffer(int amount) {
     if (diff > 0) {
         // We need to enlarge the input packet by the amount we are exceeding the buffer.
         // TODO: How should we perform accounting here?
-        const IR::Expression *newVar = createSymbolicVariable(IR::getBitType(diff), "pktVar",
-                                                              allocatedSymbolicVariables.size());
+        const IR::Expression *newVar = createPacketVariable(IR::getBitType(diff));
         appendToInputPacket(newVar);
         // If the buffer was not empty, append the data we have consumed to the newly generated
         // content and reset the buffer.
@@ -489,22 +503,15 @@ const IR::StateVariable &ExecutionState::getCurrentParserErrorLabel() const {
  *  Variables and symbolic constants
  * ============================================================================================= */
 
-const SymbolicSet &ExecutionState::getSymbolicVariables() const {
-    return allocatedSymbolicVariables;
-}
-
-const IR::SymbolicVariable *ExecutionState::createSymbolicVariable(const IR::Type *type,
-                                                                   cstring name,
-                                                                   uint64_t instanceId) {
-    const auto *variables = ToolsVariables::getSymbolicVariable(type, instanceId, name);
-    const auto &result = allocatedSymbolicVariables.insert(variables);
-    // The variable already existed, check its type.
-    if (!result.second) {
-        BUG_CHECK((*result.first)->type->equiv(*type),
-                  "Inconsistent types for variables variable %1%: previously %2%, but now %3%",
-                  variables->toString(), (*result.first)->type, type);
-    }
-    return variables;
+const IR::SymbolicVariable *ExecutionState::createPacketVariable(const IR::Type *type) {
+    const auto *variable = ToolsVariables::getSymbolicVariable(
+        type, "pktvar_" + std::to_string(numAllocatedPacketVariables));
+    numAllocatedPacketVariables++;
+    BUG_CHECK(numAllocatedPacketVariables < UINT16_MAX,
+              "Allocating too many symbolic packet variables. The symbolic variable counter with "
+              "maximum size %1% counter will overflow.",
+              UINT16_MAX);
+    return variable;
 }
 
 }  // namespace P4Tools::P4Testgen
diff --git a/backends/p4tools/modules/testgen/lib/execution_state.h b/backends/p4tools/modules/testgen/lib/execution_state.h
index be879d4d95..20360825cb 100644
--- a/backends/p4tools/modules/testgen/lib/execution_state.h
+++ b/backends/p4tools/modules/testgen/lib/execution_state.h
@@ -39,18 +39,31 @@ class ExecutionState : public AbstractExecutionState {
      public:
         using ExceptionHandlers = std::map<Continuation::Exception, Continuation>;
 
+     private:
         Continuation normalContinuation;
         ExceptionHandlers exceptionHandlers;
         const NamespaceContext *namespaces = nullptr;
 
-        StackFrame(Continuation normalContinuation, const NamespaceContext *namespaces)
-            : StackFrame(normalContinuation, {}, namespaces) {}
+     public:
+        StackFrame(Continuation normalContinuation, const NamespaceContext *namespaces);
 
         StackFrame(Continuation normalContinuation, ExceptionHandlers exceptionHandlers,
-                   const NamespaceContext *namespaces)
-            : normalContinuation(normalContinuation),
-              exceptionHandlers(exceptionHandlers),
-              namespaces(namespaces) {}
+                   const NamespaceContext *namespaces);
+
+        StackFrame(const StackFrame &) = default;
+        StackFrame(StackFrame &&) noexcept = default;
+        StackFrame &operator=(const StackFrame &) = default;
+        StackFrame &operator=(StackFrame &&) = default;
+        ~StackFrame() = default;
+
+        /// @returns the top-level continuation of this particular stack frame.
+        [[nodiscard]] const Continuation &getContinuation() const;
+
+        /// @returns the exception handlers contained within this stack frame.
+        [[nodiscard]] const ExceptionHandlers &getExceptionHandlers() const;
+
+        /// @returns the namespaces contained within this stack frame.
+        [[nodiscard]] const NamespaceContext *getNameSpaces() const;
     };
 
     /// No move semantics because of constant members. We always need to clone a state.
@@ -59,10 +72,6 @@ class ExecutionState : public AbstractExecutionState {
     ~ExecutionState() override = default;
 
  private:
-    /// The list of variables that have been created in this state.
-    /// These variables are later fed to the model for completion.
-    SymbolicSet allocatedSymbolicVariables;
-
     /// The program trace for the current program point (i.e., how we got to the current state).
     std::vector<std::reference_wrapper<const TraceEvent>> trace;
 
@@ -119,6 +128,16 @@ class ExecutionState : public AbstractExecutionState {
     /// State that is needed to track reachability of statements given a query.
     ReachabilityEngineState *reachabilityEngineState = nullptr;
 
+    /// The number of individual packet variables that have been created in this state.
+    /// Used to create unique symbolic variables in some cases.
+    uint16_t numAllocatedPacketVariables = 0;
+
+    /// Helper function to create a new, unique symbolic packet variable.
+    /// Keeps track of the allocated packet variables by incrementing @ref
+    /// numAllocatedPacketVariables.
+    /// @returns a fresh symbolic variable.
+    [[nodiscard]] const IR::SymbolicVariable *createPacketVariable(const IR::Type *type);
+
     /* =========================================================================================
      *  Accessors
      * ========================================================================================= */
@@ -366,22 +385,6 @@ class ExecutionState : public AbstractExecutionState {
     /// @returns the current parser error label. Throws a BUG if the label is a nullptr.
     [[nodiscard]] const IR::StateVariable &getCurrentParserErrorLabel() const;
 
-    /* =========================================================================================
-     *  Variables and symbolic constants.
-     * =========================================================================================
-     *  These mirror what's available in IRUtils, but automatically fill in the incarnation number,
-     *  based on how many times newParser() has been called.
-     */
-    /// @returns the symbolic variables that were allocated in this state
-    [[nodiscard]] const SymbolicSet &getSymbolicVariables() const;
-
-    /// @see ToolsVariables::getSymbolicVariable.
-    /// We also place the symbolic variables in the set of allocated symbolic variables of this
-    /// state.
-    [[nodiscard]] const IR::SymbolicVariable *createSymbolicVariable(const IR::Type *type,
-                                                                     cstring name,
-                                                                     uint64_t instanceID = 0);
-
     /* =========================================================================================
      *  Constructors
      * ========================================================================================= */
diff --git a/backends/p4tools/modules/testgen/lib/final_state.cpp b/backends/p4tools/modules/testgen/lib/final_state.cpp
index 5679ae0afc..6e580a30e5 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/final_state.cpp
@@ -28,7 +28,7 @@ FinalState::FinalState(AbstractSolver &solver, const ExecutionState &finalState)
       state(finalState),
       completedModel(completeModel(finalState, new Model(solver.getSymbolicMapping()))) {
     for (const auto &event : finalState.getTrace()) {
-        trace.emplace_back(*event.get().evaluate(completedModel));
+        trace.emplace_back(*event.get().evaluate(completedModel, true));
     }
 }
 
@@ -36,13 +36,13 @@ FinalState::FinalState(AbstractSolver &solver, const ExecutionState &finalState,
                        const Model &completedModel)
     : solver(solver), state(finalState), completedModel(completedModel) {
     for (const auto &event : finalState.getTrace()) {
-        trace.emplace_back(*event.get().evaluate(completedModel));
+        trace.emplace_back(*event.get().evaluate(completedModel, true));
     }
 }
 
 void FinalState::calculatePayload(const ExecutionState &executionState, Model &evaluatedModel) {
     const auto &packetBitSizeVar = ExecutionState::getInputPacketSizeVar();
-    const auto *payloadSizeConst = evaluatedModel.evaluate(packetBitSizeVar);
+    const auto *payloadSizeConst = evaluatedModel.evaluate(packetBitSizeVar, true);
     int calculatedPacketSize = IR::getIntFromLiteral(payloadSizeConst);
     const auto *inputPacketExpr = executionState.getInputPacket();
     int payloadSize = calculatedPacketSize - inputPacketExpr->type->width_bits();
@@ -58,24 +58,14 @@ void FinalState::calculatePayload(const ExecutionState &executionState, Model &e
 
 Model &FinalState::completeModel(const ExecutionState &finalState, const Model *model,
                                  bool postProcess) {
-    // Complete the model based on the symbolic environment.
-    auto *completedModel = finalState.getSymbolicEnv().complete(*model);
-
-    // Also complete all the symbolic variables that were collected in this state.
-    const auto &symbolicVars = finalState.getSymbolicVariables();
-    completedModel->complete(symbolicVars);
-
     // Now that the models initial values are completed evaluate the values that
     // are part of the constraints that have been added to the solver.
-    auto *evaluatedModel = finalState.getSymbolicEnv().evaluate(*completedModel);
+    auto *evaluatedModel = finalState.getSymbolicEnv().evaluate(*model);
 
     if (postProcess) {
         // Append a payload, if requested.
         calculatePayload(finalState, *evaluatedModel);
     }
-    for (const auto &event : finalState.getTrace()) {
-        event.get().complete(evaluatedModel);
-    }
 
     return *evaluatedModel;
 }
diff --git a/backends/p4tools/modules/testgen/lib/test_backend.cpp b/backends/p4tools/modules/testgen/lib/test_backend.cpp
index 18eb5be9d4..87ed321e06 100644
--- a/backends/p4tools/modules/testgen/lib/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/lib/test_backend.cpp
@@ -144,8 +144,8 @@ TestBackEnd::TestInfo TestBackEnd::produceTestInfo(
     const std::vector<std::reference_wrapper<const TraceEvent>> *programTraces) {
     // Evaluate all the important expressions necessary for program execution by using the
     // completed model.
-    int calculatedPacketSize =
-        IR::getIntFromLiteral(completedModel->evaluate(ExecutionState::getInputPacketSizeVar()));
+    int calculatedPacketSize = IR::getIntFromLiteral(
+        completedModel->evaluate(ExecutionState::getInputPacketSizeVar(), true));
     const auto *inputPacketExpr = executionState->getInputPacket();
     // The payload fills the space between the minimum input size needed and the symbolically
     // calculated packet size.
@@ -157,12 +157,12 @@ TestBackEnd::TestInfo TestBackEnd::produceTestInfo(
             IR::getBitType(outputPacketExpr->type->width_bits() + payloadExpr->type->width_bits()),
             outputPacketExpr, payloadExpr);
     }
-    const auto *inputPacket = completedModel->evaluate(inputPacketExpr);
-    const auto *outputPacket = completedModel->evaluate(outputPacketExpr);
+    const auto *inputPacket = completedModel->evaluate(inputPacketExpr, true);
+    const auto *outputPacket = completedModel->evaluate(outputPacketExpr, true);
     const auto *inputPort =
-        completedModel->evaluate(executionState->get(programInfo.getTargetInputPortVar()));
+        completedModel->evaluate(executionState->get(programInfo.getTargetInputPortVar()), true);
 
-    const auto *outputPortVar = completedModel->evaluate(outputPortExpr);
+    const auto *outputPortVar = completedModel->evaluate(outputPortExpr, true);
     // Build the taint mask by dissecting the program packet variable
     const auto *evalMask = Taint::buildTaintMask(executionState->getSymbolicEnv().getInternalMap(),
                                                  completedModel, outputPacketExpr);
diff --git a/backends/p4tools/modules/testgen/lib/test_object.h b/backends/p4tools/modules/testgen/lib/test_object.h
index 3145f3bd89..63b9c72b3f 100644
--- a/backends/p4tools/modules/testgen/lib/test_object.h
+++ b/backends/p4tools/modules/testgen/lib/test_object.h
@@ -26,7 +26,7 @@ class TestObject : public ICastable {
 
     /// @returns a version of the test object where all expressions are resolved and symbolic
     /// variables are substituted according to the mapping present in the @param model.
-    [[nodiscard]] virtual const TestObject *evaluate(const Model &model) const = 0;
+    [[nodiscard]] virtual const TestObject *evaluate(const Model &model, bool doComplete) const = 0;
 };
 
 /// A map of test objects.
diff --git a/backends/p4tools/modules/testgen/lib/test_spec.cpp b/backends/p4tools/modules/testgen/lib/test_spec.cpp
index c775a4d8d3..4acb1a7e16 100644
--- a/backends/p4tools/modules/testgen/lib/test_spec.cpp
+++ b/backends/p4tools/modules/testgen/lib/test_spec.cpp
@@ -45,9 +45,9 @@ const IR::Constant *Packet::getEvaluatedPayload() const {
     return constant;
 }
 
-const Packet *Packet::evaluate(const Model &model) const {
-    const auto *newPayload = model.evaluate(payload);
-    const auto *newPayloadIgnoreMask = model.evaluate(payloadIgnoreMask);
+const Packet *Packet::evaluate(const Model &model, bool doComplete) const {
+    const auto *newPayload = model.evaluate(payload, true);
+    const auto *newPayloadIgnoreMask = model.evaluate(payloadIgnoreMask, doComplete);
     return new Packet(port, newPayload, newPayloadIgnoreMask);
 }
 
@@ -76,8 +76,8 @@ const IR::Constant *ActionArg::getEvaluatedValue() const {
 
 cstring ActionArg::getObjectName() const { return "ActionArg"; }
 
-const ActionArg *ActionArg::evaluate(const Model &model) const {
-    const auto &newValue = model.evaluate(value);
+const ActionArg *ActionArg::evaluate(const Model &model, bool doComplete) const {
+    const auto &newValue = model.evaluate(value, doComplete);
     return new ActionArg(param, newValue);
 }
 
@@ -91,11 +91,11 @@ cstring ActionCall::getActionName() const { return identifier; }
 
 const IR::P4Action *ActionCall::getAction() const { return action; }
 
-const ActionCall *ActionCall::evaluate(const Model &model) const {
+const ActionCall *ActionCall::evaluate(const Model &model, bool doComplete) const {
     std::vector<ActionArg> evaluatedArgs;
     evaluatedArgs.reserve(args.size());
     for (const auto &actionArg : args) {
-        evaluatedArgs.emplace_back(*actionArg.evaluate(model));
+        evaluatedArgs.emplace_back(*actionArg.evaluate(model, doComplete));
     }
     return new ActionCall(identifier, action, evaluatedArgs);
 }
@@ -129,9 +129,9 @@ const IR::Constant *Ternary::getEvaluatedMask() const {
     return constant;
 }
 
-const Ternary *Ternary::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(value);
-    const auto *evaluatedMask = model.evaluate(mask);
+const Ternary *Ternary::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
+    const auto *evaluatedMask = model.evaluate(mask, doComplete);
     return new Ternary(getKey(), evaluatedValue, evaluatedMask);
 }
 
@@ -158,9 +158,9 @@ const IR::Constant *LPM::getEvaluatedPrefixLength() const {
     return constant;
 }
 
-const LPM *LPM::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(value);
-    const auto *evaluatedPrefixLength = model.evaluate(prefixLength);
+const LPM *LPM::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
+    const auto *evaluatedPrefixLength = model.evaluate(prefixLength, doComplete);
     return new LPM(getKey(), evaluatedValue, evaluatedPrefixLength);
 }
 
@@ -177,8 +177,8 @@ const IR::Constant *Exact::getEvaluatedValue() const {
     return constant;
 }
 
-const Exact *Exact::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(value);
+const Exact *Exact::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
     return new Exact(getKey(), evaluatedValue);
 }
 
@@ -197,16 +197,16 @@ int TableRule::getTTL() const { return ttl; }
 
 cstring TableRule::getObjectName() const { return "TableRule"; }
 
-const TableRule *TableRule::evaluate(const Model &model) const {
+const TableRule *TableRule::evaluate(const Model &model, bool doComplete) const {
     TableMatchMap evaluatedMatches;
     for (const auto &matchTuple : matches) {
         auto name = matchTuple.first;
         const auto &match = matchTuple.second;
         // This is a lambda function that applies the visitor to each variant.
-        const auto *evaluatedMatch = match->evaluate(model)->checkedTo<TableMatch>();
+        const auto *evaluatedMatch = match->evaluate(model, doComplete)->checkedTo<TableMatch>();
         evaluatedMatches[name] = evaluatedMatch;
     }
-    const auto *evaluatedAction = action.evaluate(model);
+    const auto *evaluatedAction = action.evaluate(model, doComplete);
     return new TableRule(evaluatedMatches, priority, *evaluatedAction, ttl);
 }
 
@@ -240,10 +240,10 @@ void TableConfig::addTableProperty(cstring propertyName, const TestObject *prope
     tableProperties[propertyName] = property;
 }
 
-const TableConfig *TableConfig::evaluate(const Model &model) const {
+const TableConfig *TableConfig::evaluate(const Model &model, bool doComplete) const {
     std::vector<TableRule> evaluatedRules;
     for (const auto &rule : rules) {
-        const auto *evaluatedRule = rule.evaluate(model);
+        const auto *evaluatedRule = rule.evaluate(model, doComplete);
         evaluatedRules.emplace_back(*evaluatedRule);
     }
     TestObjectMap evaluatedProperties;
@@ -251,7 +251,7 @@ const TableConfig *TableConfig::evaluate(const Model &model) const {
         auto name = propertyTuple.first;
         const auto *property = propertyTuple.second;
         // This is a lambda function that applies the visitor to each variant.
-        const auto *evaluatedProperty = property->evaluate(model);
+        const auto *evaluatedProperty = property->evaluate(model, doComplete);
         evaluatedProperties.emplace(name, evaluatedProperty);
     }
     return new TableConfig(table, evaluatedRules, evaluatedProperties);
diff --git a/backends/p4tools/modules/testgen/lib/test_spec.h b/backends/p4tools/modules/testgen/lib/test_spec.h
index f791849a0c..ef299585e2 100644
--- a/backends/p4tools/modules/testgen/lib/test_spec.h
+++ b/backends/p4tools/modules/testgen/lib/test_spec.h
@@ -38,7 +38,7 @@ class Packet : public TestObject {
  public:
     Packet(int port, const IR::Expression *payload, const IR::Expression *payloadIgnoreMask);
 
-    [[nodiscard]] const Packet *evaluate(const Model &model) const override;
+    [[nodiscard]] const Packet *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -71,7 +71,7 @@ class ActionArg : public TestObject {
  public:
     ActionArg(const IR::Parameter *param, const IR::Expression *value);
 
-    [[nodiscard]] const ActionArg *evaluate(const Model &model) const override;
+    [[nodiscard]] const ActionArg *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -102,7 +102,7 @@ class ActionCall : public TestObject {
 
     ActionCall(const IR::P4Action *action, std::vector<ActionArg> args);
 
-    [[nodiscard]] const ActionCall *evaluate(const Model &model) const override;
+    [[nodiscard]] const ActionCall *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -143,7 +143,7 @@ class Ternary : public TableMatch {
     explicit Ternary(const IR::KeyElement *key, const IR::Expression *value,
                      const IR::Expression *mask);
 
-    [[nodiscard]] const Ternary *evaluate(const Model &model) const override;
+    [[nodiscard]] const Ternary *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -170,7 +170,7 @@ class LPM : public TableMatch {
     explicit LPM(const IR::KeyElement *key, const IR::Expression *value,
                  const IR::Expression *prefixLength);
 
-    [[nodiscard]] const LPM *evaluate(const Model &model) const override;
+    [[nodiscard]] const LPM *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -193,7 +193,7 @@ class Exact : public TableMatch {
  public:
     explicit Exact(const IR::KeyElement *key, const IR::Expression *value);
 
-    [[nodiscard]] const Exact *evaluate(const Model &model) const override;
+    [[nodiscard]] const Exact *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -217,7 +217,7 @@ class TableRule : public TestObject {
  public:
     TableRule(TableMatchMap matches, int priority, ActionCall action, int ttl);
 
-    [[nodiscard]] const TableRule *evaluate(const Model &model) const override;
+    [[nodiscard]] const TableRule *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -255,7 +255,7 @@ class TableConfig : public TestObject {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const TableConfig *evaluate(const Model &model) const override;
+    [[nodiscard]] const TableConfig *evaluate(const Model &model, bool doComplete) const override;
 
     /// @returns the table rules of this table.
     [[nodiscard]] const std::vector<TableRule> *getRules() const;
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp
index 8df5e0a7d6..711330a18c 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp
@@ -11,6 +11,7 @@
 #include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/lib/arch_spec.h"
 #include "backends/p4tools/common/lib/constants.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/id.h"
 #include "ir/ir.h"
 #include "ir/irutils.h"
@@ -80,7 +81,7 @@ void Bmv2V1ModelCmdStepper::initializeTargetEnvironment(ExecutionState &nextStat
     const auto *nineBitType = IR::getBitType(9);
     const auto *oneBitType = IR::getBitType(1);
     nextState.set(programInfo.getTargetInputPortVar(),
-                  nextState.createSymbolicVariable(nineBitType, "bmv2_ingress_port"));
+                  ToolsVariables::getSymbolicVariable(nineBitType, "bmv2_ingress_port"));
     // BMv2 implicitly sets the output port to 0.
     nextState.set(programInfo.getTargetOutputPortVar(), IR::getConstant(nineBitType, 0));
     // Initialize parser_err with no error.
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp b/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp
index 19d5512065..d1104eb028 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp
@@ -100,8 +100,8 @@ big_int Bmv2Concolic::computeChecksum(const std::vector<const IR::Expression *>
             const auto *remainderExpr = IR::getConstant(IR::getBitType(fillWidth), 0);
             concatExpr = new IR::Concat(IR::getBitType(concatWidth), concatExpr, remainderExpr);
         }
-        auto dataInt =
-            IR::getBigIntFromLiteral(completedModel.evaluate(concatExpr, resolvedExpressions));
+        auto dataInt = IR::getBigIntFromLiteral(
+            completedModel.evaluate(concatExpr, true, resolvedExpressions));
         bytes = convertBigIntToBytes(dataInt, concatWidth);
     }
     return checksumFun(bytes.data(), bytes.size());
@@ -137,11 +137,12 @@ const ConcolicMethodImpls::ImplList Bmv2Concolic::BMV2_CONCOLIC_METHOD_IMPLS{
          // Assign arguments to concrete variables and perform type checking.
          auto algo = args->at(1)->expression->checkedTo<IR::Constant>()->asInt();
          Model::ExpressionMap resolvedExpressions;
-         const auto *base = completedModel.evaluate(args->at(2)->expression, &resolvedExpressions);
+         const auto *base =
+             completedModel.evaluate(args->at(2)->expression, true, &resolvedExpressions);
          auto baseInt = IR::getBigIntFromLiteral(base);
          const auto *dataExpr = args->at(3)->expression;
          const auto *maxHash =
-             completedModel.evaluate(args->at(4)->expression, &resolvedExpressions);
+             completedModel.evaluate(args->at(4)->expression, true, &resolvedExpressions);
          auto maxHashInt = IR::getBigIntFromLiteral(maxHash);
 
          /// Flatten the data input and compute the byte array that will be used for
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
index 14769fcf9a..553bf10afe 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
@@ -92,7 +92,7 @@ void Bmv2V1ModelExprStepper::processClone(const ExecutionState &state,
     const auto &preserveIndex = cloneInfo->getPreserveIndex();
     const auto &egressPortVar = programInfo.getTargetOutputPortVar();
     const auto &clonePortVar =
-        ToolsVariables::getSymbolicVariable(egressPortVar->type, 0, "clone_port_var");
+        ToolsVariables::getSymbolicVariable(egressPortVar->type, "clone_port_var");
 
     uint64_t recirculateCount = 0;
     if (state.hasProperty("recirculate_count")) {
@@ -912,7 +912,7 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
              const auto *meterState =
                  state.getTestObject("meter_values", externInstance->controlPlaneName(), false);
              Bmv2V1ModelMeterValue *meterValue = nullptr;
-             const auto &inputValue = nextState.createSymbolicVariable(
+             const auto &inputValue = ToolsVariables::getSymbolicVariable(
                  meterResult->type, "meter_value" + std::to_string(call->clone_id));
              // Make sure we do not accidentally get "3" as enum assignment...
              auto *cond = new IR::Lss(inputValue, IR::getConstant(meterResult->type, 3));
@@ -1013,7 +1013,7 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
              const auto *meterState =
                  state.getTestObject("meter_values", externInstance->controlPlaneName(), false);
              Bmv2V1ModelMeterValue *meterValue = nullptr;
-             const auto &inputValue = nextState.createSymbolicVariable(
+             const auto &inputValue = ToolsVariables::getSymbolicVariable(
                  meterResult->type, "meter_value" + std::to_string(call->clone_id));
              // Make sure we do not accidentally get "3" as enum assignment...
              auto *cond = new IR::Lss(inputValue, IR::getConstant(meterResult->type, 3));
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
index d0f43de8a3..456b3b58de 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
@@ -151,7 +151,7 @@ const IR::Expression *makeConstant(Token input, const IR::Vector<IR::KeyElement>
             } else {
                 BUG("Unexpected key type %s.", keyType->node_type_name());
             }
-            return ToolsVariables::getSymbolicVariable(type, 0, std::string(inputStr));
+            return ToolsVariables::getSymbolicVariable(type, std::string(inputStr));
         }
     }
     if (input.is(Token::Kind::Number)) {
@@ -162,8 +162,7 @@ const IR::Expression *makeConstant(Token input, const IR::Vector<IR::KeyElement>
     }
     // TODO: Is this the right solution for priorities?
     if (input.is(Token::Kind::Priority)) {
-        return ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(32), 0,
-                                                   std::string(inputStr));
+        return ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(32), std::string(inputStr));
     }
     BUG_CHECK(result != nullptr,
               "Could not match restriction key label %s was not found in key list.",
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp
index ae9a9e32cc..9ce0700b80 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.cpp
@@ -34,7 +34,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
     } else {
         tmp = currentName + currentKeyName;
     }
-    auto left = ToolsVariables::getSymbolicVariable(type, 0, tmp);
+    auto left = ToolsVariables::getSymbolicVariable(type, tmp);
     std::string str = currentName.c_str();
     std::vector<std::string> elems;
     std::stringstream ss(str);
@@ -47,7 +47,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
         str += elems[i] + ".";
     }
     tmp = str + destTableName + "_key_" + destKeyName;
-    auto right = ToolsVariables::getSymbolicVariable(type, 0, tmp);
+    auto right = ToolsVariables::getSymbolicVariable(type, tmp);
     auto *expr = new IR::Equ(left, right);
     std::vector<const IR::Expression *> constraint;
     constraint.push_back(expr);
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
index 23c1b22a74..44782b7aea 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
@@ -9,6 +9,7 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/lib/trace_event_types.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/declaration.h"
 #include "ir/id.h"
 #include "ir/irutils.h"
@@ -36,8 +37,8 @@
 namespace P4Tools::P4Testgen::Bmv2 {
 
 const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
-    ExecutionState &nextState, const TableUtils::KeyProperties &keyProperties,
-    TableMatchMap *matches, const IR::Expression *hitCondition) {
+    const TableUtils::KeyProperties &keyProperties, TableMatchMap *matches,
+    const IR::Expression *hitCondition) {
     const IR::Expression *keyExpr = keyProperties.key->expression;
 
     // TODO: We consider optional match types to be a no-op, but we could make them exact matches.
@@ -45,7 +46,7 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
         // We can recover from taint by simply not adding the optional match.
         // Create a new symbolic variable that corresponds to the key expression.
         cstring keyName = properties.tableName + "_key_" + keyProperties.name;
-        const auto ctrlPlaneKey = nextState.createSymbolicVariable(keyExpr->type, keyName);
+        const auto *ctrlPlaneKey = ToolsVariables::getSymbolicVariable(keyExpr->type, keyName);
         if (keyProperties.isTainted) {
             matches->emplace(keyProperties.name,
                              new Optional(keyProperties.key, ctrlPlaneKey, false));
@@ -75,8 +76,8 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
             maxKey = IR::getConstant(keyExpr->type, IR::getMaxBvVal(keyExpr->type));
             keyExpr = minKey;
         } else {
-            minKey = nextState.createSymbolicVariable(keyExpr->type, minName);
-            maxKey = nextState.createSymbolicVariable(keyExpr->type, maxName);
+            minKey = ToolsVariables::getSymbolicVariable(keyExpr->type, minName);
+            maxKey = ToolsVariables::getSymbolicVariable(keyExpr->type, maxName);
         }
         matches->emplace(keyProperties.name, new Range(keyProperties.key, minKey, maxKey));
         return new IR::LAnd(hitCondition, new IR::LAnd(new IR::LAnd(new IR::Lss(minKey, maxKey),
@@ -84,13 +85,18 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
                                                        new IR::Leq(keyExpr, maxKey)));
     }
     // If the custom match type does not match, delete to the core match types.
-    return TableStepper::computeTargetMatchType(nextState, keyProperties, matches, hitCondition);
+    return TableStepper::computeTargetMatchType(keyProperties, matches, hitCondition);
 }
 
 void Bmv2V1ModelTableStepper::evalTableActionProfile(
     const std::vector<const IR::ActionListElement *> &tableActionList) {
     const auto *state = getExecutionState();
 
+    // First, we compute the hit condition to trigger this particular action call.
+    TableMatchMap matches;
+    const auto *hitCondition = computeHit(&matches);
+
+    // Now we iterate over all table actions and create a path per table action.
     for (const auto *action : tableActionList) {
         // Grab the path from the method call.
         const auto *tableAction = action->expression->checkedTo<IR::MethodCallExpression>();
@@ -113,7 +119,7 @@ void Bmv2V1ModelTableStepper::evalTableActionProfile(
             // Getting the unique name is needed to avoid generating duplicate arguments.
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
+            const auto &actionArg = ToolsVariables::getSymbolicVariable(parameter->type, keyName);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
             // Note how we use the control plane name for the parameter here.
@@ -129,10 +135,6 @@ void Bmv2V1ModelTableStepper::evalTableActionProfile(
         auto *synthesizedAction = tableAction->clone();
         synthesizedAction->arguments = arguments;
 
-        // Now we compute the hit condition to trigger this particular action call.
-        TableMatchMap matches;
-        const auto *hitCondition = computeHit(nextState, &matches);
-
         // We need to set the table action in the state for eventual switch action_run hits.
         // We also will need it for control plane table entries.
         setTableAction(nextState, tableAction);
@@ -175,6 +177,11 @@ void Bmv2V1ModelTableStepper::evalTableActionSelector(
     const std::vector<const IR::ActionListElement *> &tableActionList) {
     const auto *state = getExecutionState();
 
+    // First, we compute the hit condition to trigger this particular action call.
+    TableMatchMap matches;
+    const auto *hitCondition = computeHit(&matches);
+
+    // Now we iterate over all table actions and create a path per table action.
     for (const auto *action : tableActionList) {
         // Grab the path from the method call.
         const auto *tableAction = action->expression->checkedTo<IR::MethodCallExpression>();
@@ -199,7 +206,7 @@ void Bmv2V1ModelTableStepper::evalTableActionSelector(
             // Getting the unique name is needed to avoid generating duplicate arguments.
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
+            const auto &actionArg = ToolsVariables::getSymbolicVariable(parameter->type, keyName);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
             // Note how we use the control plane name for the parameter here.
@@ -221,10 +228,6 @@ void Bmv2V1ModelTableStepper::evalTableActionSelector(
         auto *synthesizedAction = tableAction->clone();
         synthesizedAction->arguments = arguments;
 
-        // Now we compute the hit condition to trigger this particular action call.
-        TableMatchMap matches;
-        const auto *hitCondition = computeHit(nextState, &matches);
-
         // We need to set the table action in the state for eventual switch action_run hits.
         // We also will need it for control plane table entries.
         setTableAction(nextState, tableAction);
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.h b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.h
index 38e6f365ca..7ff9533213 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.h
@@ -56,8 +56,7 @@ class Bmv2V1ModelTableStepper : public TableStepper {
     void evalTableActionSelector(const std::vector<const IR::ActionListElement *> &tableActionList);
 
  protected:
-    const IR::Expression *computeTargetMatchType(ExecutionState &nextState,
-                                                 const TableUtils::KeyProperties &keyProperties,
+    const IR::Expression *computeTargetMatchType(const TableUtils::KeyProperties &keyProperties,
                                                  TableMatchMap *matches,
                                                  const IR::Expression *hitCondition) override;
 
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp b/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp
index 43eb5fc6b7..78a95e0ff8 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp
@@ -66,10 +66,10 @@ Bmv2TestBackend::Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecuto
 }
 
 TestBackEnd::TestInfo Bmv2TestBackend::produceTestInfo(
-    const ExecutionState *executionState, const Model *completedModel,
+    const ExecutionState *executionState, const Model *finalModel,
     const IR::Expression *outputPacketExpr, const IR::Expression *outputPortExpr,
     const std::vector<std::reference_wrapper<const TraceEvent>> *programTraces) {
-    auto testInfo = TestBackEnd::produceTestInfo(executionState, completedModel, outputPacketExpr,
+    auto testInfo = TestBackEnd::produceTestInfo(executionState, finalModel, outputPacketExpr,
                                                  outputPortExpr, programTraces);
     // This is a hack to deal with a behavioral model quirk.
     // Packets that are too small are truncated to 02000000 (in hex) with width 32 bit.
@@ -84,8 +84,7 @@ TestBackEnd::TestInfo Bmv2TestBackend::produceTestInfo(
 }
 
 const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionState,
-                                                const Model *completedModel,
-                                                const TestInfo &testInfo) {
+                                                const Model *finalModel, const TestInfo &testInfo) {
     // Create a testSpec.
     TestSpec *testSpec = nullptr;
 
@@ -109,7 +108,7 @@ const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionS
         const auto &flatFields = executionState->getFlatFields(
             localMetadataVar, localMetadataType->checkedTo<IR::Type_Struct>(), {});
         for (const auto &fieldRef : flatFields) {
-            const auto *fieldVal = completedModel->evaluate(executionState->get(fieldRef));
+            const auto *fieldVal = finalModel->evaluate(executionState->get(fieldRef), true);
             // Try to remove the leading internal name for the metadata field.
             // Thankfully, this string manipulation is safe if we are out of range.
             auto fieldString = fieldRef->toString();
@@ -127,7 +126,7 @@ const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionS
     for (const auto &tablePair : uninterpretedTableConfigs) {
         const auto tableName = tablePair.first;
         const auto *uninterpretedTableConfig = tablePair.second->checkedTo<TableConfig>();
-        const auto *const tableConfig = uninterpretedTableConfig->evaluate(*completedModel);
+        const auto *tableConfig = uninterpretedTableConfig->evaluate(*finalModel, true);
         testSpec->addTestObject("tables", tableName, tableConfig);
     }
 
@@ -135,7 +134,7 @@ const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionS
     for (const auto &testObject : actionProfiles) {
         const auto profileName = testObject.first;
         const auto *actionProfile = testObject.second->checkedTo<Bmv2V1ModelActionProfile>();
-        const auto *evaluatedProfile = actionProfile->evaluate(*completedModel);
+        const auto *evaluatedProfile = actionProfile->evaluate(*finalModel, true);
         testSpec->addTestObject("action_profiles", profileName, evaluatedProfile);
     }
 
@@ -143,7 +142,7 @@ const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionS
     for (const auto &testObject : actionSelectors) {
         const auto selectorName = testObject.first;
         const auto *actionSelector = testObject.second->checkedTo<Bmv2V1ModelActionSelector>();
-        const auto *evaluatedSelector = actionSelector->evaluate(*completedModel);
+        const auto *evaluatedSelector = actionSelector->evaluate(*finalModel, true);
         testSpec->addTestObject("action_selectors", selectorName, evaluatedSelector);
     }
 
@@ -151,7 +150,7 @@ const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionS
     for (const auto &testObject : cloneSpecs) {
         const auto sessionId = testObject.first;
         const auto *cloneSpec = testObject.second->checkedTo<Bmv2V1ModelCloneSpec>();
-        const auto *evaluatedInfo = cloneSpec->evaluate(*completedModel);
+        const auto *evaluatedInfo = cloneSpec->evaluate(*finalModel, true);
         testSpec->addTestObject("clone_specs", sessionId, evaluatedInfo);
     }
 
@@ -159,7 +158,7 @@ const TestSpec *Bmv2TestBackend::createTestSpec(const ExecutionState *executionS
     for (const auto &testObject : meterInfos) {
         const auto meterName = testObject.first;
         const auto *meterInfo = testObject.second->checkedTo<Bmv2V1ModelMeterValue>();
-        const auto *evaluateMeterValue = meterInfo->evaluate(*completedModel);
+        const auto *evaluateMeterValue = meterInfo->evaluate(*finalModel, true);
         testSpec->addTestObject("meter_values", meterName, evaluateMeterValue);
     }
 
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test_spec.cpp b/backends/p4tools/modules/testgen/targets/bmv2/test_spec.cpp
index 98c93195a1..1ffadacd1a 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/test_spec.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/test_spec.cpp
@@ -34,9 +34,9 @@ const IR::Expression *IndexExpression::getValue() const { return value; }
 
 cstring IndexExpression::getObjectName() const { return "IndexExpression"; }
 
-const IndexExpression *IndexExpression::evaluate(const Model &model) const {
-    const auto *evaluatedIndex = model.evaluate(index);
-    const auto *evaluatedValue = model.evaluate(value);
+const IndexExpression *IndexExpression::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedIndex = model.evaluate(index, doComplete);
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
     return new IndexExpression(evaluatedIndex, evaluatedValue);
 }
 
@@ -91,11 +91,12 @@ Bmv2V1ModelRegisterValue::Bmv2V1ModelRegisterValue(const IR::Expression *initial
 
 cstring Bmv2V1ModelRegisterValue::getObjectName() const { return "Bmv2V1ModelRegisterValue"; }
 
-const Bmv2V1ModelRegisterValue *Bmv2V1ModelRegisterValue::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(getInitialValue());
+const Bmv2V1ModelRegisterValue *Bmv2V1ModelRegisterValue::evaluate(const Model &model,
+                                                                   bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(getInitialValue(), doComplete);
     auto *evaluatedRegisterValue = new Bmv2V1ModelRegisterValue(evaluatedValue);
     for (const auto &cond : indexConditions) {
-        const auto *evaluatedCond = cond.evaluate(model);
+        const auto *evaluatedCond = cond.evaluate(model, doComplete);
         evaluatedRegisterValue->writeToIndex(evaluatedCond->getEvaluatedIndex(),
                                              evaluatedCond->getEvaluatedValue());
     }
@@ -111,11 +112,12 @@ Bmv2V1ModelMeterValue::Bmv2V1ModelMeterValue(const IR::Expression *initialValue,
 
 cstring Bmv2V1ModelMeterValue::getObjectName() const { return "Bmv2V1ModelMeterValue"; }
 
-const Bmv2V1ModelMeterValue *Bmv2V1ModelMeterValue::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(getInitialValue());
+const Bmv2V1ModelMeterValue *Bmv2V1ModelMeterValue::evaluate(const Model &model,
+                                                             bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(getInitialValue(), doComplete);
     auto *evaluatedMeterValue = new Bmv2V1ModelMeterValue(evaluatedValue, isDirect);
     for (const auto &cond : indexConditions) {
-        const auto *evaluatedCond = cond.evaluate(model);
+        const auto *evaluatedCond = cond.evaluate(model, doComplete);
         evaluatedMeterValue->writeToIndex(evaluatedCond->getEvaluatedIndex(),
                                           evaluatedCond->getEvaluatedValue());
     }
@@ -146,14 +148,15 @@ void Bmv2V1ModelActionProfile::addToActionMap(cstring actionName,
 }
 size_t Bmv2V1ModelActionProfile::getActionMapSize() const { return actions.size(); }
 
-const Bmv2V1ModelActionProfile *Bmv2V1ModelActionProfile::evaluate(const Model &model) const {
+const Bmv2V1ModelActionProfile *Bmv2V1ModelActionProfile::evaluate(const Model &model,
+                                                                   bool doComplete) const {
     auto *profile = new Bmv2V1ModelActionProfile(profileDecl);
     for (const auto &actionTuple : actions) {
         auto actionArgs = actionTuple.second;
         std::vector<ActionArg> evaluatedArgs;
         evaluatedArgs.reserve(actionArgs.size());
         for (const auto &actionArg : actionArgs) {
-            evaluatedArgs.emplace_back(*actionArg.evaluate(model));
+            evaluatedArgs.emplace_back(*actionArg.evaluate(model, doComplete));
         }
         profile->addToActionMap(actionTuple.first, evaluatedArgs);
     }
@@ -176,8 +179,9 @@ const Bmv2V1ModelActionProfile *Bmv2V1ModelActionSelector::getActionProfile() co
     return actionProfile;
 }
 
-const Bmv2V1ModelActionSelector *Bmv2V1ModelActionSelector::evaluate(const Model &model) const {
-    const auto *evaluatedProfile = actionProfile->evaluate(model);
+const Bmv2V1ModelActionSelector *Bmv2V1ModelActionSelector::evaluate(const Model &model,
+                                                                     bool doComplete) const {
+    const auto *evaluatedProfile = actionProfile->evaluate(model, doComplete);
     return new Bmv2V1ModelActionSelector(selectorDecl, evaluatedProfile);
 }
 
@@ -204,7 +208,8 @@ const ExecutionState &Bmv2V1ModelCloneInfo::getClonedState() const { return clon
 
 std::optional<int> Bmv2V1ModelCloneInfo::getPreserveIndex() const { return preserveIndex; }
 
-const Bmv2V1ModelCloneInfo *Bmv2V1ModelCloneInfo::evaluate(const Model & /*model*/) const {
+const Bmv2V1ModelCloneInfo *Bmv2V1ModelCloneInfo::evaluate(const Model & /*model*/,
+                                                           bool /*doComplete*/) const {
     P4C_UNIMPLEMENTED("Evaluate is not implemented for this test object.");
 }
 
@@ -236,8 +241,10 @@ const IR::Constant *Bmv2V1ModelCloneSpec::getEvaluatedSessionId() const {
     return constant;
 }
 
-const Bmv2V1ModelCloneSpec *Bmv2V1ModelCloneSpec::evaluate(const Model &model) const {
-    return new Bmv2V1ModelCloneSpec(model.evaluate(sessionId), model.evaluate(clonePort), isClone);
+const Bmv2V1ModelCloneSpec *Bmv2V1ModelCloneSpec::evaluate(const Model &model,
+                                                           bool doComplete) const {
+    return new Bmv2V1ModelCloneSpec(model.evaluate(sessionId, doComplete),
+                                    model.evaluate(clonePort, doComplete), isClone);
 }
 
 bool Bmv2V1ModelCloneSpec::isClonedPacket() const { return isClone; }
@@ -258,8 +265,8 @@ const IR::Constant *Optional::getEvaluatedValue() const {
     return constant;
 }
 
-const Optional *Optional::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(value);
+const Optional *Optional::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
     return new Optional(getKey(), evaluatedValue, addMatch);
 }
 
@@ -288,9 +295,9 @@ const IR::Constant *Range::getEvaluatedHigh() const {
     return constant;
 }
 
-const Range *Range::evaluate(const Model &model) const {
-    const auto *evaluatedLow = model.evaluate(low);
-    const auto *evaluatedHigh = model.evaluate(high);
+const Range *Range::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedLow = model.evaluate(low, doComplete);
+    const auto *evaluatedHigh = model.evaluate(high, doComplete);
     return new Range(getKey(), evaluatedLow, evaluatedHigh);
 }
 
@@ -302,7 +309,8 @@ MetadataCollection::MetadataCollection() = default;
 
 cstring MetadataCollection::getObjectName() const { return "MetadataCollection"; }
 
-const MetadataCollection *MetadataCollection::evaluate(const Model & /*model*/) const {
+const MetadataCollection *MetadataCollection::evaluate(const Model & /*model*/,
+                                                       bool /*completedModel*/) const {
     P4C_UNIMPLEMENTED("%1% has no implementation for \"evaluate\".", getObjectName());
 }
 
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test_spec.h b/backends/p4tools/modules/testgen/targets/bmv2/test_spec.h
index b301163bbb..a57c295db0 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/test_spec.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/test_spec.h
@@ -51,7 +51,8 @@ class IndexExpression : public TestObject {
     /// @returns the value stored in the index expression.
     [[nodiscard]] const IR::Expression *getValue() const;
 
-    [[nodiscard]] const IndexExpression *evaluate(const Model &model) const override;
+    [[nodiscard]] const IndexExpression *evaluate(const Model &model,
+                                                  bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 };
@@ -106,7 +107,8 @@ class Bmv2V1ModelRegisterValue : public IndexMap {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const Bmv2V1ModelRegisterValue *evaluate(const Model &model) const override;
+    [[nodiscard]] const Bmv2V1ModelRegisterValue *evaluate(const Model &model,
+                                                           bool doComplete) const override;
 };
 
 /* =========================================================================================
@@ -123,7 +125,8 @@ class Bmv2V1ModelMeterValue : public IndexMap {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const Bmv2V1ModelMeterValue *evaluate(const Model &model) const override;
+    [[nodiscard]] const Bmv2V1ModelMeterValue *evaluate(const Model &model,
+                                                        bool doComplete) const override;
 
     /// @returns whether the meter associated with this meter value object is a direct meter.
     [[nodiscard]] bool isDirectMeter() const;
@@ -157,7 +160,8 @@ class Bmv2V1ModelActionProfile : public TestObject {
     /// Add an action (its name) and the arguments to the action map of this profile.
     void addToActionMap(cstring actionName, std::vector<ActionArg> actionArgs);
 
-    [[nodiscard]] const Bmv2V1ModelActionProfile *evaluate(const Model &model) const override;
+    [[nodiscard]] const Bmv2V1ModelActionProfile *evaluate(const Model &model,
+                                                           bool doComplete) const override;
 };
 
 /* =========================================================================================
@@ -183,7 +187,8 @@ class Bmv2V1ModelActionSelector : public TestObject {
     /// @returns the associated action profile.
     [[nodiscard]] const Bmv2V1ModelActionProfile *getActionProfile() const;
 
-    [[nodiscard]] const Bmv2V1ModelActionSelector *evaluate(const Model &model) const override;
+    [[nodiscard]] const Bmv2V1ModelActionSelector *evaluate(const Model &model,
+                                                            bool doComplete) const override;
 };
 
 /* =========================================================================================
@@ -211,7 +216,8 @@ class Bmv2V1ModelCloneInfo : public TestObject {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const Bmv2V1ModelCloneInfo *evaluate(const Model &model) const override;
+    [[nodiscard]] const Bmv2V1ModelCloneInfo *evaluate(const Model &model,
+                                                       bool doComplete) const override;
 
     /// @returns the associated session ID with this cloned packet.
     [[nodiscard]] const IR::Expression *getSessionId() const;
@@ -247,7 +253,8 @@ class Bmv2V1ModelCloneSpec : public TestObject {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const Bmv2V1ModelCloneSpec *evaluate(const Model &model) const override;
+    [[nodiscard]] const Bmv2V1ModelCloneSpec *evaluate(const Model &model,
+                                                       bool doComplete) const override;
 
     /// @returns the associated session ID with this cloned packet.
     [[nodiscard]] const IR::Expression *getSessionId() const;
@@ -281,7 +288,8 @@ class MetadataCollection : public TestObject {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const MetadataCollection *evaluate(const Model & /*model*/) const override;
+    [[nodiscard]] const MetadataCollection *evaluate(const Model & /*model*/,
+                                                     bool doComplete) const override;
 
     /// @returns the list of metadata fields.
     [[nodiscard]] const std::map<cstring, const IR::Literal *> &getMetadataFields() const;
@@ -308,7 +316,7 @@ class Optional : public TableMatch {
  public:
     explicit Optional(const IR::KeyElement *key, const IR::Expression *value, bool addMatch);
 
-    [[nodiscard]] const Optional *evaluate(const Model &model) const override;
+    [[nodiscard]] const Optional *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
@@ -332,7 +340,7 @@ class Range : public TableMatch {
     explicit Range(const IR::KeyElement *key, const IR::Expression *low,
                    const IR::Expression *high);
 
-    [[nodiscard]] const Range *evaluate(const Model &model) const override;
+    [[nodiscard]] const Range *evaluate(const Model &model, bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.cpp b/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.cpp
index 88eee317b7..db07052915 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.cpp
@@ -13,13 +13,6 @@
 
 namespace P4Tools::P4Testgen::EBPF {
 
-const IR::Expression *EBPFTableStepper::computeTargetMatchType(
-    ExecutionState &nextState, const TableUtils::KeyProperties &keyProperties,
-    TableMatchMap *matches, const IR::Expression *hitCondition) {
-    // If the custom match type does not match, delete to the core match types.
-    return TableStepper::computeTargetMatchType(nextState, keyProperties, matches, hitCondition);
-}
-
 void EBPFTableStepper::checkTargetProperties(
     const std::vector<const IR::ActionListElement *> & /*tableActionList*/) {
     // Iterate over the table keys and check whether we can mitigate taint.
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.h b/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.h
index 17b842f225..f9635e118a 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.h
+++ b/backends/p4tools/modules/testgen/targets/ebpf/table_stepper.h
@@ -28,11 +28,6 @@ class EBPFTableStepper : public TableStepper {
     } EBPFProperties;
 
  protected:
-    const IR::Expression *computeTargetMatchType(ExecutionState &nextState,
-                                                 const TableUtils::KeyProperties &keyProperties,
-                                                 TableMatchMap *matches,
-                                                 const IR::Expression *hitCondition) override;
-
     void checkTargetProperties(
         const std::vector<const IR::ActionListElement *> &tableActionList) override;
 
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/test/P4Tests.cmake b/backends/p4tools/modules/testgen/targets/ebpf/test/P4Tests.cmake
index 7f3ec329e9..44c28cd6e0 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/test/P4Tests.cmake
+++ b/backends/p4tools/modules/testgen/targets/ebpf/test/P4Tests.cmake
@@ -6,7 +6,6 @@ include(${CMAKE_CURRENT_LIST_DIR}/TestTemplate.cmake)
 # ##################################################################################################
 # TEST PROGRAMS
 # ##################################################################################################
-set(P4TESTGEN_EBPF_EXCLUDES "ebpf_checksum_extern\\.p4" "ebpf_conntrack_extern\\.p4")
 
 set(EBPF_SEARCH_PATTERNS "include.*ebpf_model.p4")
 set(P4TESTS_FOR_EBPF "${P4C_SOURCE_DIR}/testdata/p4_16_samples/*.p4")
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp b/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp
index 1c6ae380db..c4e751f20c 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp
@@ -55,10 +55,10 @@ EBPFTestBackend::EBPFTestBackend(const ProgramInfo &programInfo, SymbolicExecuto
 }
 
 TestBackEnd::TestInfo EBPFTestBackend::produceTestInfo(
-    const ExecutionState *executionState, const Model *completedModel,
+    const ExecutionState *executionState, const Model *finalModel,
     const IR::Expression *outputPacketExpr, const IR::Expression *outputPortExpr,
     const std::vector<std::reference_wrapper<const TraceEvent>> *programTraces) {
-    auto testInfo = TestBackEnd::produceTestInfo(executionState, completedModel, outputPacketExpr,
+    auto testInfo = TestBackEnd::produceTestInfo(executionState, finalModel, outputPacketExpr,
                                                  outputPortExpr, programTraces);
     // This is a hack to deal with an virtual kernel interface quirk.
     // Packets that are too small are truncated to 02000000 (in hex) with width 32 bit.
@@ -78,8 +78,7 @@ TestBackEnd::TestInfo EBPFTestBackend::produceTestInfo(
 }
 
 const TestSpec *EBPFTestBackend::createTestSpec(const ExecutionState *executionState,
-                                                const Model *completedModel,
-                                                const TestInfo &testInfo) {
+                                                const Model *finalModel, const TestInfo &testInfo) {
     // Create a testSpec.
     TestSpec *testSpec = nullptr;
 
@@ -99,7 +98,7 @@ const TestSpec *EBPFTestBackend::createTestSpec(const ExecutionState *executionS
     for (const auto &tablePair : uninterpretedTableConfigs) {
         const auto tableName = tablePair.first;
         const auto *uninterpretedTableConfig = tablePair.second->checkedTo<TableConfig>();
-        const auto *const tableConfig = uninterpretedTableConfig->evaluate(*completedModel);
+        const auto *const tableConfig = uninterpretedTableConfig->evaluate(*finalModel, true);
         testSpec->addTestObject("tables", tableName, tableConfig);
     }
     return testSpec;
diff --git a/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.cpp b/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.cpp
index e31e917664..ec8a71bf90 100644
--- a/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.cpp
@@ -6,14 +6,6 @@
 
 namespace P4Tools::P4Testgen::Pna {
 
-const IR::Expression *PnaDpdkTableStepper::computeTargetMatchType(
-    ExecutionState &nextState, const TableUtils::KeyProperties &keyProperties,
-    TableMatchMap *matches, const IR::Expression *hitCondition) {
-    // If the custom match type does not match, delete to the core match types.
-    return SharedPnaTableStepper::computeTargetMatchType(nextState, keyProperties, matches,
-                                                         hitCondition);
-}
-
 PnaDpdkTableStepper::PnaDpdkTableStepper(PnaDpdkExprStepper *stepper, const IR::P4Table *table)
     : SharedPnaTableStepper(stepper, table) {}
 
diff --git a/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.h b/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.h
index d745e069cb..c5ffec330a 100644
--- a/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.h
+++ b/backends/p4tools/modules/testgen/targets/pna/dpdk/table_stepper.h
@@ -11,12 +11,6 @@
 namespace P4Tools::P4Testgen::Pna {
 
 class PnaDpdkTableStepper : public SharedPnaTableStepper {
- protected:
-    const IR::Expression *computeTargetMatchType(ExecutionState &nextState,
-                                                 const TableUtils::KeyProperties &keyProperties,
-                                                 TableMatchMap *matches,
-                                                 const IR::Expression *hitCondition) override;
-
  public:
     explicit PnaDpdkTableStepper(PnaDpdkExprStepper *stepper, const IR::P4Table *table);
 };
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 3e1a2f9e36..ec63d584fc 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
@@ -9,6 +9,7 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/lib/trace_event_types.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/declaration.h"
 #include "ir/id.h"
 #include "ir/irutils.h"
@@ -36,8 +37,8 @@
 namespace P4Tools::P4Testgen::Pna {
 
 const IR::Expression *SharedPnaTableStepper::computeTargetMatchType(
-    ExecutionState &nextState, const TableUtils::KeyProperties &keyProperties,
-    TableMatchMap *matches, const IR::Expression *hitCondition) {
+    const TableUtils::KeyProperties &keyProperties, TableMatchMap *matches,
+    const IR::Expression *hitCondition) {
     const IR::Expression *keyExpr = keyProperties.key->expression;
 
     // TODO: We consider optional match types to be a no-op, but we could make them exact matches.
@@ -45,7 +46,7 @@ const IR::Expression *SharedPnaTableStepper::computeTargetMatchType(
         // We can recover from taint by simply not adding the optional match.
         // Create a new symbolic variable that corresponds to the key expression.
         cstring keyName = properties.tableName + "_key_" + keyProperties.name;
-        const auto *ctrlPlaneKey = nextState.createSymbolicVariable(keyExpr->type, keyName);
+        const auto *ctrlPlaneKey = ToolsVariables::getSymbolicVariable(keyExpr->type, keyName);
         if (keyProperties.isTainted) {
             matches->emplace(keyProperties.name,
                              new Optional(keyProperties.key, ctrlPlaneKey, false));
@@ -75,8 +76,8 @@ const IR::Expression *SharedPnaTableStepper::computeTargetMatchType(
             maxKey = IR::getConstant(keyExpr->type, IR::getMaxBvVal(keyExpr->type));
             keyExpr = minKey;
         } else {
-            minKey = nextState.createSymbolicVariable(keyExpr->type, minName);
-            maxKey = nextState.createSymbolicVariable(keyExpr->type, maxName);
+            minKey = ToolsVariables::getSymbolicVariable(keyExpr->type, minName);
+            maxKey = ToolsVariables::getSymbolicVariable(keyExpr->type, maxName);
         }
         matches->emplace(keyProperties.name, new Range(keyProperties.key, minKey, maxKey));
         return new IR::LAnd(hitCondition, new IR::LAnd(new IR::LAnd(new IR::Lss(minKey, maxKey),
@@ -84,13 +85,18 @@ const IR::Expression *SharedPnaTableStepper::computeTargetMatchType(
                                                        new IR::Leq(keyExpr, maxKey)));
     }
     // If the custom match type does not match, delete to the core match types.
-    return TableStepper::computeTargetMatchType(nextState, keyProperties, matches, hitCondition);
+    return TableStepper::computeTargetMatchType(keyProperties, matches, hitCondition);
 }
 
 void SharedPnaTableStepper::evalTableActionProfile(
     const std::vector<const IR::ActionListElement *> &tableActionList) {
     const auto *state = getExecutionState();
 
+    // First, we compute the hit condition to trigger this particular action call.
+    TableMatchMap matches;
+    const auto *hitCondition = computeHit(&matches);
+
+    // Now we iterate over all table actions and create a path per table action.
     for (const auto *action : tableActionList) {
         // Grab the path from the method call.
         const auto *tableAction = action->expression->checkedTo<IR::MethodCallExpression>();
@@ -113,7 +119,7 @@ void SharedPnaTableStepper::evalTableActionProfile(
             // Getting the unique name is needed to avoid generating duplicate arguments.
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
+            const auto &actionArg = ToolsVariables::getSymbolicVariable(parameter->type, keyName);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
             // Note how we use the control plane name for the parameter here.
@@ -129,10 +135,6 @@ void SharedPnaTableStepper::evalTableActionProfile(
         auto *synthesizedAction = tableAction->clone();
         synthesizedAction->arguments = arguments;
 
-        // Now we compute the hit condition to trigger this particular action call.
-        TableMatchMap matches;
-        const auto *hitCondition = computeHit(nextState, &matches);
-
         // We need to set the table action in the state for eventual switch action_run hits.
         // We also will need it for control plane table entries.
         setTableAction(nextState, tableAction);
@@ -175,6 +177,11 @@ void SharedPnaTableStepper::evalTableActionSelector(
     const std::vector<const IR::ActionListElement *> &tableActionList) {
     const auto *state = getExecutionState();
 
+    // First, we compute the hit condition to trigger this particular action call.
+    TableMatchMap matches;
+    const auto *hitCondition = computeHit(&matches);
+
+    // Now we iterate over all table actions and create a path per table action.
     for (const auto *action : tableActionList) {
         // Grab the path from the method call.
         const auto *tableAction = action->expression->checkedTo<IR::MethodCallExpression>();
@@ -199,7 +206,7 @@ void SharedPnaTableStepper::evalTableActionSelector(
             // Getting the unique name is needed to avoid generating duplicate arguments.
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
+            const auto &actionArg = ToolsVariables::getSymbolicVariable(parameter->type, keyName);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
             // Note how we use the control plane name for the parameter here.
@@ -221,10 +228,6 @@ void SharedPnaTableStepper::evalTableActionSelector(
         auto *synthesizedAction = tableAction->clone();
         synthesizedAction->arguments = arguments;
 
-        // Now we compute the hit condition to trigger this particular action call.
-        TableMatchMap matches;
-        const auto *hitCondition = computeHit(nextState, &matches);
-
         // We need to set the table action in the state for eventual switch action_run hits.
         // We also will need it for control plane table entries.
         setTableAction(nextState, tableAction);
diff --git a/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.h b/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.h
index abcfd3dba2..2e74aeba8e 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.h
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.h
@@ -55,8 +55,7 @@ class SharedPnaTableStepper : public TableStepper {
         TableImplementation implementaton = TableImplementation::standard;
     } SharedPnaProperties;
 
-    const IR::Expression *computeTargetMatchType(ExecutionState &nextState,
-                                                 const TableUtils::KeyProperties &keyProperties,
+    const IR::Expression *computeTargetMatchType(const TableUtils::KeyProperties &keyProperties,
                                                  TableMatchMap *matches,
                                                  const IR::Expression *hitCondition) override;
 
diff --git a/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp b/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp
index fbcf3ef22a..1d42649466 100644
--- a/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp
@@ -52,17 +52,16 @@ PnaTestBackend::PnaTestBackend(const ProgramInfo &programInfo, SymbolicExecutor
 }
 
 TestBackEnd::TestInfo PnaTestBackend::produceTestInfo(
-    const ExecutionState *executionState, const Model *completedModel,
+    const ExecutionState *executionState, const Model *finalModel,
     const IR::Expression *outputPacketExpr, const IR::Expression *outputPortExpr,
     const std::vector<std::reference_wrapper<const TraceEvent>> *programTraces) {
-    auto testInfo = TestBackEnd::produceTestInfo(executionState, completedModel, outputPacketExpr,
+    auto testInfo = TestBackEnd::produceTestInfo(executionState, finalModel, outputPacketExpr,
                                                  outputPortExpr, programTraces);
     return testInfo;
 }
 
 const TestSpec *PnaTestBackend::createTestSpec(const ExecutionState *executionState,
-                                               const Model *completedModel,
-                                               const TestInfo &testInfo) {
+                                               const Model *finalModel, const TestInfo &testInfo) {
     // Create a testSpec.
     TestSpec *testSpec = nullptr;
 
@@ -86,7 +85,7 @@ const TestSpec *PnaTestBackend::createTestSpec(const ExecutionState *executionSt
         const auto &flatFields = executionState->getFlatFields(
             localMetadataVar, localMetadataType->checkedTo<IR::Type_Struct>(), {});
         for (const auto &fieldRef : flatFields) {
-            const auto *fieldVal = completedModel->evaluate(executionState->get(fieldRef));
+            const auto *fieldVal = finalModel->evaluate(executionState->get(fieldRef), true);
             // Try to remove the leading internal name for the metadata field.
             // Thankfully, this string manipulation is safe if we are out of range.
             auto fieldString = fieldRef->toString();
@@ -104,7 +103,7 @@ const TestSpec *PnaTestBackend::createTestSpec(const ExecutionState *executionSt
     for (const auto &tablePair : uninterpretedTableConfigs) {
         const auto tableName = tablePair.first;
         const auto *uninterpretedTableConfig = tablePair.second->checkedTo<TableConfig>();
-        const auto *const tableConfig = uninterpretedTableConfig->evaluate(*completedModel);
+        const auto *const tableConfig = uninterpretedTableConfig->evaluate(*finalModel, true);
         testSpec->addTestObject("tables", tableName, tableConfig);
     }
 
@@ -112,7 +111,7 @@ const TestSpec *PnaTestBackend::createTestSpec(const ExecutionState *executionSt
     for (const auto &testObject : actionProfiles) {
         const auto profileName = testObject.first;
         const auto *actionProfile = testObject.second->checkedTo<PnaDpdkActionProfile>();
-        const auto *evaluatedProfile = actionProfile->evaluate(*completedModel);
+        const auto *evaluatedProfile = actionProfile->evaluate(*finalModel, true);
         testSpec->addTestObject("action_profiles", profileName, evaluatedProfile);
     }
 
@@ -120,7 +119,7 @@ const TestSpec *PnaTestBackend::createTestSpec(const ExecutionState *executionSt
     for (const auto &testObject : actionSelectors) {
         const auto selectorName = testObject.first;
         const auto *actionSelector = testObject.second->checkedTo<PnaDpdkActionSelector>();
-        const auto *evaluatedSelector = actionSelector->evaluate(*completedModel);
+        const auto *evaluatedSelector = actionSelector->evaluate(*finalModel, true);
         testSpec->addTestObject("action_selectors", selectorName, evaluatedSelector);
     }
 
diff --git a/backends/p4tools/modules/testgen/targets/pna/test_spec.cpp b/backends/p4tools/modules/testgen/targets/pna/test_spec.cpp
index c025bc4553..f9cda0b0e7 100644
--- a/backends/p4tools/modules/testgen/targets/pna/test_spec.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/test_spec.cpp
@@ -24,9 +24,9 @@ cstring PnaDpdkRegisterValue::getObjectName() const { return "PnaDpdkRegisterVal
 
 const IR::Expression *PnaDpdkRegisterValue::getCurrentValue(const IR::Expression *index) const {
     const IR::Expression *baseExpr = initialValue;
-    for (const auto &PnaDpdkregisterValue : registerConditions) {
-        const auto *storedIndex = PnaDpdkregisterValue.index;
-        const auto *storedVal = PnaDpdkregisterValue.value;
+    for (const auto &pnaDpdkregisterValue : registerConditions) {
+        const auto *storedIndex = pnaDpdkregisterValue.index;
+        const auto *storedVal = pnaDpdkregisterValue.value;
         baseExpr =
             new IR::Mux(baseExpr->type, new IR::Equ(storedIndex, index), storedVal, baseExpr);
     }
@@ -40,12 +40,13 @@ const IR::Constant *PnaDpdkRegisterValue::getEvaluatedValue() const {
     return constant;
 }
 
-const PnaDpdkRegisterValue *PnaDpdkRegisterValue::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(initialValue);
+const PnaDpdkRegisterValue *PnaDpdkRegisterValue::evaluate(const Model &model,
+                                                           bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(initialValue, doComplete);
     auto *evaluatedRegisterValue = new PnaDpdkRegisterValue(evaluatedValue);
     const std::vector<ActionArg> evaluatedConditions;
     for (const auto &cond : registerConditions) {
-        evaluatedRegisterValue->addRegisterCondition(*cond.evaluate(model));
+        evaluatedRegisterValue->addRegisterCondition(*cond.evaluate(model, doComplete));
     }
     return evaluatedRegisterValue;
 }
@@ -68,9 +69,10 @@ const IR::Constant *PnaDpdkRegisterCondition::getEvaluatedIndex() const {
     return constant;
 }
 
-const PnaDpdkRegisterCondition *PnaDpdkRegisterCondition::evaluate(const Model &model) const {
-    const auto *evaluatedIndex = model.evaluate(index);
-    const auto *evaluatedValue = model.evaluate(value);
+const PnaDpdkRegisterCondition *PnaDpdkRegisterCondition::evaluate(const Model &model,
+                                                                   bool doComplete) const {
+    const auto *evaluatedIndex = model.evaluate(index, doComplete);
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
     return new PnaDpdkRegisterCondition(evaluatedIndex, evaluatedValue);
 }
 
@@ -97,14 +99,15 @@ void PnaDpdkActionProfile::addToActionMap(cstring actionName, std::vector<Action
 }
 size_t PnaDpdkActionProfile::getActionMapSize() const { return actions.size(); }
 
-const PnaDpdkActionProfile *PnaDpdkActionProfile::evaluate(const Model &model) const {
+const PnaDpdkActionProfile *PnaDpdkActionProfile::evaluate(const Model &model,
+                                                           bool doComplete) const {
     auto *profile = new PnaDpdkActionProfile(profileDecl);
     for (const auto &actionTuple : actions) {
         auto actionArgs = actionTuple.second;
         std::vector<ActionArg> evaluatedArgs;
         evaluatedArgs.reserve(actionArgs.size());
         for (const auto &actionArg : actionArgs) {
-            evaluatedArgs.emplace_back(*actionArg.evaluate(model));
+            evaluatedArgs.emplace_back(*actionArg.evaluate(model, doComplete));
         }
         profile->addToActionMap(actionTuple.first, evaluatedArgs);
     }
@@ -127,8 +130,9 @@ const PnaDpdkActionProfile *PnaDpdkActionSelector::getActionProfile() const {
     return actionProfile;
 }
 
-const PnaDpdkActionSelector *PnaDpdkActionSelector::evaluate(const Model &model) const {
-    const auto *evaluatedProfile = actionProfile->evaluate(model);
+const PnaDpdkActionSelector *PnaDpdkActionSelector::evaluate(const Model &model,
+                                                             bool doComplete) const {
+    const auto *evaluatedProfile = actionProfile->evaluate(model, doComplete);
     return new PnaDpdkActionSelector(selectorDecl, evaluatedProfile);
 }
 
@@ -148,8 +152,8 @@ const IR::Constant *Optional::getEvaluatedValue() const {
     return constant;
 }
 
-const Optional *Optional::evaluate(const Model &model) const {
-    const auto *evaluatedValue = model.evaluate(value);
+const Optional *Optional::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedValue = model.evaluate(value, doComplete);
     return new Optional(getKey(), evaluatedValue, addMatch);
 }
 
@@ -178,9 +182,9 @@ const IR::Constant *Range::getEvaluatedHigh() const {
     return constant;
 }
 
-const Range *Range::evaluate(const Model &model) const {
-    const auto *evaluatedLow = model.evaluate(low);
-    const auto *evaluatedHigh = model.evaluate(high);
+const Range *Range::evaluate(const Model &model, bool doComplete) const {
+    const auto *evaluatedLow = model.evaluate(low, doComplete);
+    const auto *evaluatedHigh = model.evaluate(high, doComplete);
     return new Range(getKey(), evaluatedLow, evaluatedHigh);
 }
 
@@ -192,7 +196,8 @@ MetadataCollection::MetadataCollection() = default;
 
 cstring MetadataCollection::getObjectName() const { return "MetadataCollection"; }
 
-const MetadataCollection *MetadataCollection::evaluate(const Model & /*model*/) const {
+const MetadataCollection *MetadataCollection::evaluate(const Model & /*model*/,
+                                                       bool /*completedModel*/) const {
     P4C_UNIMPLEMENTED("%1% has no implementation for \"evaluate\".", getObjectName());
 }
 
diff --git a/backends/p4tools/modules/testgen/targets/pna/test_spec.h b/backends/p4tools/modules/testgen/targets/pna/test_spec.h
index 63175abb72..871951b337 100644
--- a/backends/p4tools/modules/testgen/targets/pna/test_spec.h
+++ b/backends/p4tools/modules/testgen/targets/pna/test_spec.h
@@ -38,7 +38,8 @@ class PnaDpdkRegisterCondition : public TestObject {
     /// The function will throw a bug if this is not the case.
     [[nodiscard]] const IR::Constant *getEvaluatedValue() const;
 
-    [[nodiscard]] const PnaDpdkRegisterCondition *evaluate(const Model &model) const override;
+    [[nodiscard]] const PnaDpdkRegisterCondition *evaluate(const Model &model,
+                                                           bool doComplete) const override;
 
     [[nodiscard]] cstring getObjectName() const override;
 };
@@ -79,7 +80,8 @@ class PnaDpdkRegisterValue : public TestObject {
     /// The function will throw a bug if this is not the case.
     [[nodiscard]] const IR::Constant *getEvaluatedValue() const;
 
-    [[nodiscard]] const PnaDpdkRegisterValue *evaluate(const Model &model) const override;
+    [[nodiscard]] const PnaDpdkRegisterValue *evaluate(const Model &model,
+                                                       bool doComplete) const override;
 };
 
 /* =========================================================================================
@@ -110,7 +112,8 @@ class PnaDpdkActionProfile : public TestObject {
     /// Add an action (its name) and the arguments to the action map of this profile.
     void addToActionMap(cstring actionName, std::vector<ActionArg> actionArgs);
 
-    [[nodiscard]] const PnaDpdkActionProfile *evaluate(const Model &model) const override;
+    [[nodiscard]] const PnaDpdkActionProfile *evaluate(const Model &model,
+                                                       bool doComplete) const override;
 };
 
 /* =========================================================================================
@@ -136,7 +139,8 @@ class PnaDpdkActionSelector : public TestObject {
     /// @returns the associated action profile.
     [[nodiscard]] const PnaDpdkActionProfile *getActionProfile() const;
 
-    [[nodiscard]] const PnaDpdkActionSelector *evaluate(const Model &model) const override;
+    [[nodiscard]] const PnaDpdkActionSelector *evaluate(const Model &model,
+                                                        bool doComplete) const override;
 };
 
 /* =========================================================================================
@@ -151,7 +155,8 @@ class MetadataCollection : public TestObject {
 
     [[nodiscard]] cstring getObjectName() const override;
 
-    [[nodiscard]] const MetadataCollection *evaluate(const Model & /*model*/) const override;
+    [[nodiscard]] const MetadataCollection *evaluate(const Model & /*model*/,
+                                                     bool doComplete) const override;
 
     /// @returns the clone port expression.
     [[nodiscard]] const std::map<cstring, const IR::Literal *> &getMetadataFields() const;
@@ -176,7 +181,7 @@ class Optional : public TableMatch {
  public:
     explicit Optional(const IR::KeyElement *key, const IR::Expression *value, bool addMatch);
 
-    const Optional *evaluate(const Model &model) const override;
+    const Optional *evaluate(const Model &model, bool doComplete) const override;
 
     cstring getObjectName() const override;
 
@@ -200,7 +205,7 @@ class Range : public TableMatch {
     explicit Range(const IR::KeyElement *key, const IR::Expression *low,
                    const IR::Expression *high);
 
-    const Range *evaluate(const Model &model) const override;
+    const Range *evaluate(const Model &model, bool doComplete) const override;
 
     cstring getObjectName() const override;
 
diff --git a/backends/p4tools/modules/testgen/test/gtest_utils.cpp b/backends/p4tools/modules/testgen/test/gtest_utils.cpp
index 5600a570a6..e943ced19d 100644
--- a/backends/p4tools/modules/testgen/test/gtest_utils.cpp
+++ b/backends/p4tools/modules/testgen/test/gtest_utils.cpp
@@ -59,7 +59,7 @@ void P4ToolsTestCase::ensureInit() {
 }
 
 const IR::SymbolicVariable *SymbolicConverter::preorder(IR::Member *member) {
-    return P4Tools::ToolsVariables::getSymbolicVariable(member->type, 0, member->toString());
+    return P4Tools::ToolsVariables::getSymbolicVariable(member->type, member->toString());
 }
 
 }  // namespace Test
diff --git a/backends/p4tools/modules/testgen/test/small-step/p4_asserts_parser_test.cpp b/backends/p4tools/modules/testgen/test/small-step/p4_asserts_parser_test.cpp
index 13c91c6fda..76ad48ae13 100644
--- a/backends/p4tools/modules/testgen/test/small-step/p4_asserts_parser_test.cpp
+++ b/backends/p4tools/modules/testgen/test/small-step/p4_asserts_parser_test.cpp
@@ -101,9 +101,9 @@ TEST_F(P4AssertsParserTest, Restrictions) {
     ASSERT_EQ(parsingResult.size(), (unsigned long)1);
     {
         const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
-            IR::Type_Bits::get(8), 0, "ingress.ternary_table_mask_h.h.a1");
+            IR::Type_Bits::get(8), "ingress.ternary_table_mask_h.h.a1");
         const auto &expr2 = P4Tools::ToolsVariables::getSymbolicVariable(
-            IR::Type_Bits::get(8), 0, "ingress.ternary_table_lpm_prefix_h.h.a1");
+            IR::Type_Bits::get(8), "ingress.ternary_table_lpm_prefix_h.h.a1");
         const auto *const1 = IR::getConstant(IR::Type_Bits::get(8), 0);
         const auto *const2 = IR::getConstant(IR::Type_Bits::get(8), 64);
         const auto *operation =
@@ -112,14 +112,14 @@ TEST_F(P4AssertsParserTest, Restrictions) {
     }
     {
         const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
-            IR::Type_Bits::get(8), 0, "ingress.ternary_table_key_h.h.a1");
+            IR::Type_Bits::get(8), "ingress.ternary_table_key_h.h.a1");
         const auto *const1 = IR::getConstant(IR::Type_Bits::get(8), 0);
         const auto *operation1 = new IR::Neq(expr1, const1);
         ASSERT_TRUE(parsingResult[0][1]->equiv(*operation1));
     }
     {
         const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
-            IR::Type_Bits::get(8), 0, "ingress.ternary_table_key_h.h.a");
+            IR::Type_Bits::get(8), "ingress.ternary_table_key_h.h.a");
         const auto *const2 = IR::getConstant(IR::Type_Bits::get(8), 255);
         const auto *operation2 = new IR::Neq(expr1, const2);
         ASSERT_TRUE(parsingResult[0][2]->equiv(*operation2));
@@ -131,9 +131,9 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInTable) {
         "backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4",
         false);
     ASSERT_EQ(parsingResult.size(), (unsigned long)3);
-    const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), 0,
+    const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8),
                                                                      "ingress.table_1_key_h.h.a");
-    const auto &expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), 0,
+    const auto &expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8),
                                                                      "ingress.table_2_key_h.h.b");
     const auto *operation = new IR::Equ(expr1, expr2);
     ASSERT_TRUE(parsingResult[0][0]->equiv(*operation));
@@ -144,11 +144,11 @@ TEST_F(P4AssertsParserTest, RestrictionMiddleblockReferToInAction) {
         "backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_restrictions_2.p4",
         false);
     ASSERT_EQ(parsingResult.size(), (unsigned long)3);
-    auto expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
-        IR::Type_Bits::get(8), 0, "ingress.table_1_arg_ingress.MyAction10");
-    auto expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), 0,
-                                                              "ingress.table_1_key_h.h.a");
-    auto operation = new IR::Equ(expr1, expr2);
+    const auto *expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
+        IR::Type_Bits::get(8), "ingress.table_1_arg_ingress.MyAction10");
+    const auto *expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8),
+                                                                     "ingress.table_1_key_h.h.a");
+    auto *operation = new IR::Equ(expr1, expr2);
     ASSERT_TRUE(parsingResult[1][0]->equiv(*operation));
 }
 
diff --git a/backends/p4tools/modules/testgen/test/small-step/util.h b/backends/p4tools/modules/testgen/test/small-step/util.h
index 419431c247..1362cc1edf 100644
--- a/backends/p4tools/modules/testgen/test/small-step/util.h
+++ b/backends/p4tools/modules/testgen/test/small-step/util.h
@@ -156,11 +156,11 @@ void stepAndExamineOp(
     // Examine the resulting stack.
     ASSERT_EQ(executionState.get().getStack().size(), 1u);
     const auto stackFrame = executionState.get().getStack().top();
-    ASSERT_TRUE(stackFrame.get().exceptionHandlers.empty());
-    ASSERT_EQ(stackFrame.get().namespaces, NamespaceContext::Empty);
+    ASSERT_TRUE(stackFrame.get().getExceptionHandlers().empty());
+    ASSERT_EQ(stackFrame.get().getNameSpaces(), NamespaceContext::Empty);
 
     // Examine the pushed continuation.
-    Continuation pushedContinuation = stackFrame.get().normalContinuation;
+    Continuation pushedContinuation = stackFrame.get().getContinuation();
     ASSERT_TRUE(pushedContinuation.parameterOpt);
     Body pushedBody = pushedContinuation.body;
     ASSERT_EQ(pushedBody, Body({Return(rebuildNode(*pushedContinuation.parameterOpt))}));