From 06f520f4200827381d546c7123b3778468fcf6c4 Mon Sep 17 00:00:00 2001
From: Fabian Ruffy <5960321+fruffy@users.noreply.github.com>
Date: Fri, 28 Apr 2023 11:12:03 -0400
Subject: [PATCH] Split state variables and symbolic variables. Stricter type
 checking. (#3987)

* Split state variables and symbolic variables. Stricter type checking.

* Rename variables appropriately.

* IWYU.

* Refactor the concolic execution model. Push concolic refresh into final state.

* Fix up gtests.

* Remove flawed test.

* Move packet variables out of the execution state.

* State variables never used the incarnation count. Remove.

* There is no need to look up the declaration in convertPathExpr.
---
 backends/p4tools/common/CMakeLists.txt        |   2 +-
 .../common/compiler/convert_hs_index.h        |   2 +-
 backends/p4tools/common/core/solver.h         |  23 ++-
 backends/p4tools/common/core/z3_solver.cpp    |  57 +++-----
 backends/p4tools/common/core/z3_solver.h      |  31 ++--
 backends/p4tools/common/lib/format_int.cpp    |   1 -
 backends/p4tools/common/lib/model.cpp         |  91 +++++-------
 backends/p4tools/common/lib/model.h           |  57 +++++++-
 backends/p4tools/common/lib/symbolic_env.cpp  |  11 +-
 backends/p4tools/common/lib/taint.cpp         |  41 ++----
 .../p4tools/common/lib/trace_event_types.cpp  |   1 -
 .../p4tools/common/lib/trace_event_types.h    |   2 +
 backends/p4tools/common/lib/util.cpp          |  73 +---------
 backends/p4tools/common/lib/util.h            |  46 +-----
 backends/p4tools/common/lib/variables.cpp     |  61 ++++++++
 backends/p4tools/common/lib/variables.h       |  55 +++++++
 backends/p4tools/common/lib/zombie.cpp        |  66 ---------
 backends/p4tools/common/lib/zombie.h          |  48 -------
 .../p4tools/modules/testgen/CMakeLists.txt    |   1 +
 .../modules/testgen/core/program_info.cpp     |  12 +-
 .../modules/testgen/core/program_info.h       |   7 +-
 .../core/small_step/abstract_stepper.cpp      |  21 +--
 .../testgen/core/small_step/cmd_stepper.cpp   |  15 +-
 .../testgen/core/small_step/cmd_stepper.h     |   2 +-
 .../testgen/core/small_step/expr_stepper.cpp  |   6 +-
 .../testgen/core/small_step/expr_stepper.h    |   5 +-
 .../core/small_step/extern_stepper.cpp        |  15 +-
 .../testgen/core/small_step/table_stepper.cpp |  49 +++++--
 .../testgen/core/small_step/table_stepper.h   |  10 +-
 .../p4tools/modules/testgen/core/target.cpp   |   1 -
 .../p4tools/modules/testgen/core/target.h     |   1 -
 .../p4tools/modules/testgen/lib/concolic.cpp  |  19 ++-
 .../p4tools/modules/testgen/lib/concolic.h    |  17 ++-
 .../modules/testgen/lib/execution_state.cpp   | 134 +++++++-----------
 .../modules/testgen/lib/execution_state.h     |  72 ++++------
 .../modules/testgen/lib/final_state.cpp       | 108 ++++++++++++--
 .../p4tools/modules/testgen/lib/final_state.h |  31 +++-
 .../modules/testgen/lib/packet_vars.cpp       |  22 +++
 .../p4tools/modules/testgen/lib/packet_vars.h |  38 +++++
 .../modules/testgen/lib/test_backend.cpp      | 120 +++++-----------
 .../modules/testgen/lib/test_backend.h        |   8 +-
 backends/p4tools/modules/testgen/lib/tf.h     |   1 +
 backends/p4tools/modules/testgen/main.cpp     |   4 +
 .../bmv2/backend/metadata/metadata.cpp        |   1 +
 .../targets/bmv2/backend/metadata/metadata.h  |   1 +
 .../bmv2/backend/protobuf/protobuf.cpp        |   1 +
 .../targets/bmv2/backend/protobuf/protobuf.h  |   2 +-
 .../testgen/targets/bmv2/backend/ptf/ptf.h    |   1 +
 .../testgen/targets/bmv2/backend/stf/stf.cpp  |   1 +
 .../testgen/targets/bmv2/backend/stf/stf.h    |   2 +-
 .../testgen/targets/bmv2/cmd_stepper.cpp      |   5 +-
 .../modules/testgen/targets/bmv2/concolic.cpp |  53 ++-----
 .../testgen/targets/bmv2/expr_stepper.cpp     |  22 +--
 .../targets/bmv2/p4_asserts_parser.cpp        |  20 ++-
 .../targets/bmv2/p4_refers_to_parser.cpp      |  10 +-
 .../targets/bmv2/p4_refers_to_parser.h        |   2 +-
 .../testgen/targets/bmv2/program_info.cpp     |  29 ++--
 .../testgen/targets/bmv2/program_info.h       |   9 +-
 .../testgen/targets/bmv2/table_stepper.cpp    |  21 ++-
 .../modules/testgen/targets/bmv2/target.cpp   |   1 -
 .../testgen/targets/bmv2/test/P4Tests.cmake   |   8 +-
 .../testgen/targets/ebpf/backend/stf/stf.cpp  |   1 +
 .../testgen/targets/ebpf/backend/stf/stf.h    |   2 +-
 .../testgen/targets/ebpf/expr_stepper.cpp     |   4 +-
 .../testgen/targets/ebpf/program_info.cpp     |  25 ++--
 .../testgen/targets/ebpf/program_info.h       |   7 +-
 .../modules/testgen/targets/ebpf/target.cpp   |   1 -
 .../targets/pna/backend/metadata/metadata.cpp |   1 +
 .../targets/pna/backend/metadata/metadata.h   |   1 +
 .../modules/testgen/targets/pna/constants.cpp |   9 +-
 .../modules/testgen/targets/pna/constants.h   |   6 +-
 .../testgen/targets/pna/dpdk/cmd_stepper.cpp  |   6 +-
 .../targets/pna/shared_expr_stepper.cpp       |   4 +-
 .../targets/pna/shared_program_info.cpp       |  20 +--
 .../testgen/targets/pna/shared_program_info.h |   7 +-
 .../targets/pna/shared_table_stepper.cpp      |  21 ++-
 .../modules/testgen/targets/pna/target.cpp    |   1 -
 .../modules/testgen/test/gtest_utils.cpp      |   4 +
 .../modules/testgen/test/gtest_utils.h        |   7 +
 .../modules/testgen/test/lib/taint.cpp        |  28 ++--
 .../small-step/p4_asserts_parser_test.cpp     |  32 ++---
 .../transformations/saturation_arithm.cpp     |  12 +-
 .../testgen/test/z3-solver/asrt_model.cpp     |  44 +++---
 .../testgen/test/z3-solver/expressions.cpp    |  14 +-
 backends/p4tools/p4tools.def                  |  83 ++++++++---
 ir/ir.def                                     |   4 +-
 86 files changed, 959 insertions(+), 961 deletions(-)
 create mode 100644 backends/p4tools/common/lib/variables.cpp
 create mode 100644 backends/p4tools/common/lib/variables.h
 delete mode 100644 backends/p4tools/common/lib/zombie.cpp
 delete mode 100644 backends/p4tools/common/lib/zombie.h
 create mode 100644 backends/p4tools/modules/testgen/lib/packet_vars.cpp
 create mode 100644 backends/p4tools/modules/testgen/lib/packet_vars.h

diff --git a/backends/p4tools/common/CMakeLists.txt b/backends/p4tools/common/CMakeLists.txt
index 8baf940e781..c9ae2ed00c0 100644
--- a/backends/p4tools/common/CMakeLists.txt
+++ b/backends/p4tools/common/CMakeLists.txt
@@ -43,7 +43,7 @@ set(
   lib/trace_event.cpp
   lib/trace_event_types.cpp
   lib/util.cpp
-  lib/zombie.cpp
+  lib/variables.cpp
 )
 
 add_p4tools_library(p4tools-common ${P4C_TOOLS_COMMON_SOURCES})
diff --git a/backends/p4tools/common/compiler/convert_hs_index.h b/backends/p4tools/common/compiler/convert_hs_index.h
index 3a1dbabf4b5..98cf96e7432 100644
--- a/backends/p4tools/common/compiler/convert_hs_index.h
+++ b/backends/p4tools/common/compiler/convert_hs_index.h
@@ -1,7 +1,7 @@
 #ifndef BACKENDS_P4TOOLS_COMMON_COMPILER_CONVERT_HS_INDEX_H_
 #define BACKENDS_P4TOOLS_COMMON_COMPILER_CONVERT_HS_INDEX_H_
 
-#include <stddef.h>
+#include <cstddef>
 
 #include "ir/ir.h"
 #include "ir/node.h"
diff --git a/backends/p4tools/common/core/solver.h b/backends/p4tools/common/core/solver.h
index 34e04d87ca3..0cc141ce2a2 100644
--- a/backends/p4tools/common/core/solver.h
+++ b/backends/p4tools/common/core/solver.h
@@ -4,7 +4,11 @@
 #include <optional>
 #include <vector>
 
-#include "backends/p4tools/common/lib/model.h"
+#include <boost/container/flat_map.hpp>
+#include <boost/container/flat_set.hpp>
+
+#include "ir/ir.h"
+#include "lib/castable.h"
 #include "lib/cstring.h"
 
 namespace P4Tools {
@@ -13,6 +17,19 @@ namespace P4Tools {
 // TODO: This should implement AbstractRepCheckedNode<Constraint>.
 using Constraint = IR::Expression;
 
+/// Comparator to compare SymbolicVariable pointers.
+struct SymbolicVarComp {
+    bool operator()(const IR::SymbolicVariable *s1, const IR::SymbolicVariable *s2) const {
+        return s1->operator<(*s2);
+    }
+};
+
+/// This type maps symbolic variables to their value assigned by the solver.
+using SymbolicMapping = boost::container::flat_map<const IR::SymbolicVariable *,
+                                                   const IR::Expression *, SymbolicVarComp>;
+
+using SymbolicSet = boost::container::flat_set<const IR::SymbolicVariable *, SymbolicVarComp>;
+
 /// Provides a higher-level interface for an SMT solver.
 class AbstractSolver : public ICastable {
  public:
@@ -40,13 +57,13 @@ class AbstractSolver : public ICastable {
     /// @checkSat returned anything other than true, if there was no such previous call, or if the
     /// state in the solver has changed since the last such call (e.g., more assertions have been
     /// made).
-    virtual const Model *getModel() const = 0;
+    [[nodiscard]] virtual const SymbolicMapping &getSymbolicMapping() const = 0;
 
     /// Saves solver state to the given JSON generator.
     virtual void toJSON(JSONGenerator &) const = 0;
 
     /// @returns whether this solver is incremental.
-    virtual bool isInIncrementalMode() const = 0;
+    [[nodiscard]] virtual bool isInIncrementalMode() const = 0;
 
     /// Cast an abstract solver to its specific sub type.
     /// Casts involving "const" have to explicit in this case. This is necessary because abstract
diff --git a/backends/p4tools/common/core/z3_solver.cpp b/backends/p4tools/common/core/z3_solver.cpp
index 93f439ebde2..199b13a9aab 100644
--- a/backends/p4tools/common/core/z3_solver.cpp
+++ b/backends/p4tools/common/core/z3_solver.cpp
@@ -8,13 +8,11 @@
 #include <iterator>
 #include <list>
 #include <map>
-#include <ostream>
 #include <string>
 #include <utility>
 
 #include <boost/multiprecision/cpp_int.hpp>
 
-#include "backends/p4tools/common/lib/model.h"
 #include "ir/ir.h"
 #include "ir/irutils.h"
 #include "ir/json_loader.h"  // IWYU pragma: keep
@@ -70,8 +68,7 @@ class Z3Translator : public virtual Inspector {
     bool preorder(const IR::BoolLiteral *boolLiteral) override;
 
     /// Translates variables.
-    bool preorder(const IR::Member *member) override;
-    bool preorder(const IR::ConcolicVariable *var) override;
+    bool preorder(const IR::SymbolicVariable *var) override;
 
     // Translations for unary operations.
     bool preorder(const IR::Neg *op) override;
@@ -161,35 +158,21 @@ z3::sort Z3Solver::toSort(const IR::Type *type) {
     BUG("Z3Solver: unimplemented type %1%: %2% ", type->node_type_name(), type);
 }
 
-std::string Z3Solver::generateName(const IR::StateVariable &var) const {
+std::string Z3Solver::generateName(const IR::SymbolicVariable &var) {
     std::ostringstream ostr;
-    generateName(ostr, var);
+    ostr << var;
     return ostr.str();
 }
 
-void Z3Solver::generateName(std::ostringstream &ostr, const IR::StateVariable &var) const {
-    // Recurse into the parent member expression to retrieve the full name of the variable.
-    if (const auto *next = var->expr->to<IR::Member>()) {
-        generateName(ostr, next);
-    } else {
-        const auto *path = var->expr->to<IR::PathExpression>();
-        BUG_CHECK(path, "Z3Solver: expected to be a PathExpression: %1%", var->expr);
-        ostr << path->path->name;
-    }
-
-    ostr << "." << var->member;
-}
-
-z3::expr Z3Solver::declareVar(const IR::StateVariable &var) {
-    BUG_CHECK(var, "Z3Solver: attempted to declare a non-member: %1%", var);
-    auto sort = toSort(var->type);
+z3::expr Z3Solver::declareVar(const IR::SymbolicVariable &var) {
+    auto sort = toSort(var.type);
     auto expr = z3context.constant(generateName(var).c_str(), sort);
     BUG_CHECK(
         !declaredVarsById.empty(),
         "DeclaredVarsById should have at least one entry! Check if push() was used correctly.");
     // Need to take the reference here to avoid accidental copies.
     auto *latestVars = &declaredVarsById.back();
-    latestVars->emplace(expr.id(), var);
+    latestVars->emplace(expr.id(), &var);
     return expr;
 }
 
@@ -320,17 +303,17 @@ void Z3Solver::asrt(const Constraint *assertion) {
     }
 }
 
-const Model *Z3Solver::getModel() const {
-    auto *result = new Model();
+const SymbolicMapping &Z3Solver::getSymbolicMapping() const {
+    auto *result = new SymbolicMapping();
     // First, collect a map of all the declared variables we have encountered in the stack.
-    std::map<unsigned int, IR::StateVariable> declaredVars;
+    std::map<unsigned int, const IR::SymbolicVariable *> declaredVars;
     for (auto it = declaredVarsById.rbegin(); it != declaredVarsById.rend(); ++it) {
         auto latestVars = *it;
         for (auto var : latestVars) {
             declaredVars.emplace(var);
         }
     }
-    // Then, get the model and match each declaration in the model to its IR::StateVariable.
+    // Then, get the model and match each declaration in the model to its IR::SymbolicVariable.
     try {
         Util::ScopedTimer ctZ3("z3");
         Util::ScopedTimer ctCheckSat("getModel");
@@ -346,13 +329,13 @@ const Model *Z3Solver::getModel() const {
             auto z3Expr = z3Func();
             auto z3Value = z3Model.get_const_interp(z3Func);
 
-            // Convert to a state variable and value.
+            // Convert to a symbolic variable and value.
             auto exprId = z3Expr.id();
             BUG_CHECK(declaredVars.count(exprId) > 0, "Z3Solver: unknown variable declaration: %1%",
                       z3Expr);
-            const auto stateVar = declaredVars.at(exprId);
-            const auto *value = toLiteral(z3Value, stateVar->type);
-            result->emplace(stateVar, value);
+            const auto *symbolicVar = declaredVars.at(exprId);
+            const auto *value = toLiteral(z3Value, symbolicVar->type);
+            result->emplace(symbolicVar, value);
         }
     } catch (z3::exception &e) {
         BUG("Z3Solver : Z3 exception: %1%", e.msg());
@@ -361,7 +344,7 @@ const Model *Z3Solver::getModel() const {
     } catch (...) {
         BUG("Z3Solver : unknown segmentation fault in getModel");
     }
-    return result;
+    return *result;
 }
 
 const IR::Literal *Z3Solver::toLiteral(const z3::expr &e, const IR::Type *type) {
@@ -533,14 +516,8 @@ bool Z3Translator::preorder(const IR::BoolLiteral *boolLiteral) {
     return false;
 }
 
-bool Z3Translator::preorder(const IR::Member *member) {
-    result = solver.declareVar(member);
-    return false;
-}
-
-bool Z3Translator::preorder(const IR::ConcolicVariable *var) {
-    /// Declare the member contained within the concolic variable
-    result = solver.declareVar(var->concolicMember);
+bool Z3Translator::preorder(const IR::SymbolicVariable *var) {
+    result = solver.declareVar(*var);
     return false;
 }
 
diff --git a/backends/p4tools/common/core/z3_solver.h b/backends/p4tools/common/core/z3_solver.h
index 20688fd0bfd..d02e65a9ec9 100644
--- a/backends/p4tools/common/core/z3_solver.h
+++ b/backends/p4tools/common/core/z3_solver.h
@@ -1,16 +1,15 @@
 #ifndef BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 #define BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 
-#include <stddef.h>
 #include <z3++.h>
 
+#include <cstddef>
 #include <iosfwd>
 #include <optional>
 #include <string>
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/lib/model.h"
 #include "ir/ir.h"
 #include "ir/json_generator.h"
 #include "lib/cstring.h"
@@ -22,7 +21,7 @@ namespace P4Tools {
 /// A stack of maps, which map Z3-internal expression IDs of declared Z3 variables to their
 /// corresponding P4 state variable. The maps are pushed and pop according to the solver push() and
 /// pop() operations.
-using Z3DeclareVariablesMap = std::vector<ordered_map<unsigned, const IR::StateVariable>>;
+using Z3DeclaredVariablesMap = std::vector<ordered_map<unsigned, const IR::SymbolicVariable *>>;
 
 /// A Z3-based implementation of AbstractSolver. Encapsulates a z3::solver and a z3::context.
 class Z3Solver : public AbstractSolver {
@@ -31,7 +30,7 @@ class Z3Solver : public AbstractSolver {
     friend class Z3SolverAccessor;
 
  public:
-    virtual ~Z3Solver() = default;
+    ~Z3Solver() override = default;
 
     explicit Z3Solver(bool isIncremental = true,
                       std::optional<std::istream *> inOpt = std::nullopt);
@@ -44,20 +43,20 @@ class Z3Solver : public AbstractSolver {
 
     std::optional<bool> checkSat(const std::vector<const Constraint *> &asserts) override;
 
-    const Model *getModel() const override;
+    [[nodiscard]] const SymbolicMapping &getSymbolicMapping() const override;
 
     void toJSON(JSONGenerator & /*json*/) const override;
 
-    bool isInIncrementalMode() const override;
+    [[nodiscard]] bool isInIncrementalMode() const override;
 
     /// Get the actual Z3 solver backing this class.
-    const z3::solver &getZ3Solver() const;
+    [[nodiscard]] const z3::solver &getZ3Solver() const;
 
     /// Get the actual Z3 context that this class uses.
-    const z3::context &getZ3Ctx() const;
+    [[nodiscard]] const z3::context &getZ3Ctx() const;
 
     /// @returns the list of active assertions on this solver.
-    safe_vector<const Constraint *> getAssertions() const;
+    [[nodiscard]] safe_vector<const Constraint *> getAssertions() const;
 
  private:
     /// Resets the internal state: pops all assertions from previous solver
@@ -76,17 +75,13 @@ class Z3Solver : public AbstractSolver {
     /// Converts a P4 type to a Z3 sort.
     z3::sort toSort(const IR::Type *type);
 
-    /// Declares the given state variable to Z3.
+    /// Declares the given symbolic variable to Z3.
     ///
     /// @returns the resulting Z3 variable.
-    z3::expr declareVar(const IR::StateVariable &var);
+    z3::expr declareVar(const IR::SymbolicVariable &var);
 
-    /// Generates a Z3 name for the given variable.
-    std::string generateName(const IR::StateVariable &var) const;
-
-    /// Generates a Z3 name for the given variable. The generated name is written to the given
-    /// output stream.
-    void generateName(std::ostringstream &ostr, const IR::StateVariable &var) const;
+    /// Generates a Z3 name for the given symbolic variable.
+    [[nodiscard]] static std::string generateName(const IR::SymbolicVariable &var);
 
     /// Converts a Z3 expression to an IR::Literal with the given type.
     static const IR::Literal *toLiteral(const z3::expr &e, const IR::Type *type);
@@ -107,7 +102,7 @@ class Z3Solver : public AbstractSolver {
 
     /// For each state variable declared in the solver, this maps the variable's Z3 expression ID
     /// to the original state variable.
-    Z3DeclareVariablesMap declaredVarsById;
+    Z3DeclaredVariablesMap declaredVarsById;
 
     /// The sequence of P4 assertions that have been made to the solver.
     safe_vector<const Constraint *> p4Assertions;
diff --git a/backends/p4tools/common/lib/format_int.cpp b/backends/p4tools/common/lib/format_int.cpp
index 10a74e203f0..eb93e158177 100644
--- a/backends/p4tools/common/lib/format_int.cpp
+++ b/backends/p4tools/common/lib/format_int.cpp
@@ -13,7 +13,6 @@
 
 #include "lib/cstring.h"
 #include "lib/exceptions.h"
-#include "lib/log.h"
 
 namespace P4Tools {
 
diff --git a/backends/p4tools/common/lib/model.cpp b/backends/p4tools/common/lib/model.cpp
index a553e642c12..b7d8ad912a8 100644
--- a/backends/p4tools/common/lib/model.cpp
+++ b/backends/p4tools/common/lib/model.cpp
@@ -10,47 +10,49 @@
 #include "ir/indexed_vector.h"
 #include "ir/irutils.h"
 #include "ir/vector.h"
-#include "ir/visitor.h"
 #include "lib/cstring.h"
 #include "lib/exceptions.h"
 #include "lib/log.h"
 
 namespace P4Tools {
 
-// A visitor that iterates over an input expression and visits all the variables in the input
-// expression. These variables correspond to variables that were used for constraints in model
-// generated by the SMT solver. 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. Completed
-/// variables are added to the model.
-class CompleteVisitor : public Inspector {
-    Model *model;
-
- public:
-    bool preorder(const IR::Member *member) override {
-        if (model->count(member) == 0) {
-            LOG_FEATURE(
-                "common", 5,
-                "***** Did not find a binding for " << member << ". Autocompleting." << std::endl);
-            const auto *type = member->type;
-            model->emplace(member, IR::getDefaultValue(type));
-        }
-        return false;
-    }
+Model::SubstVisitor::SubstVisitor(const Model &model) : self(model) {}
+
+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);
+    prune();
+    return self.symbolicMap.at(var)->checkedTo<IR::Literal>();
+}
+
+const IR::Literal *Model::SubstVisitor::preorder(IR::TaintExpression *var) {
+    return IR::getDefaultValue(var->type);
+}
+
+Model::CompleteVisitor::CompleteVisitor(Model &model) : self(model) {}
 
-    bool preorder(const IR::ConcolicVariable *var) override {
-        auto stateVar = IR::StateVariable(var->concolicMember);
-        model->emplace(stateVar, IR::getDefaultValue(var->type));
-        return false;
+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));
     }
+    return false;
+}
 
-    explicit CompleteVisitor(Model *model) : model(model) {}
-};
+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 IR::Expression *expr) { expr->apply(CompleteVisitor(*this)); }
 
-void Model::complete(const std::set<IR::StateVariable> &inputSet) {
-    auto completionVisitor = CompleteVisitor(this);
+void Model::complete(const SymbolicSet &inputSet) {
+    auto completionVisitor = CompleteVisitor(*this);
     for (const auto &var : inputSet) {
         var->apply(completionVisitor);
     }
@@ -59,7 +61,7 @@ void Model::complete(const std::set<IR::StateVariable> &inputSet) {
 void Model::complete(const SymbolicMapType &inputMap) {
     for (const auto &inputTuple : inputMap) {
         const auto *expr = inputTuple.second;
-        expr->apply(CompleteVisitor(this));
+        expr->apply(CompleteVisitor(*this));
     }
 }
 
@@ -97,29 +99,6 @@ const IR::ListExpression *Model::evaluateListExpr(const IR::ListExpression *list
 
 const IR::Literal *Model::evaluate(const IR::Expression *expr,
                                    ExpressionMap *resolvedExpressions) const {
-    class SubstVisitor : public Transform {
-        const Model &self;
-
-     public:
-        const IR::Literal *preorder(IR::Member *member) override {
-            BUG_CHECK(self.count(member), "Variable not bound in model: %1%", member);
-            prune();
-            return self.at(IR::StateVariable(member))->checkedTo<IR::Literal>();
-        }
-
-        const IR::Literal *preorder(IR::TaintExpression *var) override {
-            return IR::getDefaultValue(var->type);
-        }
-
-        const IR::Literal *preorder(IR::ConcolicVariable *var) override {
-            auto stateVar = IR::StateVariable(var->concolicMember);
-            BUG_CHECK(self.count(stateVar), "Variable not bound in model: %1%",
-                      stateVar->toString());
-            return self.at(stateVar)->checkedTo<IR::Literal>();
-        }
-
-        explicit SubstVisitor(const Model &model) : self(model) {}
-    };
     const auto *substituted = expr->apply(SubstVisitor(*this));
     const auto *evaluated = P4::optimizeExpression(substituted);
     const auto *literal = evaluated->checkedTo<IR::Literal>();
@@ -133,7 +112,7 @@ const IR::Literal *Model::evaluate(const IR::Expression *expr,
 Model *Model::evaluate(const SymbolicMapType &inputMap, ExpressionMap *resolvedExpressions) const {
     auto *result = new Model(*this);
     for (const auto &inputTuple : inputMap) {
-        auto name = inputTuple.first;
+        const auto &name = inputTuple.first;
         const auto *expr = inputTuple.second;
         (*result)[name] = evaluate(expr, resolvedExpressions);
     }
@@ -149,4 +128,6 @@ const IR::Expression *Model::get(const IR::StateVariable &var, bool checked) con
     return nullptr;
 }
 
+const SymbolicMapping &Model::getSymbolicMap() { return symbolicMap; }
+
 }  // namespace P4Tools
diff --git a/backends/p4tools/common/lib/model.h b/backends/p4tools/common/lib/model.h
index 114f04b87e1..79eadf03ee9 100644
--- a/backends/p4tools/common/lib/model.h
+++ b/backends/p4tools/common/lib/model.h
@@ -2,12 +2,14 @@
 #define BACKENDS_P4TOOLS_COMMON_LIB_MODEL_H_
 
 #include <map>
-#include <set>
+#include <utility>
 #include <vector>
 
 #include <boost/container/flat_map.hpp>
 
+#include "backends/p4tools/common/core/solver.h"
 #include "ir/ir.h"
+#include "ir/visitor.h"
 
 namespace P4Tools {
 
@@ -17,13 +19,55 @@ using SymbolicMapType = boost::container::flat_map<IR::StateVariable, const IR::
 /// Represents a solution found by the solver. A model is a concretized form of a symbolic
 /// environment. All the expressions in a Model must be of type IR::Literal.
 class Model : public SymbolicMapType {
+ private:
+    /// The mapping of symbolic variables to values. Usually generated by an SMT solver.
+    SymbolicMapping symbolicMap;
+
+    // A visitor that iterates over an input expression and visits all the variables in the input
+    // expression. These variables correspond to variables that were used for constraints in model
+    // generated by the SMT solver. 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.
+    class SubstVisitor : public Transform {
+        const Model &self;
+
+     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);
+    };
+
  public:
     // Maps an expression to its value in the model.
     using ExpressionMap = std::map<const IR::Expression *, const IR::Literal *>;
 
+    /// A model is initialized with a symbolic map. Usually, these are derived from the solver.
+    explicit Model(SymbolicMapping symbolicMap) : symbolicMap(std::move(symbolicMap)) {}
+
+    Model(const Model &) = default;
+    Model(Model &&) = default;
+    Model &operator=(const Model &) = default;
+    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.
+    /// 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
@@ -33,7 +77,7 @@ class Model : public SymbolicMapType {
 
     /// 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 std::set<IR::StateVariable> &inputSet);
+    void complete(const SymbolicSet &inputSet);
 
     /// Evaluates a P4 expression in the context of this model.
     ///
@@ -83,7 +127,10 @@ class Model : public SymbolicMapType {
     /// Tries to retrieve @param var from the model.
     /// If @param checked is true, this function throws a BUG if the variable can not be found.
     /// Otherwise, it returns a nullptr.
-    const IR::Expression *get(const IR::StateVariable &var, bool checked) const;
+    [[nodiscard]] const IR::Expression *get(const IR::StateVariable &var, bool checked) const;
+
+    /// @returns the symbolic map contained within this model.
+    const SymbolicMapping &getSymbolicMap();
 };
 
 }  // namespace P4Tools
diff --git a/backends/p4tools/common/lib/symbolic_env.cpp b/backends/p4tools/common/lib/symbolic_env.cpp
index 892e502377e..9a120bc26a6 100644
--- a/backends/p4tools/common/lib/symbolic_env.cpp
+++ b/backends/p4tools/common/lib/symbolic_env.cpp
@@ -8,7 +8,6 @@
 #include <boost/container/vector.hpp>
 
 #include "backends/p4tools/common/lib/model.h"
-#include "backends/p4tools/common/lib/zombie.h"
 #include "frontends/p4/optimizeExpressions.h"
 #include "ir/indexed_vector.h"
 #include "ir/vector.h"
@@ -74,6 +73,11 @@ const IR::Expression *SymbolicEnv::subst(const IR::Expression *expr) const {
 const SymbolicMapType &SymbolicEnv::getInternalMap() const { return map; }
 
 bool SymbolicEnv::isSymbolicValue(const IR::Node *node) {
+    // Check the obvious case first.
+    if (node->is<IR::SymbolicVariable>()) {
+        return true;
+    }
+
     // Parser states are symbolic values.
     if (node->is<IR::ParserState>()) {
         return true;
@@ -107,11 +111,6 @@ bool SymbolicEnv::isSymbolicValue(const IR::Node *node) {
         return true;
     }
 
-    // Symbolic constants are references to fields under the struct p4t*zombie.const.
-    if (const auto *member = expr->to<IR::Member>()) {
-        return Zombie::isSymbolicConst(member);
-    }
-
     // Symbolic values can be composed using several IR nodes.
     if (const auto *unary = expr->to<IR::Operation_Unary>()) {
         return (unary->is<IR::Neg>() || unary->is<IR::LNot>() || unary->is<IR::Cmpl>() ||
diff --git a/backends/p4tools/common/lib/taint.cpp b/backends/p4tools/common/lib/taint.cpp
index 108e40842c8..67f009d8803 100644
--- a/backends/p4tools/common/lib/taint.cpp
+++ b/backends/p4tools/common/lib/taint.cpp
@@ -7,8 +7,7 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/lib/model.h"
-#include "backends/p4tools/common/lib/symbolic_env.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/indexed_vector.h"
 #include "ir/irutils.h"
 #include "ir/node.h"
@@ -29,12 +28,13 @@ const IR::StringLiteral Taint::TAINTED_STRING_LITERAL = IR::StringLiteral(cstrin
 static bitvec computeTaintedBits(const SymbolicMapType &varMap, const IR::Expression *expr) {
     CHECK_NULL(expr);
     if (const auto *member = expr->to<IR::Member>()) {
-        if (SymbolicEnv::isSymbolicValue(member)) {
-            return {};
-        }
         expr = varMap.at(member);
     }
 
+    if (expr->is<IR::SymbolicVariable>()) {
+        return {};
+    }
+
     if (const auto *taintExpr = expr->to<IR::TaintExpression>()) {
         return {0, static_cast<size_t>(taintExpr->type->width_bits())};
     }
@@ -89,9 +89,6 @@ static bitvec computeTaintedBits(const SymbolicMapType &varMap, const IR::Expres
     if (expr->is<IR::DefaultExpression>()) {
         return {};
     }
-    if (expr->is<IR::ConcolicVariable>()) {
-        return {};
-    }
     BUG("Taint pair collection is unsupported for %1% of type %2%", expr, expr->node_type_name());
 }
 
@@ -99,12 +96,12 @@ bool Taint::hasTaint(const SymbolicMapType &varMap, const IR::Expression *expr)
     if (expr->is<IR::TaintExpression>()) {
         return true;
     }
-    if (const auto *member = expr->to<IR::Member>()) {
-        if (!SymbolicEnv::isSymbolicValue(member)) {
-            return hasTaint(varMap, varMap.at(member));
-        }
+    if (expr->is<IR::SymbolicVariable>()) {
         return false;
     }
+    if (const auto *member = expr->to<IR::Member>()) {
+        return hasTaint(varMap, varMap.at(member));
+    }
     if (const auto *structExpr = expr->to<IR::StructExpression>()) {
         for (const auto *subExpr : structExpr->components) {
             if (hasTaint(varMap, subExpr->expression)) {
@@ -139,9 +136,6 @@ bool Taint::hasTaint(const SymbolicMapType &varMap, const IR::Expression *expr)
     if (expr->is<IR::DefaultExpression>()) {
         return false;
     }
-    if (expr->is<IR::ConcolicVariable>()) {
-        return false;
-    }
     BUG("Taint checking is unsupported for %1% of type %2%", expr, expr->node_type_name());
 }
 
@@ -163,23 +157,16 @@ class TaintPropagator : public Transform {
         return lit;
     }
 
-    const IR::Node *postorder(IR::PathExpression *path) override {
-        // Path expressions as part of members can be encountered during the post-order traversal.
-        // Ignore them.
-        return path;
-    }
-
     const IR::Node *postorder(IR::TaintExpression *expr) override { return expr; }
 
-    const IR::Node *postorder(IR::ConcolicVariable *var) override {
+    const IR::Node *postorder(IR::SymbolicVariable *var) override {
         return new IR::Constant(var->type, IR::getMaxBvVal(var->type));
     }
-    const IR::Node *postorder(IR::Operation_Unary *unary_op) override { return unary_op->expr; }
 
-    const IR::Node *postorder(IR::Member *member) override {
-        // We do not want to split members.
-        return member;
+    const IR::Node *postorder(IR::ConcolicVariable *var) override {
+        return new IR::Constant(var->type, IR::getMaxBvVal(var->type));
     }
+    const IR::Node *postorder(IR::Operation_Unary *unary_op) override { return unary_op->expr; }
 
     const IR::Node *postorder(IR::Cast *cast) override {
         if (Taint::hasTaint(varMap, cast->expr)) {
@@ -217,7 +204,7 @@ class TaintPropagator : public Transform {
         auto width = 1 + slLeftInt - slRightInt;
         const auto *sliceTb = IR::getBitType(width);
         if (Taint::hasTaint(varMap, slice)) {
-            return Utils::getTaintExpression(sliceTb);
+            return ToolsVariables::getTaintExpression(sliceTb);
         }
         // Otherwise we convert the expression to a constant of the sliced type.
         // Ultimately, the value here does not matter.
diff --git a/backends/p4tools/common/lib/trace_event_types.cpp b/backends/p4tools/common/lib/trace_event_types.cpp
index 5cde9989827..bb9a76c2583 100644
--- a/backends/p4tools/common/lib/trace_event_types.cpp
+++ b/backends/p4tools/common/lib/trace_event_types.cpp
@@ -9,7 +9,6 @@
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/taint.h"
-#include "ir/vector.h"
 #include "lib/exceptions.h"
 #include "lib/log.h"
 #include "lib/null.h"
diff --git a/backends/p4tools/common/lib/trace_event_types.h b/backends/p4tools/common/lib/trace_event_types.h
index db1fc799d75..ffca4fae832 100644
--- a/backends/p4tools/common/lib/trace_event_types.h
+++ b/backends/p4tools/common/lib/trace_event_types.h
@@ -2,6 +2,8 @@
 #define BACKENDS_P4TOOLS_COMMON_LIB_TRACE_EVENT_TYPES_H_
 
 #include <iosfwd>
+#include <utility>
+#include <vector>
 
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
diff --git a/backends/p4tools/common/lib/util.cpp b/backends/p4tools/common/lib/util.cpp
index 48580ad707e..8fe113b7a9c 100644
--- a/backends/p4tools/common/lib/util.cpp
+++ b/backends/p4tools/common/lib/util.cpp
@@ -6,10 +6,8 @@
 #include <cstdint>
 #include <ctime>
 #include <iomanip>
-#include <map>
 #include <optional>
 #include <ratio>
-#include <tuple>
 
 #include <boost/multiprecision/cpp_int.hpp>
 #include <boost/multiprecision/cpp_int/add.hpp>
@@ -17,7 +15,6 @@
 #include <boost/multiprecision/number.hpp>
 #include <boost/random/uniform_int_distribution.hpp>
 
-#include "backends/p4tools/common/lib/zombie.h"
 #include "ir/id.h"
 #include "ir/irutils.h"
 #include "ir/vector.h"
@@ -90,77 +87,9 @@ const IR::Constant *Utils::getRandConstantForType(const IR::Type_Bits *type) {
 }
 
 /* =========================================================================================
- *  Variables and symbolic constants.
+ *  Other.
  * ========================================================================================= */
 
-const cstring Utils::Valid = "*valid";
-
-const IR::StateVariable &Utils::getZombieTableVar(const IR::Type *type, const IR::P4Table *table,
-                                                  cstring name, std::optional<int> idx1_opt,
-                                                  std::optional<int> idx2_opt) {
-    // Mash the table name, the given name, and the optional indices together.
-    // XXX To be nice, we should probably build a PathExpression, but that's annoying to do, and we
-    // XXX can probably get away with this.
-    std::stringstream out;
-    out << table->name.toString() << "." << name;
-    if (idx1_opt.has_value()) {
-        out << "." << idx1_opt.value();
-    }
-    if (idx2_opt.has_value()) {
-        out << "." << idx2_opt.value();
-    }
-
-    return Zombie::getVar(type, 0, out.str());
-}
-
-const IR::StateVariable &Utils::getZombieVar(const IR::Type *type, int incarnation, cstring name) {
-    return Zombie::getVar(type, incarnation, name);
-}
-
-const IR::StateVariable &Utils::getZombieConst(const IR::Type *type, int incarnation,
-                                               cstring name) {
-    return Zombie::getConst(type, incarnation, name);
-}
-
-IR::StateVariable Utils::getHeaderValidity(const IR::Expression *headerRef) {
-    return new IR::Member(IR::Type::Boolean::get(), headerRef, Valid);
-}
-
-IR::StateVariable Utils::addZombiePostfix(const IR::Expression *paramPath,
-                                          const IR::Type_Base *baseType) {
-    return new IR::Member(baseType, paramPath, "*");
-}
-
-const IR::TaintExpression *Utils::getTaintExpression(const IR::Type *type) {
-    // Do not cache varbits.
-    if (type->is<IR::Extracted_Varbits>()) {
-        return new IR::TaintExpression(type);
-    }
-    // Only cache bits with width lower than 16 bit to restrict the size of the cache.
-    const auto *tb = type->to<IR::Type_Bits>();
-    if (type->width_bits() > 16 || tb == nullptr) {
-        return new IR::TaintExpression(type);
-    }
-    // Taint expressions are interned. Keys in the intern map is the signedness and width of the
-    // type.
-    using key_t = std::tuple<int, bool>;
-    static std::map<key_t, const IR::TaintExpression *> taints;
-
-    auto *&result = taints[{tb->width_bits(), tb->isSigned}];
-    if (result == nullptr) {
-        result = new IR::TaintExpression(type);
-    }
-
-    return result;
-}
-
-const IR::StateVariable &Utils::getConcolicMember(const IR::ConcolicVariable *var, int concolicId) {
-    const auto *const concolicMember = var->concolicMember;
-    auto *clonedMember = concolicMember->clone();
-    clonedMember->member = std::to_string(concolicId).c_str();
-    return *(new IR::StateVariable(clonedMember));
-}
-
 const IR::MethodCallExpression *Utils::generateInternalMethodCall(
     cstring methodName, const std::vector<const IR::Expression *> &argVector,
     const IR::Type *returnType) {
diff --git a/backends/p4tools/common/lib/util.h b/backends/p4tools/common/lib/util.h
index 305c11b3b8d..1105f11ed19 100644
--- a/backends/p4tools/common/lib/util.h
+++ b/backends/p4tools/common/lib/util.h
@@ -82,53 +82,9 @@ class Utils {
     static const IR::Constant *getRandConstantForType(const IR::Type_Bits *type);
 
     /* =========================================================================================
-     *  Variables and symbolic constants.
+     *  Other.
      * ========================================================================================= */
  public:
-    /// To represent header validity, we pretend that every header has a field that reflects the
-    /// header's validity state. This is the name of that field. This is not a valid P4 identifier,
-    /// so it is guaranteed to not conflict with any other field in the header.
-    static const cstring Valid;
-
-    /// @see Zombie::getVar.
-    static const IR::StateVariable &getZombieVar(const IR::Type *type, int incarnation,
-                                                 cstring name);
-
-    /// @see Zombie::getConst.
-    static const IR::StateVariable &getZombieConst(const IR::Type *type, int incarnation,
-                                                   cstring name);
-
-    /// @see Utils::getZombieConst.
-    /// This function is used to generated variables caused by undefined behavior. This is merely a
-    /// wrapper function for the creation of a new Taint IR object.
-    static const IR::TaintExpression *getTaintExpression(const IR::Type *type);
-
-    /// Creates a new member variable from a concolic variable but replaces its concolic ID.
-    /// This is used within concolic methods to map back several concolic variables from a single
-    /// method call.
-    static const IR::StateVariable &getConcolicMember(const IR::ConcolicVariable *var,
-                                                      int concolicId);
-
-    /// @returns the zombie variable with the given type, for tracking an aspect of the given
-    /// table. The returned variable will be named p4t*zombie.table.t.name.idx1.idx2, where t is
-    /// the name of the given table. The "idx1" and "idx2" components are produced only if idx1 and
-    /// idx2 are given, respectively.
-    static const IR::StateVariable &getZombieTableVar(const IR::Type *type,
-                                                      const IR::P4Table *table, cstring name,
-                                                      std::optional<int> idx1_opt = std::nullopt,
-                                                      std::optional<int> idx2_opt = std::nullopt);
-
-    /// @returns the state variable for the validity of the given header instance. The resulting
-    ///     variable will be boolean-typed.
-    ///
-    /// @param headerRef a header instance. This is either a Member or a PathExpression.
-    static IR::StateVariable getHeaderValidity(const IR::Expression *headerRef);
-
-    /// @returns a IR::StateVariable that is postfixed with "*". This is used for PathExpressions
-    /// with are not yet members.
-    static IR::StateVariable addZombiePostfix(const IR::Expression *paramPath,
-                                              const IR::Type_Base *baseType);
-
     /// @returns a method call to an internal extern consumed by the interpreter. The return type
     /// is typically Type_Void.
     static const IR::MethodCallExpression *generateInternalMethodCall(
diff --git a/backends/p4tools/common/lib/variables.cpp b/backends/p4tools/common/lib/variables.cpp
new file mode 100644
index 00000000000..aefc49fffac
--- /dev/null
+++ b/backends/p4tools/common/lib/variables.cpp
@@ -0,0 +1,61 @@
+#include "backends/p4tools/common/lib/variables.h"
+
+#include <map>
+#include <string>
+#include <tuple>
+
+#include "ir/id.h"
+
+namespace P4Tools {
+
+const IR::PathExpression ToolsVariables::VAR_PREFIX = IR::PathExpression("p4tools*var");
+
+const IR::StateVariable &ToolsVariables::getStateVariable(const IR::Type *type, cstring name) {
+    // TODO: Is caching worth it here?
+    // TODO: Do we really need to "allocate" a state variable? They are immediately consumed  by the
+    // symbolic environment.
+    return *new IR::StateVariable(new IR::Member(type, &VAR_PREFIX, name));
+}
+
+const IR::SymbolicVariable *ToolsVariables::getSymbolicVariable(const IR::Type *type,
+                                                                int incarnation, cstring name) {
+    // TODO: Is caching worth it here?
+    auto symbolicName = name + "_" + std::to_string(incarnation);
+    return new IR::SymbolicVariable(type, symbolicName);
+}
+
+const cstring ToolsVariables::VALID = "*valid";
+
+IR::StateVariable ToolsVariables::getHeaderValidity(const IR::Expression *headerRef) {
+    return new IR::Member(IR::Type::Boolean::get(), headerRef, VALID);
+}
+
+IR::StateVariable ToolsVariables::addStateVariablePostfix(const IR::Expression *paramPath,
+                                                          const IR::Type_Base *baseType) {
+    return new IR::Member(baseType, paramPath, "*");
+}
+
+const IR::TaintExpression *ToolsVariables::getTaintExpression(const IR::Type *type) {
+    // Do not cache varbits.
+    if (type->is<IR::Extracted_Varbits>()) {
+        return new IR::TaintExpression(type);
+    }
+    // Only cache bits with width lower than 16 bit to restrict the size of the cache.
+    const auto *tb = type->to<IR::Type_Bits>();
+    if (type->width_bits() > 16 || tb == nullptr) {
+        return new IR::TaintExpression(type);
+    }
+    // Taint expressions are interned. Keys in the intern map is the signedness and width of the
+    // type.
+    using key_t = std::tuple<int, bool>;
+    static std::map<key_t, const IR::TaintExpression *> TAINTS;
+
+    auto *&result = TAINTS[{tb->width_bits(), tb->isSigned}];
+    if (result == nullptr) {
+        result = new IR::TaintExpression(type);
+    }
+
+    return result;
+}
+
+}  // namespace P4Tools
diff --git a/backends/p4tools/common/lib/variables.h b/backends/p4tools/common/lib/variables.h
new file mode 100644
index 00000000000..fdf7d2e2bff
--- /dev/null
+++ b/backends/p4tools/common/lib/variables.h
@@ -0,0 +1,55 @@
+#ifndef BACKENDS_P4TOOLS_COMMON_LIB_VARIABLES_H_
+#define BACKENDS_P4TOOLS_COMMON_LIB_VARIABLES_H_
+
+#include "ir/ir.h"
+#include "lib/cstring.h"
+
+namespace P4Tools {
+
+/// Variables internal to P4Tools. These variables do not exist in the P4
+/// program itself, but are generated and added to the environment by the P4Tools tooling. These
+/// variables are also used for SMT solvers as symbolic variables.
+class ToolsVariables {
+ private:
+    /// The prefix used for state variables.
+    static const IR::PathExpression VAR_PREFIX;
+
+ public:
+    /// To represent header validity, we pretend that every header has a field that reflects the
+    /// header's validity state. This is the name of that field. This is not a valid P4 identifier,
+    /// so it is guaranteed to not conflict with any other field in the header.
+    static const cstring VALID;
+
+    /// @returns the variable with the given @type, @incarnation, and @name.
+    ///
+    /// A BUG occurs if this was previously called with the same @name and @incarnation, but with a
+    /// different @type.
+    static const IR::StateVariable &getStateVariable(const IR::Type *type, cstring name);
+
+    /// @returns the symbolic variable with the given @type, @incarnation, and @name.
+    ///
+    /// A BUG occurs if this was previously called with the same @name and @incarnation, but with a
+    /// different @type.
+    static const IR::SymbolicVariable *getSymbolicVariable(const IR::Type *type, int incarnation,
+                                                           cstring name);
+
+    /// @see ToolsVariables::getSymbolicVariable.
+    /// This function is used to generated variables caused by undefined behavior. This is merely a
+    /// wrapper function for the creation of a new Taint IR object.
+    static const IR::TaintExpression *getTaintExpression(const IR::Type *type);
+
+    /// @returns the state variable for the validity of the given header instance. The resulting
+    ///     variable will be boolean-typed.
+    ///
+    /// @param headerRef a header instance. This is either a Member or a PathExpression.
+    static IR::StateVariable getHeaderValidity(const IR::Expression *headerRef);
+
+    /// @returns a IR::StateVariable that is postfixed with "*". This is used for PathExpressions
+    /// with are not yet members.
+    static IR::StateVariable addStateVariablePostfix(const IR::Expression *paramPath,
+                                                     const IR::Type_Base *baseType);
+};
+
+}  // namespace P4Tools
+
+#endif /* BACKENDS_P4TOOLS_COMMON_LIB_VARIABLES_H_ */
diff --git a/backends/p4tools/common/lib/zombie.cpp b/backends/p4tools/common/lib/zombie.cpp
deleted file mode 100644
index 75e45fedc2a..00000000000
--- a/backends/p4tools/common/lib/zombie.cpp
+++ /dev/null
@@ -1,66 +0,0 @@
-#include "backends/p4tools/common/lib/zombie.h"
-
-#include <map>
-#include <string>
-#include <utility>
-
-#include "ir/id.h"
-
-namespace P4Tools {
-
-const cstring Zombie::P4tZombie = "p4t*zombie";
-const cstring Zombie::Const = "const";
-
-bool Zombie::isSymbolicConst(const IR::Member *member) {
-    // Should always have an inner member to represent at least p4t*zombie.const.
-    const auto *innerMember = member->expr->to<IR::Member>();
-    if (innerMember == nullptr) {
-        return false;
-    }
-
-    // Base case: detect p4t*zombie.const.foo.
-    if (innerMember->member == Const) {
-        if (const auto *pathExpr = innerMember->expr->to<IR::PathExpression>()) {
-            const auto *path = pathExpr->path;
-            return (path != nullptr) && path->name == P4tZombie;
-        }
-    }
-
-    // Recursive case.
-    return isSymbolicConst(innerMember);
-}
-
-const IR::StateVariable &Zombie::getVar(const IR::Type *type, int incarnation, cstring name) {
-    return getZombie(type, false, incarnation, name);
-}
-
-const IR::StateVariable &Zombie::getConst(const IR::Type *type, int incarnation, cstring name) {
-    return getZombie(type, true, incarnation, name);
-}
-
-const IR::StateVariable &Zombie::getZombie(const IR::Type *type, bool isConst, int incarnation,
-                                           cstring name) {
-    // Zombie variables are interned. Keys in the intern map are tuples of isConst, incarnations,
-    // and names.
-    return *mkZombie(type, isConst, incarnation, name);
-}
-
-const IR::StateVariable *Zombie::mkZombie(const IR::Type *type, bool isConst, int incarnation,
-                                          cstring name) {
-    static IR::PathExpression ZOMBIE_HDR(new IR::Path(P4tZombie));
-
-    using key_t = std::pair<bool, int>;
-    static std::map<key_t, const IR::Member *> incarnations;
-    const auto *&incarnationMember = incarnations[std::make_pair(isConst, incarnation)];
-    if (incarnationMember == nullptr) {
-        const IR::Expression *hdr = &ZOMBIE_HDR;
-        if (isConst) {
-            hdr = new IR::Member(hdr, Const);
-        }
-        incarnationMember = new IR::Member(hdr, cstring(std::to_string(incarnation)));
-    }
-
-    return new IR::StateVariable(new IR::Member(type, incarnationMember, name));
-}
-
-}  // namespace P4Tools
diff --git a/backends/p4tools/common/lib/zombie.h b/backends/p4tools/common/lib/zombie.h
deleted file mode 100644
index 2893c16d666..00000000000
--- a/backends/p4tools/common/lib/zombie.h
+++ /dev/null
@@ -1,48 +0,0 @@
-#ifndef BACKENDS_P4TOOLS_COMMON_LIB_ZOMBIE_H_
-#define BACKENDS_P4TOOLS_COMMON_LIB_ZOMBIE_H_
-
-#include "ir/ir.h"
-#include "lib/cstring.h"
-
-namespace P4Tools {
-
-/// Zombies are variables internal to P4Tools. They are variables that do not exist in the P4
-/// program itself, but are generated and added to the environment by the P4Tools tooling. These
-/// variables are also used for SMT solvers as symbolic variables.
-class Zombie {
- private:
-    /// The name of the top-level struct containing all zombie state.
-    static const cstring P4tZombie;
-
-    /// The name of the struct below P4tZombie that contains all symbolic constants.
-    static const cstring Const;
-
- public:
-    /// Determines whether the given member expression represents a symbolic constant. Symbolic
-    /// constants are references to fields under the nested struct p4t*zombie.const.
-    static bool isSymbolicConst(const IR::Member *);
-
-    /// @returns the zombie variable with the given @type, @incarnation, and @name.
-    ///
-    /// A BUG occurs if this was previously called with the same @name and @incarnation, but with a
-    /// different @type.
-    static const IR::StateVariable &getVar(const IR::Type *type, int incarnation, cstring name);
-
-    /// @returns the zombie symbolic constant with the given @type, @incarnation, and @name.
-    ///
-    /// A BUG occurs if this was previously called with the same @name and @incarnation, but with a
-    /// different @type.
-    static const IR::StateVariable &getConst(const IR::Type *type, int incarnation, cstring name);
-
- private:
-    /// @see getVar and getConst.
-    static const IR::StateVariable &getZombie(const IR::Type *type, bool isConst, int incarnation,
-                                              cstring name);
-
-    static const IR::StateVariable *mkZombie(const IR::Type *type, bool isConst, int incarnation,
-                                             cstring name);
-};
-
-}  // namespace P4Tools
-
-#endif /* BACKENDS_P4TOOLS_COMMON_LIB_ZOMBIE_H_ */
diff --git a/backends/p4tools/modules/testgen/CMakeLists.txt b/backends/p4tools/modules/testgen/CMakeLists.txt
index 6cd3906ffe2..bc9717870c0 100644
--- a/backends/p4tools/modules/testgen/CMakeLists.txt
+++ b/backends/p4tools/modules/testgen/CMakeLists.txt
@@ -33,6 +33,7 @@ set(
   lib/final_state.cpp
   lib/gen_eq.cpp
   lib/logging.cpp
+  lib/packet_vars.cpp
   lib/test_backend.cpp
   lib/test_spec.cpp
   lib/tf.cpp
diff --git a/backends/p4tools/modules/testgen/core/program_info.cpp b/backends/p4tools/modules/testgen/core/program_info.cpp
index 3873e47b4f2..06a164b9bdd 100644
--- a/backends/p4tools/modules/testgen/core/program_info.cpp
+++ b/backends/p4tools/modules/testgen/core/program_info.cpp
@@ -2,10 +2,12 @@
 
 #include "backends/p4tools/common/compiler/reachability.h"
 #include "backends/p4tools/common/lib/arch_spec.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/id.h"
+#include "ir/irutils.h"
 #include "lib/cstring.h"
+#include "lib/enumerator.h"
 #include "lib/exceptions.h"
 #include "midend/coverage.h"
 
@@ -57,6 +59,14 @@ const IR::Type_Declaration *ProgramInfo::resolveProgramType(const IR::IGeneralNa
     return decl;
 }
 
+const IR::Expression *ProgramInfo::createTargetUninitialized(const IR::Type *type,
+                                                             bool forceTaint) const {
+    if (forceTaint) {
+        return ToolsVariables::getTaintExpression(type);
+    }
+    return IR::getDefaultValue(type);
+}
+
 /* =============================================================================================
  *  Getters
  * ============================================================================================= */
diff --git a/backends/p4tools/modules/testgen/core/program_info.h b/backends/p4tools/modules/testgen/core/program_info.h
index e323a2c292a..c8eb58c5d5d 100644
--- a/backends/p4tools/modules/testgen/core/program_info.h
+++ b/backends/p4tools/modules/testgen/core/program_info.h
@@ -7,7 +7,6 @@
 
 #include "backends/p4tools/common/compiler/reachability.h"
 #include "backends/p4tools/common/lib/arch_spec.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "ir/declaration.h"
 #include "ir/ir.h"
 #include "lib/castable.h"
@@ -59,10 +58,10 @@ class ProgramInfo : public ICastable {
     [[nodiscard]] std::optional<const IR::Expression *> getTargetConstraints() const;
 
     /// @returns the metadata member corresponding to the ingress port
-    [[nodiscard]] virtual const IR::Member *getTargetInputPortVar() const = 0;
+    [[nodiscard]] virtual const IR::StateVariable &getTargetInputPortVar() const = 0;
 
     /// @returns the metadata member corresponding to the final output port
-    [[nodiscard]] virtual const IR::Member *getTargetOutputPortVar() const = 0;
+    [[nodiscard]] virtual const IR::StateVariable &getTargetOutputPortVar() const = 0;
 
     /// @returns an expression that checks whether the packet is to be dropped.
     /// The computation is target specific.
@@ -72,7 +71,7 @@ class ProgramInfo : public ICastable {
     /// be a taint variable or simply 0 (bits) or false (booleans).
     /// If @param forceTaint is active, this function always returns a taint variable.
     virtual const IR::Expression *createTargetUninitialized(const IR::Type *type,
-                                                            bool forceTaint) const = 0;
+                                                            bool forceTaint) const;
 
     /// Getter to access allStatements.
     [[nodiscard]] const P4::Coverage::CoverageSet &getAllStatements() const;
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 e90afbc2e78..a45a948bd91 100644
--- a/backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp
@@ -9,7 +9,7 @@
 #include "backends/p4tools/common/compiler/convert_hs_index.h"
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "frontends/p4/optimizeExpressions.h"
 #include "ir/dump.h"
 #include "ir/id.h"
@@ -185,7 +185,7 @@ bool AbstractStepper::stepGetHeaderValidity(const IR::Expression *headerRef) {
     if (const auto *headerUnion = headerRef->type->to<IR::Type_HeaderUnion>()) {
         for (const auto *field : headerUnion->fields) {
             auto *fieldRef = new IR::Member(field->type, headerRef, field->name);
-            const auto &variable = Utils::getHeaderValidity(fieldRef);
+            const auto &variable = ToolsVariables::getHeaderValidity(fieldRef);
             BUG_CHECK(state.exists(variable),
                       "At this point, the header validity bit should be initialized.");
             const auto *value = state.getSymbolicEnv().get(variable);
@@ -203,7 +203,7 @@ bool AbstractStepper::stepGetHeaderValidity(const IR::Expression *headerRef) {
         result->emplace_back(state);
         return false;
     }
-    const auto &variable = Utils::getHeaderValidity(headerRef);
+    const auto &variable = ToolsVariables::getHeaderValidity(headerRef);
     BUG_CHECK(state.exists(variable),
               "At this point, the header validity bit %1% should be initialized.", variable);
     state.replaceTopBody(Continuation::Return(variable));
@@ -213,7 +213,7 @@ bool AbstractStepper::stepGetHeaderValidity(const IR::Expression *headerRef) {
 
 void AbstractStepper::setHeaderValidity(const IR::Expression *expr, bool validity,
                                         ExecutionState &nextState) {
-    const auto &headerRefValidity = Utils::getHeaderValidity(expr);
+    const auto &headerRefValidity = ToolsVariables::getHeaderValidity(expr);
     nextState.set(headerRefValidity, IR::getBoolLiteral(validity));
 
     // In some cases, the header may be part of a union.
@@ -277,7 +277,8 @@ void generateStackAssigmentStatement(ExecutionState &nextState,
     const auto *rightArrIndex = HSIndexToMember::produceStackIndex(elemType, stackRef, rightIndex);
 
     // Check right header validity.
-    const auto *value = nextState.getSymbolicEnv().get(Utils::getHeaderValidity(rightArrIndex));
+    const auto *value =
+        nextState.getSymbolicEnv().get(ToolsVariables::getHeaderValidity(rightArrIndex));
     if (!value->checkedTo<IR::BoolLiteral>()->value) {
         replacements.emplace_back(generateStacksetValid(stackRef, leftIndex, false));
         return;
@@ -339,7 +340,7 @@ const IR::Literal *AbstractStepper::evaluateExpression(
     // value.
     const IR::Literal *result = nullptr;
     if (solverResult != std::nullopt && *solverResult) {
-        auto model = *solver.getModel();
+        auto model = Model(solver.getSymbolicMapping());
         model.complete(expr);
         result = model.evaluate(expr);
     }
@@ -357,8 +358,8 @@ void AbstractStepper::setTargetUninitialized(ExecutionState &nextState, const IR
         for (const auto *validField : validFields) {
             nextState.set(validField, IR::getBoolLiteral(false));
         }
-        // For each field in the undefined struct, we create a new zombie variable.
-        // If the variable does not have an initializer we need to create a new zombie for it.
+        // For each field in the undefined struct, we create a new symbolic variable.
+        // If the variable does not have an initializer we need to create a new variable for it.
         // For now we just use the name directly.
         for (const auto *field : fields) {
             nextState.set(field, programInfo.createTargetUninitialized(field->type, forceTaint));
@@ -379,8 +380,8 @@ void AbstractStepper::declareStructLike(ExecutionState &nextState, const IR::Exp
     for (const auto *validField : validFields) {
         nextState.set(validField, IR::getBoolLiteral(false));
     }
-    // For each field in the undefined struct, we create a new zombie variable.
-    // If the variable does not have an initializer we need to create a new zombie for it.
+    // For each field in the undefined struct, we create a new symbolic variable.
+    // If the variable does not have an initializer we need to create a new variable for it.
     // For now we just use the name directly.
     for (const auto *field : fields) {
         nextState.set(field, programInfo.createTargetUninitialized(field->type, forceTaint));
diff --git a/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp
index 90908a29c0d..db0b0372b21 100644
--- a/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.cpp
@@ -14,7 +14,7 @@
 #include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event_types.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/declaration.h"
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
@@ -26,14 +26,15 @@
 #include "lib/null.h"
 #include "midend/coverage.h"
 
-#include "backends/p4tools/modules/testgen//lib/exceptions.h"
 #include "backends/p4tools/modules/testgen/core/program_info.h"
 #include "backends/p4tools/modules/testgen/core/small_step/abstract_stepper.h"
 #include "backends/p4tools/modules/testgen/core/small_step/table_stepper.h"
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h"
 #include "backends/p4tools/modules/testgen/lib/collect_latent_statements.h"
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
+#include "backends/p4tools/modules/testgen/lib/exceptions.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/options.h"
 
 namespace P4Tools::P4Testgen {
@@ -66,8 +67,8 @@ void CmdStepper::declareVariable(ExecutionState &nextState, const IR::Declaratio
             declareStructLike(nextState, parentExpr, structType);
         }
     } else if (declType->is<IR::Type_Base>()) {
-        // If the variable does not have an initializer we need to create a new zombie for it.
-        // For now we just use the name directly.
+        // If the variable does not have an initializer we need to create a new value for it. For
+        // now we just use the name directly.
         const auto &left = nextState.convertPathExpr(new IR::PathExpression(decl->name));
         nextState.set(left, programInfo.createTargetUninitialized(decl->type, false));
     } else {
@@ -103,7 +104,7 @@ void CmdStepper::initializeBlockParams(const IR::Type_Declaration *typeDecl,
             declareStructLike(nextState, paramPath, ts, forceTaint);
         } else if (const auto *tb = paramType->to<IR::Type_Base>()) {
             // If the type is a flat Type_Base, postfix it with a "*".
-            const auto &paramRef = Utils::addZombiePostfix(paramPath, tb);
+            const auto &paramRef = ToolsVariables::addStateVariablePostfix(paramPath, tb);
             nextState.set(paramRef, programInfo.createTargetUninitialized(paramType, forceTaint));
         } else {
             P4C_UNIMPLEMENTED("Unsupported initialization type %1%", paramType->node_type_name());
@@ -363,7 +364,7 @@ bool CmdStepper::preorder(const IR::P4Program * /*program*/) {
     if (pktSize != 0) {
         const auto *fixedSizeEqu =
             new IR::Equ(ExecutionState::getInputPacketSizeVar(),
-                        IR::getConstant(ExecutionState::getPacketSizeVarType(), pktSize));
+                        IR::getConstant(&PacketVars::PACKET_SIZE_VAR_TYPE, pktSize));
         if (cond == std::nullopt) {
             cond = fixedSizeEqu;
         } else {
@@ -489,7 +490,7 @@ bool CmdStepper::preorder(const IR::ExitStatement *e) {
 
 const Constraint *CmdStepper::startParser(const IR::P4Parser *parser, ExecutionState &nextState) {
     // Reset the parser cursor to zero.
-    const auto *parserCursorVarType = ExecutionState::getPacketSizeVarType();
+    const auto *parserCursorVarType = &PacketVars::PACKET_SIZE_VAR_TYPE;
 
     // Constrain the input packet size to its maximum.
     const auto *boolType = IR::Type::Boolean::get();
diff --git a/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.h b/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.h
index 8c515770e66..ac16d54241e 100644
--- a/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.h
+++ b/backends/p4tools/modules/testgen/core/small_step/cmd_stepper.h
@@ -40,7 +40,7 @@ class CmdStepper : public AbstractStepper {
 
     /// Initializes the given state for entry into the given parser.
     ///
-    /// @returns constraints for associating packet data with program/zombie state.
+    /// @returns constraints for associating packet data with symbolic state.
     const Constraint *startParser(const IR::P4Parser *parser, ExecutionState &state);
 
     /// @see startParser. Implementations can assume that the parser has been registered, and the
diff --git a/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp
index f293190d3e0..571dda68305 100644
--- a/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/expr_stepper.cpp
@@ -8,7 +8,7 @@
 
 #include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/declaration.h"
 #include "ir/irutils.h"
 #include "ir/node.h"
@@ -101,7 +101,7 @@ void ExprStepper::evalActionCall(const IR::P4Action *action, const IR::MethodCal
     BUG_CHECK(actionNameSpace, "Does not instantiate an INamespace: %1%", actionNameSpace);
     auto &nextState = state.clone();
     // If the action has arguments, these are usually directionless control plane input.
-    // We introduce a zombie variable that takes the argument value. This value is either
+    // We introduce a symbolic variable that takes the argument value. This value is either
     // provided by a constant entry or synthesized by us.
     for (size_t argIdx = 0; argIdx < call->arguments->size(); ++argIdx) {
         const auto &parameters = action->parameters;
@@ -111,7 +111,7 @@ void ExprStepper::evalActionCall(const IR::P4Action *action, const IR::MethodCal
         BUG_CHECK(param->direction == IR::Direction::None,
                   "%1%: Only directionless action parameters are supported at this point. ",
                   action);
-        const auto &tableActionDataVar = Utils::getZombieVar(paramType, 0, paramName);
+        const auto &tableActionDataVar = ToolsVariables::getStateVariable(paramType, paramName);
         const auto *curArg = call->arguments->at(argIdx)->expression;
         nextState.set(tableActionDataVar, curArg);
     }
diff --git a/backends/p4tools/modules/testgen/core/small_step/expr_stepper.h b/backends/p4tools/modules/testgen/core/small_step/expr_stepper.h
index d112918787b..d673944cf34 100644
--- a/backends/p4tools/modules/testgen/core/small_step/expr_stepper.h
+++ b/backends/p4tools/modules/testgen/core/small_step/expr_stepper.h
@@ -1,6 +1,7 @@
 #ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_EXPR_STEPPER_H_
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_CORE_SMALL_STEP_EXPR_STEPPER_H_
 
+#include <utility>
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
@@ -99,7 +100,7 @@ class ExprStepper : public AbstractStepper {
 
     /// Evaluates a call to an action. This usually only happens when a table is invoked.
     /// In other cases, actions should be inlined. When the action call is evaluated, we use
-    /// zombie variables to pass arguments across execution boundaries. These variables persist
+    /// symbolic variables to pass arguments across execution boundaries. These variables persist
     /// until the end of program execution.
     /// @param action the action declaration that is being referenced.
     /// @param call the actual method call containing the arguments.
@@ -107,7 +108,7 @@ class ExprStepper : public AbstractStepper {
 
     /// @returns an assignment corresponding to the direction @dir that is provided. In the case
     /// of "out", we reset. If @targetPath is the destination we will write to. If @srcPath does
-    /// not exist, we create a new zombie variable for it.
+    /// not exist, we create a new symbolic variable for it.
     /// If @param forceTaint is true, out will set the parameter to tainted.
     // Otherwise, the target default value is chosen.
     /// TODO: Consolidate this into the copy_in_out extern.
diff --git a/backends/p4tools/modules/testgen/core/small_step/extern_stepper.cpp b/backends/p4tools/modules/testgen/core/small_step/extern_stepper.cpp
index 313ef14eac4..6ee414797e8 100644
--- a/backends/p4tools/modules/testgen/core/small_step/extern_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/extern_stepper.cpp
@@ -10,7 +10,7 @@
 
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event_types.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
 #include "ir/ir.h"
@@ -27,6 +27,7 @@
 #include "backends/p4tools/modules/testgen/core/small_step/small_step.h"
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/options.h"
 
 namespace P4Tools::P4Testgen {
@@ -86,14 +87,14 @@ ExprStepper::PacketCursorAdvanceInfo ExprStepper::calculateSuccessfulParserAdvan
     auto minSize =
         std::max(0, state.getInputPacketCursor() + advanceSize - state.getPacketBufferSize());
     auto *cond = new IR::Geq(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(),
-                             IR::getConstant(ExecutionState::getPacketSizeVarType(), minSize));
+                             IR::getConstant(&PacketVars::PACKET_SIZE_VAR_TYPE, minSize));
     return {advanceSize, cond, advanceSize, new IR::LNot(cond)};
 }
 
 ExprStepper::PacketCursorAdvanceInfo ExprStepper::calculateAdvanceExpression(
     const ExecutionState &state, const IR::Expression *advanceExpr,
     const IR::Expression *restrictions) const {
-    const auto *packetSizeVarType = ExecutionState::getPacketSizeVarType();
+    const auto *packetSizeVarType = &PacketVars::PACKET_SIZE_VAR_TYPE;
 
     const auto *cursorConst = IR::getConstant(packetSizeVarType, state.getInputPacketCursor());
     const auto *bufferSizeConst = IR::getConstant(packetSizeVarType, state.getPacketBufferSize());
@@ -349,7 +350,7 @@ void ExprStepper::evalInternalExternMethodCall(const IR::MethodCallExpression *c
                  }
              } else if (const auto *tb = assignType->to<IR::Type_Base>()) {
                  // If the type is a flat Type_Base, postfix it with a "*".
-                 globalRef = Utils::addZombiePostfix(globalRef, tb);
+                 globalRef = ToolsVariables::addStateVariablePostfix(globalRef, tb);
                  if (const auto *argPath = argRef->to<IR::PathExpression>()) {
                      argRef = nextState.convertPathExpr(argPath);
                  }
@@ -422,7 +423,7 @@ void ExprStepper::evalInternalExternMethodCall(const IR::MethodCallExpression *c
                  }
              } else if (const auto *tb = assignType->to<IR::Type_Base>()) {
                  // If the type is a flat Type_Base, postfix it with a "*".
-                 globalRef = Utils::addZombiePostfix(globalRef, tb);
+                 globalRef = ToolsVariables::addStateVariablePostfix(globalRef, tb);
                  if (const auto *argPath = argRef->to<IR::PathExpression>()) {
                      argRef = nextState.convertPathExpr(argPath);
                  }
@@ -812,7 +813,7 @@ void ExprStepper::evalExternMethodCall(const IR::MethodCallExpression *call,
                  TESTGEN_UNIMPLEMENTED("Emit input %1% of type %2% not supported", emitOutput,
                                        emitType);
              }
-             const auto &validVar = Utils::getHeaderValidity(emitOutput);
+             const auto &validVar = ToolsVariables::getHeaderValidity(emitOutput);
 
              // Check whether the validity bit of the header is tainted. If it is, the entire
              // emit is tainted. There is not much we can do here, so throw an error.
@@ -919,7 +920,7 @@ void ExprStepper::evalExternMethodCall(const IR::MethodCallExpression *call,
                  cond->dbprint(traceString);
                  taintedState.add(*new TraceEvents::Expression(cond, traceString));
                  const auto *errVar = state.getCurrentParserErrorLabel();
-                 taintedState.set(errVar, Utils::getTaintExpression(errVar->type));
+                 taintedState.set(errVar, ToolsVariables::getTaintExpression(errVar->type));
                  taintedState.popBody();
                  result->emplace_back(taintedState);
                  return;
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 30c82a9e2c6..bc64224db19 100644
--- a/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/core/small_step/table_stepper.cpp
@@ -12,7 +12,7 @@
 
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event_types.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
 #include "ir/irutils.h"
@@ -42,23 +42,42 @@ const ProgramInfo *TableStepper::getProgramInfo() { return &stepper->programInfo
 
 ExprStepper::Result TableStepper::getResult() { return stepper->result; }
 
+const IR::StateVariable &TableStepper::getTableStateVariable(const IR::Type *type,
+                                                             const IR::P4Table *table, cstring name,
+                                                             std::optional<int> idx1_opt,
+                                                             std::optional<int> idx2_opt) {
+    // Mash the table name, the given name, and the optional indices together.
+    // XXX To be nice, we should probably build a PathExpression, but that's annoying to do, and we
+    // XXX can probably get away with this.
+    std::stringstream out;
+    out << table->name.toString() << "." << name;
+    if (idx1_opt.has_value()) {
+        out << "." << idx1_opt.value();
+    }
+    if (idx2_opt.has_value()) {
+        out << "." << idx2_opt.value();
+    }
+
+    return ToolsVariables::getStateVariable(type, out.str());
+}
+
 const IR::StateVariable &TableStepper::getTableActionVar(const IR::P4Table *table) {
     auto numActions = table->getActionList()->size();
     const auto *type = IR::getBitTypeToFit(numActions);
-    return Utils::getZombieTableVar(type, table, "*action");
+    return getTableStateVariable(type, table, "*action");
 }
 
 const IR::StateVariable &TableStepper::getTableHitVar(const IR::P4Table *table) {
-    return Utils::getZombieTableVar(IR::Type::Boolean::get(), table, "*hit");
+    return getTableStateVariable(IR::Type::Boolean::get(), table, "*hit");
 }
 
 const IR::StateVariable &TableStepper::getTableKeyReadVar(const IR::P4Table *table, int keyIdx) {
     const auto *key = table->getKey()->keyElements.at(keyIdx);
-    return Utils::getZombieTableVar(key->expression->type, table, "*keyRead", keyIdx);
+    return getTableStateVariable(key->expression->type, table, "*keyRead", keyIdx);
 }
 
 const IR::StateVariable &TableStepper::getTableReachedVar(const IR::P4Table *table) {
-    return Utils::getZombieTableVar(IR::Type::Boolean::get(), table, "*reached");
+    return getTableStateVariable(IR::Type::Boolean::get(), table, "*reached");
 }
 
 bool TableStepper::compareLPMEntries(const IR::Entry *leftIn, const IR::Entry *rightIn,
@@ -111,9 +130,9 @@ const IR::Expression *TableStepper::computeTargetMatchType(ExecutionState &nextS
                                                            TableMatchMap *matches,
                                                            const IR::Expression *hitCondition) {
     const IR::Expression *keyExpr = keyProperties.key->expression;
-    // Create a new zombie constant that corresponds to the key expression.
+    // Create a new variables constant that corresponds to the key expression.
     cstring keyName = properties.tableName + "_key_" + keyProperties.name;
-    const auto ctrlPlaneKey = nextState.createZombieConst(keyExpr->type, keyName);
+    const auto ctrlPlaneKey = nextState.createSymbolicVariable(keyExpr->type, keyName);
 
     if (keyProperties.matchType == P4Constants::MATCH_KIND_EXACT) {
         hitCondition = new IR::LAnd(hitCondition, new IR::Equ(keyExpr, ctrlPlaneKey));
@@ -128,7 +147,7 @@ const IR::Expression *TableStepper::computeTargetMatchType(ExecutionState &nextS
             ternaryMask = IR::getConstant(keyExpr->type, 0);
             keyExpr = ternaryMask;
         } else {
-            ternaryMask = nextState.createZombieConst(keyExpr->type, maskName);
+            ternaryMask = nextState.createSymbolicVariable(keyExpr->type, maskName);
         }
         matches->emplace(keyProperties.name,
                          new Ternary(keyProperties.key, ctrlPlaneKey, ternaryMask));
@@ -139,7 +158,7 @@ const IR::Expression *TableStepper::computeTargetMatchType(ExecutionState &nextS
         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.createZombieConst(keyExpr->type, maskName);
+        const IR::Expression *maskVar = nextState.createSymbolicVariable(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);
@@ -338,14 +357,14 @@ void TableStepper::setTableDefaultEntries(
         std::vector<ActionArg> ctrlPlaneArgs;
         for (size_t argIdx = 0; argIdx < parameters->size(); ++argIdx) {
             const auto *parameter = parameters->getParameter(argIdx);
-            // Synthesize a zombie constant here that corresponds to a control plane argument.
+            // Synthesize a variables constant here that corresponds to a control plane argument.
             // We get the unique name of the table coupled with the unique name of the action.
             // Getting the unique name is needed to avoid generating duplicate arguments.
             const auto &actionDataVar =
-                Utils::getZombieTableVar(parameter->type, table, "*actionData", idx, argIdx);
+                getTableStateVariable(parameter->type, table, "*actionData", idx, argIdx);
             cstring paramName =
                 properties.tableName + "_arg_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createZombieConst(parameter->type, paramName);
+            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, paramName);
             nextState.set(actionDataVar, actionArg);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
@@ -417,14 +436,14 @@ void TableStepper::evalTableControlEntries(
         std::vector<ActionArg> ctrlPlaneArgs;
         for (size_t argIdx = 0; argIdx < parameters->size(); ++argIdx) {
             const auto *parameter = parameters->getParameter(argIdx);
-            // Synthesize a zombie constant here that corresponds to a control plane argument.
+            // Synthesize a variables constant here that corresponds to a control plane argument.
             // We get the unique name of the table coupled with the unique name of the action.
             // Getting the unique name is needed to avoid generating duplicate arguments.
             const auto &actionDataVar =
-                Utils::getZombieTableVar(parameter->type, table, "*actionData", idx, argIdx);
+                getTableStateVariable(parameter->type, table, "*actionData", idx, argIdx);
             cstring paramName =
                 properties.tableName + "_arg_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createZombieConst(parameter->type, paramName);
+            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, paramName);
             nextState.set(actionDataVar, actionArg);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
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 eccf38f2d72..b6f420a3687 100644
--- a/backends/p4tools/modules/testgen/core/small_step/table_stepper.h
+++ b/backends/p4tools/modules/testgen/core/small_step/table_stepper.h
@@ -67,6 +67,14 @@ class TableStepper {
     /* =========================================================================================
      * Table Variable Getter functions
      * ========================================================================================= */
+    /// @returns the variables variable with the given type, for tracking an aspect of the given
+    /// table. The returned variable will be named p4t*variables.table.t.name.idx1.idx2, where t is
+    /// the name of the given table. The "idx1" and "idx2" components are produced only if idx1 and
+    /// idx2 are given, respectively.
+    static const IR::StateVariable &getTableStateVariable(
+        const IR::Type *type, const IR::P4Table *table, cstring name,
+        std::optional<int> idx1_opt = std::nullopt, std::optional<int> idx2_opt = std::nullopt);
+
     /// @returns the boolean-typed state variable that tracks whether given table is reached.
     static const IR::StateVariable &getTableReachedVar(const IR::P4Table *table);
 
@@ -166,7 +174,7 @@ class TableStepper {
     /// executed.
     const IR::Expression *evalTableConstEntries();
 
-    /// This helper function evaluates potential insertion from the control plane. We use zombie
+    /// This helper function evaluates potential insertion from the control plane. We use variables
     /// variables to mimic an operator inserting entries. We only cover ONE entry per table for
     /// now.
     /// @param table the table we invoke.
diff --git a/backends/p4tools/modules/testgen/core/target.cpp b/backends/p4tools/modules/testgen/core/target.cpp
index a3c813c5acd..f5b12bfea52 100644
--- a/backends/p4tools/modules/testgen/core/target.cpp
+++ b/backends/p4tools/modules/testgen/core/target.cpp
@@ -4,7 +4,6 @@
 #include <utility>
 
 #include "backends/p4tools/common/core/target.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "ir/declaration.h"
 #include "ir/ir.h"
 #include "ir/node.h"
diff --git a/backends/p4tools/modules/testgen/core/target.h b/backends/p4tools/modules/testgen/core/target.h
index 3f44391c727..f363a1f268f 100644
--- a/backends/p4tools/modules/testgen/core/target.h
+++ b/backends/p4tools/modules/testgen/core/target.h
@@ -10,7 +10,6 @@
 #include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/core/target.h"
 #include "backends/p4tools/common/lib/arch_spec.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "ir/ir.h"
 #include "ir/vector.h"
 
diff --git a/backends/p4tools/modules/testgen/lib/concolic.cpp b/backends/p4tools/modules/testgen/lib/concolic.cpp
index 5e46a4552e9..79106129165 100644
--- a/backends/p4tools/modules/testgen/lib/concolic.cpp
+++ b/backends/p4tools/modules/testgen/lib/concolic.cpp
@@ -37,16 +37,16 @@ bool ConcolicMethodImpls::matches(const std::vector<cstring> &paramNames,
     return true;
 }
 
-bool ConcolicMethodImpls::exec(cstring qualifiedMethodName, const IR::ConcolicVariable *var,
+bool ConcolicMethodImpls::exec(cstring concolicMethodName, const IR::ConcolicVariable *var,
                                const ExecutionState &state, const Model &completedModel,
                                ConcolicVariableMap *resolvedConcolicVariables) const {
-    if (impls.count(qualifiedMethodName) == 0) {
+    if (impls.count(concolicMethodName) == 0) {
         return false;
     }
 
     const auto *args = var->arguments;
 
-    const auto &submap = impls.at(qualifiedMethodName);
+    const auto &submap = impls.at(concolicMethodName);
     if (submap.count(args->size()) == 0) {
         return false;
     }
@@ -58,7 +58,7 @@ bool ConcolicMethodImpls::exec(cstring qualifiedMethodName, const IR::ConcolicVa
         const auto &methodImpl = pair.second;
 
         if (matches(paramNames, args)) {
-            BUG_CHECK(!matchingImpl, "Ambiguous extern method call: %1%", qualifiedMethodName);
+            BUG_CHECK(!matchingImpl, "Ambiguous extern method call: %1%", concolicMethodName);
             matchingImpl = methodImpl;
         }
     }
@@ -66,7 +66,7 @@ bool ConcolicMethodImpls::exec(cstring qualifiedMethodName, const IR::ConcolicVa
     if (!matchingImpl) {
         return false;
     }
-    (*matchingImpl)(qualifiedMethodName, var, state, completedModel, resolvedConcolicVariables);
+    (*matchingImpl)(concolicMethodName, var, state, completedModel, resolvedConcolicVariables);
     return true;
 }
 
@@ -94,10 +94,9 @@ void ConcolicMethodImpls::add(const ImplList &inputImplList) {
 ConcolicMethodImpls::ConcolicMethodImpls(const ImplList &implList) { add(implList); }
 
 bool ConcolicResolver::preorder(const IR::ConcolicVariable *var) {
-    cstring concolicMethodName = var->concolicMethodName;
+    auto concolicMethodName = var->concolicMethodName;
     // Convert the concolic member variable to a state variable.
-    IR::StateVariable concolicVarName = var->concolicMember;
-    auto concolicReplacment = resolvedConcolicVariables.find(concolicVarName);
+    auto concolicReplacment = resolvedConcolicVariables.find(*var);
     if (concolicReplacment == resolvedConcolicVariables.end()) {
         bool found = concolicMethodImpls.exec(concolicMethodName, var, state, completedModel,
                                               &resolvedConcolicVariables);
@@ -126,10 +125,10 @@ ConcolicResolver::ConcolicResolver(const Model &completedModel, const ExecutionS
     visitDagOnce = false;
 }
 
-static const ConcolicMethodImpls::ImplList coreConcolicMethodImpls({});
+static const ConcolicMethodImpls::ImplList CORE_CONCOLIC_METHOD_IMPLS({});
 
 const ConcolicMethodImpls::ImplList *Concolic::getCoreConcolicMethodImpls() {
-    return &coreConcolicMethodImpls;
+    return &CORE_CONCOLIC_METHOD_IMPLS;
 }
 
 }  // namespace P4Tools::P4Testgen
diff --git a/backends/p4tools/modules/testgen/lib/concolic.h b/backends/p4tools/modules/testgen/lib/concolic.h
index a2189aaae1b..2bfd68722e0 100644
--- a/backends/p4tools/modules/testgen/lib/concolic.h
+++ b/backends/p4tools/modules/testgen/lib/concolic.h
@@ -21,14 +21,13 @@
 
 namespace P4Tools::P4Testgen {
 
-/// TODO: This is a very ugly data structure. Essentially, you can store both state variables and
-/// entire expression as keys. State variables can actually compared, expressions are always unique
-/// keys. Using this map, you can look up particular state variables and check whether they actually
-/// are present, but not expressions. The reason expressions need to be keys is that sometimes
-/// entire expressions are mapped to a particular constant.
+/// TODO: This is a very ugly data structure. Essentially, you can store both state variables
+/// and entire expression as keys. State variables can actually compared, expressions are always
+/// unique keys. Using this map, you can look up particular state variables and check whether
+/// they actually are present, but not expressions. The reason expressions need to be keys is
+/// that sometimes entire expressions are mapped to a particular constant.
 using ConcolicVariableMap =
-    ordered_map<std::variant<const IR::StateVariable, const IR::Expression *>,
-                const IR::Expression *>;
+    ordered_map<std::variant<IR::ConcolicVariable, const IR::Expression *>, const IR::Expression *>;
 
 /// Encapsulates a set of concolic method implementations.
 class ConcolicMethodImpls {
@@ -79,8 +78,8 @@ class ConcolicResolver : public Inspector {
     /// assertions are used to add constraints to the solver.
     ConcolicVariableMap resolvedConcolicVariables;
 
-    /// A reference to the list of implemented concolic methods. This is assembled by the testgen
-    /// targets.
+    /// A reference to the list of implemented concolic methods. This is assembled by the
+    /// testgen targets.
     const ConcolicMethodImpls &concolicMethodImpls;
 };
 
diff --git a/backends/p4tools/modules/testgen/lib/execution_state.cpp b/backends/p4tools/modules/testgen/lib/execution_state.cpp
index ac78b54e4a7..692f63f19d5 100644
--- a/backends/p4tools/modules/testgen/lib/execution_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/execution_state.cpp
@@ -19,7 +19,7 @@
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/taint.h"
 #include "backends/p4tools/common/lib/trace_event.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
 #include "ir/irutils.h"
@@ -28,35 +28,21 @@
 #include "lib/source_file.h"
 
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/lib/test_spec.h"
 #include "backends/p4tools/modules/testgen/options.h"
 
 namespace P4Tools::P4Testgen {
 
-const IR::Member ExecutionState::inputPacketLabel =
-    IR::Member(new IR::PathExpression("*"), "inputPacket");
-
-const IR::Member ExecutionState::packetBufferLabel =
-    IR::Member(new IR::PathExpression("*"), "packetBuffer");
-
-const IR::Member ExecutionState::emitBufferLabel =
-    IR::Member(new IR::PathExpression("*"), "emitBuffer");
-
-const IR::Member ExecutionState::payloadLabel = IR::Member(new IR::PathExpression("*"), "payload");
-
-// The methods in P4's packet_in uses 32-bit values. Conform with this to make it easier to produce
-// well-typed expressions when manipulating the parser cursor.
-const IR::Type_Bits ExecutionState::packetSizeVarType = IR::Type_Bits(32, false);
-
 ExecutionState::ExecutionState(const IR::P4Program *program)
     : namespaces(NamespaceContext::Empty->push(program)),
       body({program}),
       stack(*(new std::stack<std::reference_wrapper<const StackFrame>>())) {
-    // Insert the default zombies of the execution state.
-    // This also makes the zombies present in the state explicit.
-    allocatedZombies.insert(getInputPacketSizeVar());
-    env.set(&inputPacketLabel, IR::getConstant(IR::getBitType(0), 0));
-    env.set(&packetBufferLabel, IR::getConstant(IR::getBitType(0), 0));
+    // 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.
     setProperty("inUndefinedState", false);
     // Drop is initialized to false, too.
@@ -75,9 +61,9 @@ ExecutionState::ExecutionState(Continuation::Body body)
     : namespaces(NamespaceContext::Empty),
       body(std::move(body)),
       stack(*(new std::stack<std::reference_wrapper<const StackFrame>>())) {
-    // Insert the default zombies of the execution state.
-    // This also makes the zombies present in the state explicit.
-    allocatedZombies.insert(getInputPacketSizeVar());
+    // 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.
@@ -111,14 +97,14 @@ std::optional<const Continuation::Command> ExecutionState::getNextCmd() const {
 
 const IR::Expression *ExecutionState::get(const IR::StateVariable &var) const {
     const auto *expr = env.get(var);
-    if (var->expr->type->is<IR::Type_Header>() && var->member != Utils::Valid) {
+    if (var->expr->type->is<IR::Type_Header>() && var->member != ToolsVariables::VALID) {
         // If we are setting the member of a header, we need to check whether the
         // header is valid.
         // If the header is invalid, the get returns a tainted expression.
         // The member could have any value.
         // TODO: This is a convoluted check. We should be using runtime objects instead of flat
         // assignments.
-        auto validity = Utils::getHeaderValidity(var->expr);
+        auto validity = ToolsVariables::getHeaderValidity(var->expr);
         const auto *validVar = env.get(validity);
         // The validity bit could already be tainted or the validity bit is false.
         // Both outcomes lead to a tainted write.
@@ -127,7 +113,7 @@ const IR::Expression *ExecutionState::get(const IR::StateVariable &var) const {
             isTainted = !validBool->value;
         }
         if (isTainted) {
-            return Utils::getTaintExpression(expr->type);
+            return ToolsVariables::getTaintExpression(expr->type);
         }
     }
     return expr;
@@ -151,7 +137,7 @@ bool ExecutionState::exists(const IR::StateVariable &var) const { return env.exi
 void ExecutionState::set(const IR::StateVariable &var, const IR::Expression *value) {
     if (getProperty<bool>("inUndefinedState")) {
         // If we are in an undefined state, the variable we set is tainted.
-        value = Utils::getTaintExpression(value->type);
+        value = ToolsVariables::getTaintExpression(value->type);
     }
     env.set(var, value);
 }
@@ -346,15 +332,16 @@ void ExecutionState::pushPathConstraint(const IR::Expression *e) { pathConstrain
 
 void ExecutionState::pushBranchDecision(uint64_t bIdx) { selectedBranches.push_back(bIdx); }
 
-const IR::Type_Bits *ExecutionState::getPacketSizeVarType() { return &packetSizeVarType; }
-
-const IR::StateVariable &ExecutionState::getInputPacketSizeVar() {
-    return Utils::getZombieConst(getPacketSizeVarType(), 0, "*packetLen_bits");
+const IR::SymbolicVariable *ExecutionState::getInputPacketSizeVar() {
+    return ToolsVariables::getSymbolicVariable(&PacketVars::PACKET_SIZE_VAR_TYPE, 0,
+                                               "*packetLen_bits");
 }
 
 int ExecutionState::getMaxPacketLength() { return TestgenOptions::get().maxPktSize; }
 
-const IR::Expression *ExecutionState::getInputPacket() const { return env.get(&inputPacketLabel); }
+const IR::Expression *ExecutionState::getInputPacket() const {
+    return env.get(&PacketVars::INPUT_PACKET_LABEL);
+}
 
 int ExecutionState::getInputPacketSize() const {
     const auto *inputPkt = getInputPacket();
@@ -365,20 +352,20 @@ void ExecutionState::appendToInputPacket(const IR::Expression *expr) {
     const auto *inputPkt = getInputPacket();
     const auto *width = IR::getBitType(expr->type->width_bits() + inputPkt->type->width_bits());
     const auto *concat = new IR::Concat(width, inputPkt, expr);
-    env.set(&inputPacketLabel, concat);
+    env.set(&PacketVars::INPUT_PACKET_LABEL, concat);
 }
 
 void ExecutionState::prependToInputPacket(const IR::Expression *expr) {
     const auto *inputPkt = getInputPacket();
     const auto *width = IR::getBitType(expr->type->width_bits() + inputPkt->type->width_bits());
     const auto *concat = new IR::Concat(width, expr, inputPkt);
-    env.set(&inputPacketLabel, concat);
+    env.set(&PacketVars::INPUT_PACKET_LABEL, concat);
 }
 
 int ExecutionState::getInputPacketCursor() const { return inputPacketCursor; }
 
 const IR::Expression *ExecutionState::getPacketBuffer() const {
-    return env.get(&packetBufferLabel);
+    return env.get(&PacketVars::PACKET_BUFFER_LABEL);
 }
 
 int ExecutionState::getPacketBufferSize() const {
@@ -398,8 +385,8 @@ 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 =
-            createZombieConst(IR::getBitType(diff), "pktVar", allocatedZombies.size());
+        const IR::Expression *newVar = createSymbolicVariable(IR::getBitType(diff), "pktVar",
+                                                              allocatedSymbolicVariables.size());
         appendToInputPacket(newVar);
         // If the buffer was not empty, append the data we have consumed to the newly generated
         // content and reset the buffer.
@@ -411,7 +398,7 @@ const IR::Expression *ExecutionState::peekPacketBuffer(int amount) {
         }
         // We have peeked ahead of what is available. We need to add the content we have looked at
         // to our packet buffer, which can later be consumed.
-        env.set(&packetBufferLabel, newVar);
+        env.set(&PacketVars::PACKET_BUFFER_LABEL, newVar);
         return newVar;
     }
     // The buffer is large enough and we can grab a slice
@@ -441,8 +428,8 @@ 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 =
-            createZombieConst(IR::getBitType(diff), "pktVar", allocatedZombies.size());
+        const IR::Expression *newVar = createSymbolicVariable(IR::getBitType(diff), "pktVar",
+                                                              allocatedSymbolicVariables.size());
         appendToInputPacket(newVar);
         // If the buffer was not empty, append the data we have consumed to the newly generated
         // content and reset the buffer.
@@ -463,7 +450,7 @@ const IR::Expression *ExecutionState::slicePacketBuffer(int amount) {
     if (diff < 0) {
         auto *remainder = new IR::Slice(buffer, bufferSize - amount - 1, 0);
         remainder->type = IR::getBitType(bufferSize - amount);
-        env.set(&packetBufferLabel, remainder);
+        env.set(&PacketVars::PACKET_BUFFER_LABEL, remainder);
     }
     // The amount we slice is equal to what is in the buffer. Just set the buffer to zero.
     if (diff == 0) {
@@ -476,41 +463,33 @@ void ExecutionState::appendToPacketBuffer(const IR::Expression *expr) {
     const auto *buffer = getPacketBuffer();
     const auto *width = IR::getBitType(expr->type->width_bits() + buffer->type->width_bits());
     const auto *concat = new IR::Concat(width, buffer, expr);
-    env.set(&packetBufferLabel, concat);
+    env.set(&PacketVars::PACKET_BUFFER_LABEL, concat);
 }
 
 void ExecutionState::prependToPacketBuffer(const IR::Expression *expr) {
     const auto *buffer = getPacketBuffer();
     const auto *width = IR::getBitType(expr->type->width_bits() + buffer->type->width_bits());
     const auto *concat = new IR::Concat(width, expr, buffer);
-    env.set(&packetBufferLabel, concat);
+    env.set(&PacketVars::PACKET_BUFFER_LABEL, concat);
 }
 
 void ExecutionState::resetPacketBuffer() {
-    env.set(&packetBufferLabel, IR::getConstant(IR::getBitType(0), 0));
+    env.set(&PacketVars::PACKET_BUFFER_LABEL, IR::getConstant(IR::getBitType(0), 0));
 }
 
-const IR::Expression *ExecutionState::getEmitBuffer() const { return env.get(&emitBufferLabel); }
+const IR::Expression *ExecutionState::getEmitBuffer() const {
+    return env.get(&PacketVars::EMIT_BUFFER_LABEL);
+}
 
 void ExecutionState::resetEmitBuffer() {
-    env.set(&emitBufferLabel, IR::getConstant(IR::getBitType(0), 0));
+    env.set(&PacketVars::EMIT_BUFFER_LABEL, IR::getConstant(IR::getBitType(0), 0));
 }
 
 void ExecutionState::appendToEmitBuffer(const IR::Expression *expr) {
     const auto *buffer = getEmitBuffer();
     const auto *width = IR::getBitType(expr->type->width_bits() + buffer->type->width_bits());
     const auto *concat = new IR::Concat(width, buffer, expr);
-    env.set(&emitBufferLabel, concat);
-}
-
-const IR::Member *ExecutionState::getPayloadLabel(const IR::Type *t) {
-    // If the type is not null, we construct a member clone with the input type set.
-    if (t != nullptr) {
-        auto *label = payloadLabel.clone();
-        label->type = t;
-        return label;
-    }
-    return &payloadLabel;
+    env.set(&PacketVars::EMIT_BUFFER_LABEL, concat);
 }
 
 void ExecutionState::setParserErrorLabel(const IR::Member *parserError) {
@@ -526,19 +505,22 @@ const IR::Member *ExecutionState::getCurrentParserErrorLabel() const {
  *  Variables and symbolic constants
  * ============================================================================================= */
 
-const std::set<IR::StateVariable> &ExecutionState::getZombies() const { return allocatedZombies; }
+const SymbolicSet &ExecutionState::getSymbolicVariables() const {
+    return allocatedSymbolicVariables;
+}
 
-const IR::StateVariable &ExecutionState::createZombieConst(const IR::Type *type, cstring name,
-                                                           uint64_t instanceId) {
-    const auto &zombie = Utils::getZombieConst(type, instanceId, name);
-    const auto &result = allocatedZombies.insert(zombie);
-    // The zombie already existed, check its type.
+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 zombie variable %1%: previously %2%, but now %3%",
-                  zombie->toString(), (*result.first)->type, type);
+                  "Inconsistent types for variables variable %1%: previously %2%, but now %3%",
+                  variables->toString(), (*result.first)->type, type);
     }
-    return zombie;
+    return variables;
 }
 
 /* =========================================================================================
@@ -574,7 +556,7 @@ std::vector<const IR::Member *> ExecutionState::getFlatFields(
     // If we are dealing with a header we also include the validity bit in the list of
     // fields.
     if (validVector != nullptr && ts->is<IR::Type_Header>()) {
-        validVector->push_back(Utils::getHeaderValidity(parent));
+        validVector->push_back(ToolsVariables::getHeaderValidity(parent));
     }
     return flatFields;
 }
@@ -606,20 +588,8 @@ const IR::P4Action *ExecutionState::getActionDecl(const IR::Expression *expressi
     }
     return expression->to<IR::P4Action>();
 }
-
-const IR::StateVariable &ExecutionState::convertPathExpr(const IR::PathExpression *path) const {
-    const auto *decl = findDecl(path)->getNode();
-    // Local variable.
-    if (const auto *declVar = decl->to<IR::Declaration_Variable>()) {
-        return Utils::getZombieVar(path->type, 0, declVar->name.name);
-    }
-    if (const auto *declInst = decl->to<IR::Declaration_Instance>()) {
-        return Utils::getZombieVar(path->type, 0, declInst->name.name);
-    }
-    if (const auto *param = decl->to<IR::Parameter>()) {
-        return Utils::getZombieVar(path->type, 0, param->name.name);
-    }
-    BUG("Unsupported declaration %1% of type %2%.", decl, decl->node_type_name());
+const IR::StateVariable &ExecutionState::convertPathExpr(const IR::PathExpression *path) {
+    return ToolsVariables::getStateVariable(path->type, path->path->name);
 }
 
 ExecutionState &ExecutionState::create(const IR::P4Program *program) {
diff --git a/backends/p4tools/modules/testgen/lib/execution_state.h b/backends/p4tools/modules/testgen/lib/execution_state.h
index 11a4e67a09c..cf283219b59 100644
--- a/backends/p4tools/modules/testgen/lib/execution_state.h
+++ b/backends/p4tools/modules/testgen/lib/execution_state.h
@@ -7,13 +7,13 @@
 #include <iostream>
 #include <map>
 #include <optional>
-#include <set>
 #include <stack>
 #include <utility>
 #include <variant>
 #include <vector>
 
 #include "backends/p4tools/common/compiler/reachability.h"
+#include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/lib/namespace_context.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event.h"
@@ -33,29 +33,6 @@ namespace P4Tools::P4Testgen {
 class ExecutionState {
     friend class Test::SmallStepTest;
 
-    /// Specifies the type of the packet size variable.
-    /// This is mostly used to generate bit vector constants.
-    static const IR::Type_Bits packetSizeVarType;
-
-    /// The name of the input packet. The input packet defines the minimum size of the packet
-    /// requires to pass this particular path. Typically, calls such as extract, advance, or
-    /// lookahead cause the input packet to grow.
-    static const IR::Member inputPacketLabel;
-
-    /// The name of packet buffer. The packet buffer defines the data that can be consumed by the
-    /// parser. If the packet buffer is empty, extract/advance/lookahead calls will cause the
-    /// minimum packet size to grow. The packet buffer also forms the final output packet.
-    static const IR::Member packetBufferLabel;
-
-    /// The name of the emit buffer. Each time, emit is called, the emitted content is appended to
-    /// this buffer. Typically, after exiting the control, the emit buffer is appended to the packet
-    /// buffer.
-    static const IR::Member emitBufferLabel;
-
-    /// Canonical name for the payload. This is used for consistent naming when attaching a payload
-    /// to the packet.
-    static const IR::Member payloadLabel;
-
  public:
     class StackFrame {
      public:
@@ -75,6 +52,11 @@ class ExecutionState {
               namespaces(namespaces) {}
     };
 
+    /// No move semantics because of constant members. We always need to clone a state.
+    ExecutionState(ExecutionState &&) = delete;
+    ExecutionState &operator=(ExecutionState &&) = delete;
+    ~ExecutionState() = default;
+
  private:
     /// The namespace context in the IR for the current state. The innermost element is the P4
     /// program, representing the top-level namespace.
@@ -83,9 +65,9 @@ class ExecutionState {
     /// The symbolic environment. Maps program variables to their symbolic values.
     SymbolicEnv env;
 
-    /// The list of zombies that have been created in this state.
-    /// These zombies are later fed to the model for completion.
-    std::set<IR::StateVariable> allocatedZombies;
+    /// The list of variabless that have been created in this state.
+    /// These variabless 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;
@@ -169,7 +151,7 @@ class ExecutionState {
     [[nodiscard]] std::optional<const Continuation::Command> getNextCmd() const;
 
     /// @returns the symbolic value of the given state variable.
-    const IR::Expression *get(const IR::StateVariable &var) const;
+    [[nodiscard]] const IR::Expression *get(const IR::StateVariable &var) const;
 
     /// Checks whether the statement has been visited in this state.
     void markVisited(const IR::Statement *stmt);
@@ -182,7 +164,7 @@ class ExecutionState {
     void set(const IR::StateVariable &var, const IR::Expression *value);
 
     /// Checks whether the given variable exists in the symbolic environment of this state.
-    bool exists(const IR::StateVariable &var) const;
+    [[nodiscard]] bool exists(const IR::StateVariable &var) const;
 
     /// @see Taint::hasTaint
     bool hasTaint(const IR::Expression *expr) const;
@@ -352,12 +334,9 @@ class ExecutionState {
      *  Packet manipulation
      * ========================================================================================= */
  public:
-    /// @returns the bit type of the parser cursor.
-    [[nodiscard]] static const IR::Type_Bits *getPacketSizeVarType();
-
     /// @returns the symbolic constant representing the length of the input to the current parser,
     /// in bits.
-    static const IR::StateVariable &getInputPacketSizeVar();
+    static const IR::SymbolicVariable *getInputPacketSizeVar();
 
     /// @returns the maximum length, in bits, of the packet in the current packet buffer. This is
     /// the network's MTU.
@@ -385,8 +364,9 @@ class ExecutionState {
     [[nodiscard]] int getPacketBufferSize() const;
 
     /// Consumes and @returns a slice from the available packet buffer. If the buffer is empty, this
-    /// will produce zombie constants that are appended to the input packet. This means we generate
-    /// packet content as needed. The returned slice is optional in case one just needs to advance.
+    /// will produce variables constants that are appended to the input packet. This means we
+    /// generate packet content as needed. The returned slice is optional in case one just needs to
+    /// advance.
     const IR::Expression *slicePacketBuffer(int amount);
 
     /// Peeks ahead into the packet buffer. Works similarly to slicePacketBuffer but does NOT
@@ -413,10 +393,6 @@ class ExecutionState {
     /// Append data to the emit buffer.
     void appendToEmitBuffer(const IR::Expression *expr);
 
-    /// @returns the label associated with the payload and sets the type according to the @param.
-    /// TODO: Consider moving this to a separate utility class?
-    [[nodiscard]] static const IR::Member *getPayloadLabel(const IR::Type *t);
-
     /// Set the parser error label to the @param parserError.
     void setParserErrorLabel(const IR::Member *parserError);
 
@@ -430,13 +406,15 @@ class ExecutionState {
      *  based on how many times newParser() has been called.
      */
  public:
-    /// @returns the zombies that were allocated in this state
-    [[nodiscard]] const std::set<IR::StateVariable> &getZombies() const;
+    /// @returns the symbolic variables that were allocated in this state
+    [[nodiscard]] const SymbolicSet &getSymbolicVariables() const;
 
-    /// @see Utils::getZombieConst.
-    /// We also place the zombies in the set of allocated zombies of this state.
-    [[nodiscard]] const IR::StateVariable &createZombieConst(const IR::Type *type, cstring name,
-                                                             uint64_t instanceID = 0);
+    /// @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);
 
     /* =========================================================================================
      *  General utilities involving ExecutionState.
@@ -461,10 +439,10 @@ class ExecutionState {
 
     /// @returns a translation of the path expression into a member.
     /// This function looks up the path expression in the namespace and tries to find the
-    /// corresponding declaration. It then converts the name of the declaration into a zombie
+    /// corresponding declaration. It then converts the name of the declaration into a variables
     /// constant and returns. This is necessary because we sometimes
     /// get flat declarations without members (e.g., bit<8> tmp;)
-    [[nodiscard]] const IR::StateVariable &convertPathExpr(const IR::PathExpression *path) const;
+    [[nodiscard]] static const IR::StateVariable &convertPathExpr(const IR::PathExpression *path);
 
     /// Allocate a new execution state object with the same state as this object.
     /// Returns a reference, not a pointer.
diff --git a/backends/p4tools/modules/testgen/lib/final_state.cpp b/backends/p4tools/modules/testgen/lib/final_state.cpp
index ef8ee352e55..ab1db0add99 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/final_state.cpp
@@ -1,44 +1,129 @@
 #include "backends/p4tools/modules/testgen/lib/final_state.h"
 
+#include <list>
+#include <utility>
+#include <variant>
 #include <vector>
 
+#include <boost/container/vector.hpp>
+
 #include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event.h"
+#include "backends/p4tools/common/lib/util.h"
+#include "frontends/p4/optimizeExpressions.h"
+#include "ir/ir.h"
+#include "ir/irutils.h"
+#include "lib/error.h"
+#include "lib/null.h"
 
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 
 namespace P4Tools::P4Testgen {
 
-FinalState::FinalState(AbstractSolver &solver, const ExecutionState &inputState)
+FinalState::FinalState(AbstractSolver &solver, const ExecutionState &finalState)
     : solver(solver),
-      state(inputState),
-      completedModel(completeModel(inputState, solver.getModel())) {
-    for (const auto &event : inputState.getTrace()) {
+      state(finalState),
+      completedModel(completeModel(finalState, new Model(solver.getSymbolicMapping()))) {
+    for (const auto &event : finalState.getTrace()) {
+        trace.emplace_back(*event.get().evaluate(completedModel));
+    }
+}
+
+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));
     }
 }
 
-Model FinalState::completeModel(const ExecutionState &executionState, const Model *model) {
+void FinalState::calculatePayload(const ExecutionState &executionState, Model &evaluatedModel) {
+    const auto &packetBitSizeVar = ExecutionState::getInputPacketSizeVar();
+    const auto *payloadSizeConst = evaluatedModel.evaluate(packetBitSizeVar);
+    int calculatedPacketSize = IR::getIntFromLiteral(payloadSizeConst);
+    const auto *inputPacketExpr = executionState.getInputPacket();
+    int payloadSize = calculatedPacketSize - inputPacketExpr->type->width_bits();
+    if (payloadSize > 0) {
+        const auto *payloadType = IR::getBitType(payloadSize);
+        const IR::Expression *payloadExpr = evaluatedModel.get(&PacketVars::PAYLOAD_LABEL, false);
+        if (payloadExpr == nullptr) {
+            payloadExpr = Utils::getRandConstantForType(payloadType);
+            evaluatedModel.emplace(&PacketVars::PAYLOAD_LABEL, payloadExpr);
+        }
+    }
+}
+
+Model &FinalState::completeModel(const ExecutionState &finalState, const Model *model,
+                                 bool postProcess) {
     // Complete the model based on the symbolic environment.
-    auto *completedModel = executionState.getSymbolicEnv().complete(*model);
+    auto *completedModel = finalState.getSymbolicEnv().complete(*model);
 
-    // Also complete all the zombies that were collected in this state.
-    const auto &zombies = executionState.getZombies();
-    completedModel->complete(zombies);
+    // 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 = executionState.getSymbolicEnv().evaluate(*completedModel);
+    auto *evaluatedModel = finalState.getSymbolicEnv().evaluate(*completedModel);
 
-    for (const auto &event : executionState.getTrace()) {
+    if (postProcess) {
+        // Append a payload, if requested.
+        calculatePayload(finalState, *evaluatedModel);
+    }
+    for (const auto &event : finalState.getTrace()) {
         event.get().complete(evaluatedModel);
     }
 
     return *evaluatedModel;
 }
 
+std::optional<std::reference_wrapper<const FinalState>> FinalState::computeConcolicState(
+    const ConcolicVariableMap &resolvedConcolicVariables) const {
+    // If there are no new concolic variables, there is nothing to do.
+    if (resolvedConcolicVariables.empty()) {
+        return *this;
+    }
+    std::vector<const Constraint *> asserts = state.get().getPathConstraint();
+
+    for (const auto &resolvedConcolicVariable : resolvedConcolicVariables) {
+        const auto &concolicVariable = resolvedConcolicVariable.first;
+        const auto *concolicAssignment = resolvedConcolicVariable.second;
+        const IR::Expression *pathConstraint = nullptr;
+        // We need to differentiate between state variables and expressions here.
+        if (std::holds_alternative<IR::ConcolicVariable>(concolicVariable)) {
+            pathConstraint = new IR::Equ(std::get<IR::ConcolicVariable>(concolicVariable).clone(),
+                                         concolicAssignment);
+        } else if (std::holds_alternative<const IR::Expression *>(concolicVariable)) {
+            pathConstraint =
+                new IR::Equ(std::get<const IR::Expression *>(concolicVariable), concolicAssignment);
+        }
+        CHECK_NULL(pathConstraint);
+        pathConstraint = state.get().getSymbolicEnv().subst(pathConstraint);
+        pathConstraint = P4::optimizeExpression(pathConstraint);
+        asserts.push_back(pathConstraint);
+    }
+    auto solverResult = solver.get().checkSat(asserts);
+    if (!solverResult) {
+        ::warning("Timed out trying to solve this concolic execution path.");
+        return std::nullopt;
+    }
+
+    if (!*solverResult) {
+        ::warning("Concolic constraints for this path are unsatisfiable.");
+        return std::nullopt;
+    }
+    auto &model = completeModel(state, new Model(solver.get().getSymbolicMapping()), false);
+    /// Transfer any derived variables from that are missing  in this model.
+    /// Do NOT update any variables that already exist.
+    for (const auto &varTuple : completedModel) {
+        model.emplace(varTuple.first, varTuple.second);
+    }
+    return *new FinalState(solver, state, model);
+}
+
 const Model *FinalState::getCompletedModel() const { return &completedModel; }
 
 AbstractSolver &FinalState::getSolver() const { return solver; }
@@ -50,5 +135,4 @@ const std::vector<std::reference_wrapper<const TraceEvent>> *FinalState::getTrac
 }
 
 const P4::Coverage::CoverageSet &FinalState::getVisited() const { return state.get().getVisited(); }
-
 }  // namespace P4Tools::P4Testgen
diff --git a/backends/p4tools/modules/testgen/lib/final_state.h b/backends/p4tools/modules/testgen/lib/final_state.h
index dca83ec2309..24376258f1e 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.h
+++ b/backends/p4tools/modules/testgen/lib/final_state.h
@@ -2,6 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_FINAL_STATE_H_
 
 #include <functional>
+#include <optional>
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
@@ -9,6 +10,7 @@
 #include "backends/p4tools/common/lib/trace_event.h"
 #include "midend/coverage.h"
 
+#include "backends/p4tools/modules/testgen/lib/concolic.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
 
 namespace P4Tools::P4Testgen {
@@ -24,18 +26,39 @@ class FinalState {
     std::reference_wrapper<const ExecutionState> state;
 
     /// The final model which has been augmented with environment completions.
-    const Model completedModel;
+    const Model &completedModel;
 
     /// The final program trace.
     std::vector<std::reference_wrapper<const TraceEvent>> trace;
 
- public:
-    FinalState(AbstractSolver &solver, const ExecutionState &inputState);
+    /// If the calculated payload size (the size of the symbolic packet size variable minus the size
+    /// of the input packet) is not negative, create a randomly sized payload and add the variable
+    /// to the model. Only do this if the payload has not been set yet.
+    static void calculatePayload(const ExecutionState &executionState, Model &evaluatedModel);
 
     /// Complete the model according to target-specific completion criteria.
     /// We first complete (this means we fill all the variables that have not been bound).
     /// Then we evaluate the model (we assign values to the variables that have been bound).
-    static Model completeModel(const ExecutionState &executionState, const Model *model);
+    static Model &completeModel(const ExecutionState &finalState, const Model *model,
+                                bool postProcess = true);
+
+ public:
+    /// This constructor invokes @function completeModel() to produce the model based on the solver
+    /// and the executionState.
+    FinalState(AbstractSolver &solver, const ExecutionState &finalState);
+
+    /// This constructor takes the input model as is and does not invoke @function completeModel().
+    FinalState(AbstractSolver &solver, const ExecutionState &finalState,
+               const Model &completedModel);
+
+    /// If there are concolic variables in the program, compute a new final state by rerunning the
+    /// solver on the concolic assignments. If the concolic assignment is not satisfiable, return
+    /// std::nullopt. Otherwise, create a new final state with the new assignment. IMPORTANT: Some
+    /// variables in this final state may have been added in post, e.g., the payload size. If the
+    /// concolic variables do not recompute these variables, the model will simply copy these
+    /// variables over manually to the newly generated model.
+    [[nodiscard]] std::optional<std::reference_wrapper<const FinalState>> computeConcolicState(
+        const ConcolicVariableMap &resolvedConcolicVariables) const;
 
     /// @returns the model after it was augmented by completions from the symbolic environment.
     [[nodiscard]] const Model *getCompletedModel() const;
diff --git a/backends/p4tools/modules/testgen/lib/packet_vars.cpp b/backends/p4tools/modules/testgen/lib/packet_vars.cpp
new file mode 100644
index 00000000000..dddf0dc562e
--- /dev/null
+++ b/backends/p4tools/modules/testgen/lib/packet_vars.cpp
@@ -0,0 +1,22 @@
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
+
+#include "ir/id.h"
+
+namespace P4Tools::P4Testgen {
+
+// The methods in P4's packet_in uses 32-bit values. Conform with this to make it easier to produce
+// well-typed expressions when manipulating the parser cursor.
+const IR::Type_Bits PacketVars::PACKET_SIZE_VAR_TYPE = IR::Type_Bits(32, false);
+
+const IR::Member PacketVars::INPUT_PACKET_LABEL =
+    IR::Member(new IR::PathExpression("*"), "inputPacket");
+
+const IR::Member PacketVars::PACKET_BUFFER_LABEL =
+    IR::Member(new IR::PathExpression("*"), "packetBuffer");
+
+const IR::Member PacketVars::EMIT_BUFFER_LABEL =
+    IR::Member(new IR::PathExpression("*"), "emitBuffer");
+
+const IR::Member PacketVars::PAYLOAD_LABEL = IR::Member(new IR::PathExpression("*"), "payload");
+
+}  // namespace P4Tools::P4Testgen
diff --git a/backends/p4tools/modules/testgen/lib/packet_vars.h b/backends/p4tools/modules/testgen/lib/packet_vars.h
new file mode 100644
index 00000000000..92fa18dfe82
--- /dev/null
+++ b/backends/p4tools/modules/testgen/lib/packet_vars.h
@@ -0,0 +1,38 @@
+#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_PACKET_VARS_H_
+#define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_PACKET_VARS_H_
+
+#include "ir/ir.h"
+
+namespace P4Tools::P4Testgen {
+
+/// Contains utility functions and variables related to the creation and manipulation of input
+/// packets.
+class PacketVars {
+ public:
+    /// Specifies the type of the packet size variable.
+    /// This is mostly used to generate bit vector constants.
+    static const IR::Type_Bits PACKET_SIZE_VAR_TYPE;
+
+    /// The name of the input packet. The input packet defines the minimum size of the packet
+    /// requires to pass this particular path. Typically, calls such as extract, advance, or
+    /// lookahead cause the input packet to grow.
+    static const IR::Member INPUT_PACKET_LABEL;
+
+    /// The name of packet buffer. The packet buffer defines the data that can be consumed by the
+    /// parser. If the packet buffer is empty, extract/advance/lookahead calls will cause the
+    /// minimum packet size to grow. The packet buffer also forms the final output packet.
+    static const IR::Member PACKET_BUFFER_LABEL;
+
+    /// The name of the emit buffer. Each time, emit is called, the emitted content is appended to
+    /// this buffer. Typically, after exiting the control, the emit buffer is appended to the packet
+    /// buffer.
+    static const IR::Member EMIT_BUFFER_LABEL;
+
+    /// Canonical name for the payload. This is used for consistent naming when attaching a payload
+    /// to the packet.
+    static const IR::Member PAYLOAD_LABEL;
+};
+
+}  // namespace P4Tools::P4Testgen
+
+#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_PACKET_VARS_H_ */
diff --git a/backends/p4tools/modules/testgen/lib/test_backend.cpp b/backends/p4tools/modules/testgen/lib/test_backend.cpp
index 1870bd74e8b..f2f040f59d1 100644
--- a/backends/p4tools/modules/testgen/lib/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/lib/test_backend.cpp
@@ -1,23 +1,16 @@
 #include "backends/p4tools/modules/testgen/lib/test_backend.h"
 
 #include <iostream>
-#include <list>
 #include <optional>
-#include <utility>
-#include <variant>
 
-#include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/core/z3_solver.h"
 #include "backends/p4tools/common/lib/format_int.h"
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/taint.h"
 #include "backends/p4tools/common/lib/trace_event.h"
 #include "backends/p4tools/common/lib/util.h"
-#include "frontends/p4/optimizeExpressions.h"
 #include "ir/irutils.h"
 #include "lib/cstring.h"
-#include "lib/error.h"
 #include "lib/exceptions.h"
 #include "lib/log.h"
 #include "lib/null.h"
@@ -30,67 +23,13 @@
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
 #include "backends/p4tools/modules/testgen/lib/final_state.h"
 #include "backends/p4tools/modules/testgen/lib/logging.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/lib/test_spec.h"
 #include "backends/p4tools/modules/testgen/lib/tf.h"
 #include "backends/p4tools/modules/testgen/options.h"
 
 namespace P4Tools::P4Testgen {
 
-const Model *TestBackEnd::computeConcolicVariables(const ExecutionState *executionState,
-                                                   const Model *completedModel, Z3Solver *solver,
-                                                   const IR::Expression *outputPacketExpr,
-                                                   const IR::Expression *outputPortExpr) const {
-    // Execute concolic functions that may occur in the output packet, the output port,
-    // or any path conditions.
-    auto concolicResolver =
-        ConcolicResolver(*completedModel, *executionState, *programInfo.getConcolicMethodImpls());
-
-    outputPacketExpr->apply(concolicResolver);
-    outputPortExpr->apply(concolicResolver);
-    for (const auto *assert : executionState->getPathConstraint()) {
-        CHECK_NULL(assert);
-        assert->apply(concolicResolver);
-    }
-    const auto *resolvedConcolicVariables = concolicResolver.getResolvedConcolicVariables();
-
-    // If we resolved concolic variables and substitute them, check the solver again under
-    // the new constraints.
-    if (!resolvedConcolicVariables->empty()) {
-        std::vector<const Constraint *> asserts = executionState->getPathConstraint();
-
-        for (const auto &resolvedConcolicVariable : *resolvedConcolicVariables) {
-            const auto &concolicVariable = resolvedConcolicVariable.first;
-            const auto *concolicAssignment = resolvedConcolicVariable.second;
-            const IR::Expression *pathConstraint = nullptr;
-            // We need to differentiate between state variables and expressions here.
-            if (std::holds_alternative<const IR::StateVariable>(concolicVariable)) {
-                pathConstraint = new IR::Equ(std::get<const IR::StateVariable>(concolicVariable),
-                                             concolicAssignment);
-            } else if (std::holds_alternative<const IR::Expression *>(concolicVariable)) {
-                pathConstraint = new IR::Equ(std::get<const IR::Expression *>(concolicVariable),
-                                             concolicAssignment);
-            }
-            CHECK_NULL(pathConstraint);
-            pathConstraint = executionState->getSymbolicEnv().subst(pathConstraint);
-            pathConstraint = P4::optimizeExpression(pathConstraint);
-            asserts.push_back(pathConstraint);
-        }
-        auto solverResult = solver->checkSat(asserts);
-        if (!solverResult) {
-            ::warning("Timed out trying to solve this concolic execution path.");
-            return nullptr;
-        }
-
-        if (!*solverResult) {
-            ::warning("Concolic constraints for this path are unsatisfiable.");
-            return nullptr;
-        }
-        const auto *concolicFinalState = new FinalState(*solver, *executionState);
-        completedModel = concolicFinalState->getCompletedModel();
-    }
-    return completedModel;
-}
-
 bool TestBackEnd::run(const FinalState &state) {
     {
         // Evaluate the model and extract the input and output packets.
@@ -99,9 +38,7 @@ bool TestBackEnd::run(const FinalState &state) {
         const auto *completedModel = state.getCompletedModel();
         const auto *outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
         const auto &allStatements = programInfo.getAllStatements();
-
-        auto *solver = state.getSolver().to<Z3Solver>();
-        CHECK_NULL(solver);
+        const auto *programTraces = state.getTraces();
 
         // Don't increase the test count if --with-output-packet is enabled and we don't
         // produce a test with an output packet.
@@ -123,16 +60,34 @@ bool TestBackEnd::run(const FinalState &state) {
         }
 
         bool abort = false;
-        const auto *concolicModel = computeConcolicVariables(executionState, completedModel, solver,
-                                                             outputPacketExpr, outputPortExpr);
-        if (concolicModel == nullptr) {
+
+        // Execute concolic functions that may occur in the output packet, the output port,
+        // or any path conditions.
+        auto concolicResolver = ConcolicResolver(*completedModel, *executionState,
+                                                 *programInfo.getConcolicMethodImpls());
+
+        outputPacketExpr->apply(concolicResolver);
+        outputPortExpr->apply(concolicResolver);
+        for (const auto *assert : executionState->getPathConstraint()) {
+            CHECK_NULL(assert);
+            assert->apply(concolicResolver);
+        }
+        const ConcolicVariableMap *resolvedConcolicVariables =
+            concolicResolver.getResolvedConcolicVariables();
+        // If we resolved concolic variables and substitute them, check the solver again under
+        // the new constraints.
+        auto concolicOptState = state.computeConcolicState(*resolvedConcolicVariables);
+        if (!concolicOptState.has_value()) {
             testCount++;
             printPerformanceReport(false);
             return needsToTerminate(testCount);
         }
-        completedModel = concolicModel;
+        auto replacedState = concolicOptState.value().get();
+        executionState = replacedState.getExecutionState();
+        outputPacketExpr = executionState->getPacketBuffer();
+        completedModel = replacedState.getCompletedModel();
+        outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
 
-        const auto *programTraces = state.getTraces();
         auto testInfo = produceTestInfo(executionState, completedModel, outputPacketExpr,
                                         outputPortExpr, programTraces);
 
@@ -152,7 +107,7 @@ bool TestBackEnd::run(const FinalState &state) {
 
         // Commit an update to the visited statements.
         // Only do this once we are sure we are generating a test.
-        symbex.updateVisitedStatements(state.getVisited());
+        symbex.updateVisitedStatements(replacedState.getVisited());
         const P4::Coverage::CoverageSet &visitedStatements = symbex.getVisitedStatements();
         auto coverage =
             static_cast<float>(visitedStatements.size()) / static_cast<float>(allStatements.size());
@@ -190,27 +145,18 @@ TestBackEnd::TestInfo TestBackEnd::produceTestInfo(
     const auto *inputPacketExpr = executionState->getInputPacket();
     // The payload fills the space between the minimum input size needed and the symbolically
     // calculated packet size.
-    int payloadSize = calculatedPacketSize - inputPacketExpr->type->width_bits();
-    if (payloadSize > 0) {
-        const auto *payloadType = IR::getBitType(payloadSize);
-        const auto *payloadExpr =
-            completedModel->get(ExecutionState::getPayloadLabel(payloadType), false);
-        if (payloadExpr == nullptr) {
-            payloadExpr = Utils::getRandConstantForType(payloadType);
-        }
-        BUG_CHECK(payloadExpr->type->width_bits() == payloadSize,
-                  "The width (%1%) of the payload expression should match the calculated payload "
-                  "size %2%.",
-                  payloadExpr->type->width_bits(), payloadSize);
+    const auto *payloadExpr = completedModel->get(&PacketVars::PAYLOAD_LABEL, false);
+    if (payloadExpr != nullptr) {
         inputPacketExpr =
             new IR::Concat(IR::getBitType(calculatedPacketSize), inputPacketExpr, payloadExpr);
-        outputPacketExpr =
-            new IR::Concat(IR::getBitType(outputPacketExpr->type->width_bits() + payloadSize),
-                           outputPacketExpr, payloadExpr);
+        outputPacketExpr = new IR::Concat(
+            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 *inputPort = completedModel->evaluate(programInfo.getTargetInputPortVar());
+    const auto *inputPort =
+        completedModel->evaluate(executionState->get(programInfo.getTargetInputPortVar()));
 
     const auto *outputPortVar = completedModel->evaluate(outputPortExpr);
     // Build the taint mask by dissecting the program packet variable
diff --git a/backends/p4tools/modules/testgen/lib/test_backend.h b/backends/p4tools/modules/testgen/lib/test_backend.h
index 2225808611a..958bd6c185d 100644
--- a/backends/p4tools/modules/testgen/lib/test_backend.h
+++ b/backends/p4tools/modules/testgen/lib/test_backend.h
@@ -4,9 +4,9 @@
 #include <stdint.h>
 
 #include <functional>
+#include <optional>
 #include <vector>
 
-#include "backends/p4tools/common/core/z3_solver.h"
 #include "backends/p4tools/common/lib/model.h"
 #include "backends/p4tools/common/lib/trace_event.h"
 #include "ir/ir.h"
@@ -97,10 +97,8 @@ class TestBackEnd {
                                const IR::Expression *outputPortExpr);
 
     /// @returns a new modules with all concolic variables in the program resolved.
-    const Model *computeConcolicVariables(const ExecutionState *executionState,
-                                          const Model *completedModel, Z3Solver *solver,
-                                          const IR::Expression *outputPacketExpr,
-                                          const IR::Expression *outputPortExpr) const;
+    [[nodiscard]] std::optional<std::reference_wrapper<const FinalState>> computeConcolicVariables(
+        const FinalState &state) const;
 
     /// @returns a TestInfo objects, which contains information about the input/output ports, the
     /// taint mask, the packet sizes, etc...
diff --git a/backends/p4tools/modules/testgen/lib/tf.h b/backends/p4tools/modules/testgen/lib/tf.h
index c15e7213403..94403f78ec8 100644
--- a/backends/p4tools/modules/testgen/lib/tf.h
+++ b/backends/p4tools/modules/testgen/lib/tf.h
@@ -2,6 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TF_H_
 
 #include <cstddef>
+#include <filesystem>
 #include <functional>
 #include <iosfwd>
 #include <map>
diff --git a/backends/p4tools/modules/testgen/main.cpp b/backends/p4tools/modules/testgen/main.cpp
index adf2fdaa112..eaeeafb5b19 100644
--- a/backends/p4tools/modules/testgen/main.cpp
+++ b/backends/p4tools/modules/testgen/main.cpp
@@ -1,3 +1,7 @@
+#include <exception>
+#include <iostream>
+#include <vector>
+
 #include "lib/crash.h"
 #include "lib/exceptions.h"
 
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp
index 200e31d95be..a85f712b2d3 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.cpp
@@ -1,6 +1,7 @@
 #include "backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.h"
 
 #include <algorithm>
+#include <functional>
 #include <iomanip>
 #include <map>
 #include <string>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.h b/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.h
index 6c65398bea6..8a96aec0307 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/metadata/metadata.h
@@ -2,6 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_BACKEND_METADATA_METADATA_H_
 
 #include <cstddef>
+#include <filesystem>
 #include <fstream>
 #include <optional>
 #include <string>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp
index 482f6398350..725f8640042 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.cpp
@@ -2,6 +2,7 @@
 
 #include <algorithm>
 #include <filesystem>
+#include <fstream>
 #include <iomanip>
 #include <map>
 #include <optional>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.h b/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.h
index f8bd69d7f7e..6c6d9ca6a92 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/protobuf/protobuf.h
@@ -2,7 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_BACKEND_PROTOBUF_PROTOBUF_H_
 
 #include <cstddef>
-#include <fstream>
+#include <filesystem>
 #include <optional>
 #include <string>
 #include <utility>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.h b/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.h
index f30a07e7ebb..e0307b13e63 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.h
@@ -2,6 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_BACKEND_PTF_PTF_H_
 
 #include <cstddef>
+#include <filesystem>
 #include <fstream>
 #include <map>
 #include <optional>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp b/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp
index 5e00a684cc4..54033f503bd 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.cpp
@@ -1,5 +1,6 @@
 #include "backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.h"
 
+#include <fstream>
 #include <iomanip>
 #include <map>
 #include <optional>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.h b/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.h
index f65eccca328..d0240d4e829 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/backend/stf/stf.h
@@ -2,7 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_BACKEND_STF_STF_H_
 
 #include <cstddef>
-#include <fstream>
+#include <filesystem>
 #include <map>
 #include <optional>
 #include <string>
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp
index 73618a24350..d8be6f5badb 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/cmd_stepper.cpp
@@ -23,6 +23,7 @@
 #include "backends/p4tools/modules/testgen/core/target.h"
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/options.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/constants.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/program_info.h"
@@ -77,7 +78,7 @@ void Bmv2V1ModelCmdStepper::initializeTargetEnvironment(ExecutionState &nextStat
     const auto *nineBitType = IR::getBitType(9);
     const auto *oneBitType = IR::getBitType(1);
     nextState.set(programInfo.getTargetInputPortVar(),
-                  nextState.createZombieConst(nineBitType, "*bmv2_ingress_port"));
+                  nextState.createSymbolicVariable(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.
@@ -90,7 +91,7 @@ void Bmv2V1ModelCmdStepper::initializeTargetEnvironment(ExecutionState &nextStat
         new IR::Member(oneBitType, new IR::PathExpression("*standard_metadata"), "checksum_error");
     nextState.set(checksumErrVar, IR::getConstant(checksumErrVar->type, 0));
     // The packet size meta data is the testgen packet length variable divided by 8.
-    const auto *pktSizeType = ExecutionState::getPacketSizeVarType();
+    const auto *pktSizeType = &PacketVars::PACKET_SIZE_VAR_TYPE;
     const auto *packetSizeVar =
         new IR::Member(pktSizeType, new IR::PathExpression("*standard_metadata"), "packet_length");
     const auto *packetSizeConst = new IR::Div(pktSizeType, ExecutionState::getInputPacketSizeVar(),
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp b/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp
index be6575202b4..19d55120656 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/concolic.cpp
@@ -2,10 +2,8 @@
 
 #include <algorithm>
 #include <iterator>
-#include <list>
 #include <map>
 #include <utility>
-#include <variant>
 #include <vector>
 
 #include <boost/multiprecision/cpp_int.hpp>
@@ -16,7 +14,6 @@
 #include <boost/multiprecision/traits/explicit_conversion.hpp>
 
 #include "backends/p4tools/common/lib/model.h"
-#include "backends/p4tools/common/lib/util.h"
 #include "ir/irutils.h"
 #include "ir/vector.h"
 #include "lib/cstring.h"
@@ -26,6 +23,7 @@
 #include "backends/p4tools/modules/testgen/lib/concolic.h"
 #include "backends/p4tools/modules/testgen/lib/exceptions.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/contrib/bmv2_hash/calculations.h"
 
 namespace P4Tools::P4Testgen::Bmv2 {
@@ -47,26 +45,6 @@ std::vector<char> Bmv2Concolic::convertBigIntToBytes(big_int &dataInt, int targe
     return bytes;
 }
 
-const IR::Expression *Bmv2Concolic::setAndComputePayload(
-    const Model &completedModel, ConcolicVariableMap *resolvedConcolicVariables, int payloadSize) {
-    const auto *payloadType = IR::getBitType(payloadSize);
-    const auto &payLoadVar = IR::StateVariable(ExecutionState::getPayloadLabel(payloadType));
-    const auto *payloadExpr = completedModel.get(payLoadVar, false);
-    // If the variable already has been fixed, return it
-    auto it = resolvedConcolicVariables->find(payLoadVar);
-    if (it != resolvedConcolicVariables->end()) {
-        return it->second;
-    }
-    payloadExpr = Utils::getRandConstantForType(payloadType);
-    BUG_CHECK(payloadExpr->type->width_bits() == payloadSize,
-              "The width (%1%) of the payload expression should match the calculated payload "
-              "size %2%.",
-              payloadExpr->type->width_bits(), payloadSize);
-    // Set the payload variable.
-    resolvedConcolicVariables->emplace(payLoadVar, payloadExpr);
-    return payloadExpr;
-}
-
 big_int Bmv2Concolic::computeChecksum(const std::vector<const IR::Expression *> &exprList,
                                       const Model &completedModel, int algo,
                                       Model::ExpressionMap *resolvedExpressions) {
@@ -187,10 +165,8 @@ const ConcolicMethodImpls::ImplList Bmv2Concolic::BMV2_CONCOLIC_METHOD_IMPLS{
 
          // Assign a value to the @param result using the computed result
          if (const auto *checksumVarType = checksumVar->type->to<IR::Type_Bits>()) {
-             auto concolicMember = Utils::getConcolicMember(var, 0);
              // Overwrite any previous assignment or result.
-             (*resolvedConcolicVariables)[concolicMember] =
-                 IR::getConstant(checksumVarType, computedResult);
+             (*resolvedConcolicVariables)[*var] = IR::getConstant(checksumVarType, computedResult);
 
          } else {
              TESTGEN_UNIMPLEMENTED("Checksum output %1% of type %2% not supported", checksumVar,
@@ -242,10 +218,8 @@ const ConcolicMethodImpls::ImplList Bmv2Concolic::BMV2_CONCOLIC_METHOD_IMPLS{
          computedResult = std::min(computedResult, maxHashInt);
          // Assign a value to the @param result using the computed result
          if (checksumVarType->is<IR::Type_Bits>()) {
-             auto concolicMember = Utils::getConcolicMember(var, 0);
              // Overwrite any previous assignment or result.
-             (*resolvedConcolicVariables)[concolicMember] =
-                 IR::getConstant(checksumVarType, computedResult);
+             (*resolvedConcolicVariables)[*var] = IR::getConstant(checksumVarType, computedResult);
          } else {
              TESTGEN_UNIMPLEMENTED("Checksum output %1% of type %2% not supported", checksumVar,
                                    checksumVarType);
@@ -264,7 +238,7 @@ const ConcolicMethodImpls::ImplList Bmv2Concolic::BMV2_CONCOLIC_METHOD_IMPLS{
     {"*method_checksum_with_payload",
      {"result", "algo", "data"},
      [](cstring /*concolicMethodName*/, const IR::ConcolicVariable *var,
-        const ExecutionState &state, const Model &completedModel,
+        const ExecutionState & /*state*/, const Model &completedModel,
         ConcolicVariableMap *resolvedConcolicVariables) {
          // Assign arguments to concrete variables and perform type checking.
          const auto *args = var->arguments;
@@ -285,18 +259,9 @@ const ConcolicMethodImpls::ImplList Bmv2Concolic::BMV2_CONCOLIC_METHOD_IMPLS{
 
          // This is the maximum value this checksum can have.
          auto maxHashInt = IR::getMaxBvVal(checksumVarType);
-         const auto &packetBitSizeVar = ExecutionState::getInputPacketSizeVar();
-         const auto *payloadSizeConst = completedModel.evaluate(packetBitSizeVar);
-         int calculatedPacketSize = IR::getIntFromLiteral(payloadSizeConst);
-
-         const auto *inputPacketExpr = state.getInputPacket();
-         int payloadSize = calculatedPacketSize - inputPacketExpr->type->width_bits();
-         // If the payload is not 0, we need to add it to our checksum calculation.
-         if (payloadSize > 0) {
-             const auto *payloadExpr =
-                 setAndComputePayload(completedModel, resolvedConcolicVariables, payloadSize);
-             // Fix the payload size only if is not fixed already.
-             resolvedConcolicVariables->emplace(packetBitSizeVar, payloadSizeConst);
+         // If the payload is present, we need to add it to our checksum calculation.
+         const auto *payloadExpr = completedModel.get(&PacketVars::PAYLOAD_LABEL, false);
+         if (payloadExpr != nullptr) {
              exprList.push_back(payloadExpr);
          }
 
@@ -307,10 +272,8 @@ const ConcolicMethodImpls::ImplList Bmv2Concolic::BMV2_CONCOLIC_METHOD_IMPLS{
          computedResult = std::min(computedResult, maxHashInt);
          // Assign a value to the @param result using the computed result
          if (checksumVarType->is<IR::Type_Bits>()) {
-             auto concolicMember = Utils::getConcolicMember(var, 0);
              // Overwrite any previous assignment or result.
-             (*resolvedConcolicVariables)[concolicMember] =
-                 IR::getConstant(checksumVarType, computedResult);
+             (*resolvedConcolicVariables)[*var] = IR::getConstant(checksumVarType, computedResult);
          } else {
              TESTGEN_UNIMPLEMENTED("Checksum output %1% of type %2% not supported", checksumVar,
                                    checksumVarType);
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
index c891232276d..c3181155703 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
@@ -15,6 +15,7 @@
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event_types.h"
 #include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/declaration.h"
 #include "ir/indexed_vector.h"
 #include "ir/irutils.h"
@@ -33,6 +34,7 @@
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
 #include "backends/p4tools/modules/testgen/lib/exceptions.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/lib/test_spec.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/constants.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/program_info.h"
@@ -848,8 +850,8 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
 
              if (cloneType == BMv2Constants::CLONE_TYPE_I2E) {
                  // Pick a clone port var. For now, pick a random value from 0-511.
-                 const auto *egressPortVar = programInfo.getTargetOutputPortVar();
-                 const auto &clonePortVar = Utils::getZombieConst(
+                 const auto &egressPortVar = programInfo.getTargetOutputPortVar();
+                 const auto &clonePortVar = ToolsVariables::getSymbolicVariable(
                      egressPortVar->type, 0, "clone_port_var" + std::to_string(call->clone_id));
                  cond = new IR::LAnd(
                      new IR::Neq(egressPortVar, clonePortVar),
@@ -1135,8 +1137,8 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
 
              if (cloneType == BMv2Constants::CLONE_TYPE_I2E) {
                  // Pick a clone port var. For now, pick a random value from 0-511.
-                 const auto *egressPortVar = programInfo.getTargetOutputPortVar();
-                 const auto &clonePortVar = Utils::getZombieConst(
+                 const auto &egressPortVar = programInfo.getTargetOutputPortVar();
+                 const auto &clonePortVar = ToolsVariables::getSymbolicVariable(
                      egressPortVar->type, 0, "clone_port_var" + std::to_string(call->clone_id));
                  cond = new IR::LAnd(
                      new IR::Neq(egressPortVar, clonePortVar),
@@ -1153,7 +1155,7 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
                  }
                  // This is the clone state.
                  auto &nextState = state.clone();
-                 auto progInfo = getProgramInfo().checkedTo<Bmv2V1ModelProgramInfo>();
+                 const auto *progInfo = getProgramInfo().checkedTo<Bmv2V1ModelProgramInfo>();
 
                  // We need to reset everything to the state before the ingress call. We use a trick
                  // by calling copyIn on the entire state again. We need a little bit of information
@@ -1242,9 +1244,9 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
 
              // We need to update the size of the packet when recirculating. Do not forget to divide
              // by 8.
-             const auto *pktSizeType = ExecutionState::getPacketSizeVarType();
-             const auto *packetSizeVar = new IR::Member(
-                 pktSizeType, new IR::PathExpression("*standard_metadata"), "packet_length");
+             const auto *pktSizeType = &PacketVars::PACKET_SIZE_VAR_TYPE;
+             auto packetSizeVar = IR::StateVariable(new IR::Member(
+                 pktSizeType, new IR::PathExpression("*standard_metadata"), "packet_length"));
              const auto *packetSizeConst =
                  IR::getConstant(pktSizeType, recState.getPacketBufferSize() / 8);
              recState.set(packetSizeVar, packetSizeConst);
@@ -1279,8 +1281,8 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
                  state.hasProperty("clone_active") && state.getProperty<bool>("clone_active");
              if (cloneActive) {
                  // Pick a clone port var. For now, pick a random value from 0-511.
-                 const auto *egressPortVar = programInfo.getTargetOutputPortVar();
-                 const auto &clonePortVar = Utils::getZombieConst(
+                 const auto &egressPortVar = programInfo.getTargetOutputPortVar();
+                 const auto &clonePortVar = ToolsVariables::getSymbolicVariable(
                      egressPortVar->type, 0, "clone_port_var" + std::to_string(call->clone_id));
                  const auto *cond = new IR::LAnd(
                      new IR::Neq(egressPortVar, clonePortVar),
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 dd4a03eba59..d0f43de8a38 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.cpp
@@ -1,7 +1,6 @@
 #include "backends/p4tools/modules/testgen/targets/bmv2/p4_asserts_parser.h"
 
-#include <stdint.h>
-
+#include <cstdint>
 #include <iostream>
 #include <optional>
 #include <string>
@@ -10,7 +9,7 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/core/z3_solver.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
 #include "ir/ir.h"
@@ -19,9 +18,7 @@
 #include "lib/error.h"
 #include "lib/exceptions.h"
 
-namespace P4Tools {
-
-namespace AssertsParser {
+namespace P4Tools::AssertsParser {
 
 static std::vector<std::string> NAMES{
     "Priority",    "Text",           "True",         "False",       "LineStatementClose",
@@ -126,7 +123,7 @@ const IR::Expression *makeSingleExpr(std::vector<const IR::Expression *> input)
     return expr;
 }
 
-/// Determines the token type according to the table key and generates a zombie constant for it.
+/// Determines the token type according to the table key and generates a symbolic variable for it.
 const IR::Expression *makeConstant(Token input, const IR::Vector<IR::KeyElement> &keyElements,
                                    const IR::Type *leftType) {
     const IR::Type_Base *type = nullptr;
@@ -154,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 Utils::getZombieConst(type, 0, std::string(inputStr));
+            return ToolsVariables::getSymbolicVariable(type, 0, std::string(inputStr));
         }
     }
     if (input.is(Token::Kind::Number)) {
@@ -165,7 +162,8 @@ 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 Utils::getZombieConst(IR::Type_Bits::get(32), 0, std::string(inputStr));
+        return ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(32), 0,
+                                                   std::string(inputStr));
     }
     BUG_CHECK(result != nullptr,
               "Could not match restriction key label %s was not found in key list.",
@@ -654,6 +652,4 @@ Token Lexer::next() noexcept {
             return atom(Token::Kind::Mul);
     }
 }
-}  // namespace AssertsParser
-
-}  // namespace P4Tools
+}  // namespace P4Tools::AssertsParser
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 2b4b25b757f..ae9a9e32cc3 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
@@ -6,7 +6,7 @@
 #include <iostream>
 #include <string>
 
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/declaration.h"
 #include "ir/id.h"
 #include "ir/indexed_vector.h"
@@ -23,8 +23,8 @@ RefersToParser::RefersToParser(std::vector<std::vector<const IR::Expression *>>
     setName("RefersToParser");
 }
 
-/// Builds names for the zombie constant and then creates a zombie constant and builds the refers_to
-/// constraints based on them
+/// Builds names for the symbolic variable and then creates a symbolic variable and builds the
+/// refers_to constraints based on them
 void RefersToParser::createConstraint(bool table, cstring currentName, cstring currentKeyName,
                                       cstring destKeyName, cstring destTableName,
                                       const IR::Type *type) {
@@ -34,7 +34,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
     } else {
         tmp = currentName + currentKeyName;
     }
-    auto left = Utils::getZombieConst(type, 0, tmp);
+    auto left = ToolsVariables::getSymbolicVariable(type, 0, 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 = Utils::getZombieConst(type, 0, tmp);
+    auto right = ToolsVariables::getSymbolicVariable(type, 0, 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/p4_refers_to_parser.h b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h
index 06db432787c..79065b06171 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h
@@ -23,7 +23,7 @@ class RefersToParser : public Inspector {
 
     bool preorder(const IR::P4Table *table) override;
 
-    /// Builds names for the zombie constant and then creates a zombie constant and builds the
+    /// Builds names for the symbolic variable and then creates a symbolic variable and builds the
     /// refers_to constraints based on them
     void createConstraint(bool table, cstring currentName, cstring currentKeyName,
                           cstring destKeyName, cstring destTableName, const IR::Type *type);
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp
index 0c378977778..29c65b1307a 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp
@@ -26,6 +26,7 @@
 #include "backends/p4tools/modules/testgen/lib/concolic.h"
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/options.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/concolic.h"
 #include "backends/p4tools/modules/testgen/targets/bmv2/constants.h"
@@ -74,7 +75,7 @@ Bmv2V1ModelProgramInfo::Bmv2V1ModelProgramInfo(
     }
     const IR::Expression *constraint =
         new IR::Grt(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(),
-                    IR::getConstant(ExecutionState::getPacketSizeVarType(), minPktSize));
+                    IR::getConstant(&PacketVars::PACKET_SIZE_VAR_TYPE, minPktSize));
     /// Vector containing pairs of restrictions and nodes to which these restrictions apply.
     std::vector<std::vector<const IR::Expression *>> restrictionsVec;
     /// Defines all "entry_restriction" and then converts restrictions from string to IR
@@ -168,37 +169,31 @@ std::vector<Continuation::Command> Bmv2V1ModelProgramInfo::processDeclaration(
     return cmds;
 }
 
-const IR::Member *Bmv2V1ModelProgramInfo::getTargetInputPortVar() const {
-    return new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                          new IR::PathExpression("*standard_metadata"), "ingress_port");
+const IR::StateVariable &Bmv2V1ModelProgramInfo::getTargetInputPortVar() const {
+    return *new IR::StateVariable(
+        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+                       new IR::PathExpression("*standard_metadata"), "ingress_port"));
 }
 
-const IR::Expression *Bmv2V1ModelProgramInfo::getPortConstraint(const IR::Member *portVar) {
+const IR::Expression *Bmv2V1ModelProgramInfo::getPortConstraint(const IR::StateVariable &portVar) {
     const IR::Operation_Binary *portConstraint =
         new IR::LOr(new IR::Equ(portVar, new IR::Constant(portVar->type, BMv2Constants::DROP_PORT)),
                     new IR::Lss(portVar, new IR::Constant(portVar->type, 8)));
     return portConstraint;
 }
 
-const IR::Member *Bmv2V1ModelProgramInfo::getTargetOutputPortVar() const {
-    return new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                          new IR::PathExpression("*standard_metadata"), "egress_spec");
+const IR::StateVariable &Bmv2V1ModelProgramInfo::getTargetOutputPortVar() const {
+    return *new IR::StateVariable(
+        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+                       new IR::PathExpression("*standard_metadata"), "egress_spec"));
 }
 
 const IR::Expression *Bmv2V1ModelProgramInfo::dropIsActive() const {
-    const auto *egressPortVar = getTargetOutputPortVar();
+    const auto &egressPortVar = getTargetOutputPortVar();
     return new IR::Equ(IR::getConstant(egressPortVar->type, BMv2Constants::DROP_PORT),
                        egressPortVar);
 }
 
-const IR::Expression *Bmv2V1ModelProgramInfo::createTargetUninitialized(const IR::Type *type,
-                                                                        bool forceTaint) const {
-    if (forceTaint) {
-        return Utils::getTaintExpression(type);
-    }
-    return IR::getDefaultValue(type);
-}
-
 const IR::Type_Bits *Bmv2V1ModelProgramInfo::getParserErrorType() const { return &PARSER_ERR_BITS; }
 
 const IR::PathExpression *Bmv2V1ModelProgramInfo::getBlockParam(cstring blockLabel,
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/program_info.h b/backends/p4tools/modules/testgen/targets/bmv2/program_info.h
index 7c5f0b3b85e..a964c2030f0 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/program_info.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/program_info.h
@@ -48,18 +48,15 @@ class Bmv2V1ModelProgramInfo : public ProgramInfo {
     [[nodiscard]] const IR::PathExpression *getBlockParam(cstring blockLabel,
                                                           size_t paramIndex) const;
 
-    [[nodiscard]] const IR::Member *getTargetInputPortVar() const override;
+    [[nodiscard]] const IR::StateVariable &getTargetInputPortVar() const override;
 
     /// @returns the constraint expression for a given port variable.
-    static const IR::Expression *getPortConstraint(const IR::Member *portVar);
+    static const IR::Expression *getPortConstraint(const IR::StateVariable &portVar);
 
-    [[nodiscard]] const IR::Member *getTargetOutputPortVar() const override;
+    [[nodiscard]] const IR::StateVariable &getTargetOutputPortVar() const override;
 
     [[nodiscard]] const IR::Expression *dropIsActive() const override;
 
-    [[nodiscard]] const IR::Expression *createTargetUninitialized(const IR::Type *type,
-                                                                  bool forceTaint) const override;
-
     [[nodiscard]] const IR::Type_Bits *getParserErrorType() const override;
 
     /// @returns the Member variable corresponding to the parameter index for the given parameter.
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
index b70305b4a79..6562f704530 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
@@ -9,7 +9,6 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/lib/trace_event_types.h"
-#include "backends/p4tools/common/lib/util.h"
 #include "ir/declaration.h"
 #include "ir/id.h"
 #include "ir/irutils.h"
@@ -43,9 +42,9 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
     // TODO: We consider optional match types to be a no-op, but we could make them exact matches.
     if (keyProperties.matchType == BMv2Constants::MATCH_KIND_OPT) {
         // We can recover from taint by simply not adding the optional match.
-        // Create a new zombie constant that corresponds to the key expression.
+        // Create a new symbolic variable that corresponds to the key expression.
         cstring keyName = properties.tableName + "_key_" + keyProperties.name;
-        const auto ctrlPlaneKey = nextState.createZombieConst(keyExpr->type, keyName);
+        const auto ctrlPlaneKey = nextState.createSymbolicVariable(keyExpr->type, keyName);
         if (keyProperties.isTainted) {
             matches->emplace(keyProperties.name,
                              new Optional(keyProperties.key, ctrlPlaneKey, false));
@@ -75,8 +74,8 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
             maxKey = IR::getConstant(keyExpr->type, IR::getMaxBvVal(keyExpr->type));
             keyExpr = minKey;
         } else {
-            minKey = nextState.createZombieConst(keyExpr->type, minName);
-            maxKey = nextState.createZombieConst(keyExpr->type, maxName);
+            minKey = nextState.createSymbolicVariable(keyExpr->type, minName);
+            maxKey = nextState.createSymbolicVariable(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),
@@ -110,14 +109,14 @@ void Bmv2V1ModelTableStepper::evalTableActionProfile(
         std::vector<ActionArg> ctrlPlaneArgs;
         for (size_t argIdx = 0; argIdx < parameters->size(); ++argIdx) {
             const auto *parameter = parameters->getParameter(argIdx);
-            // Synthesize a zombie constant here that corresponds to a control plane argument.
+            // Synthesize a symbolic variable here that corresponds to a control plane argument.
             // We get the unique name of the table coupled with the unique name of the action.
             // Getting the unique name is needed to avoid generating duplicate arguments.
             const auto &actionDataVar =
-                Utils::getZombieTableVar(parameter->type, table, "*actionData", idx, argIdx);
+                getTableStateVariable(parameter->type, table, "*actionData", idx, argIdx);
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createZombieConst(parameter->type, keyName);
+            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
             nextState.set(actionDataVar, actionArg);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
@@ -201,14 +200,14 @@ void Bmv2V1ModelTableStepper::evalTableActionSelector(
         std::vector<ActionArg> ctrlPlaneArgs;
         for (size_t argIdx = 0; argIdx < parameters->size(); ++argIdx) {
             const auto *parameter = parameters->getParameter(argIdx);
-            // Synthesize a zombie constant here that corresponds to a control plane argument.
+            // Synthesize a symbolic variable here that corresponds to a control plane argument.
             // We get the unique name of the table coupled with the unique name of the action.
             // Getting the unique name is needed to avoid generating duplicate arguments.
             const auto &actionDataVar =
-                Utils::getZombieTableVar(parameter->type, table, "*actionData", idx, argIdx);
+                getTableStateVariable(parameter->type, table, "*actionData", idx, argIdx);
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createZombieConst(parameter->type, keyName);
+            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
             nextState.set(actionDataVar, actionArg);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/target.cpp b/backends/p4tools/modules/testgen/targets/bmv2/target.cpp
index 60dde3e74e0..bdfb009d62e 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/target.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/target.cpp
@@ -5,7 +5,6 @@
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "ir/ir.h"
 #include "lib/cstring.h"
 #include "lib/exceptions.h"
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test/P4Tests.cmake b/backends/p4tools/modules/testgen/targets/bmv2/test/P4Tests.cmake
index 5f76af509a4..ca5d0f3630a 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/test/P4Tests.cmake
+++ b/backends/p4tools/modules/testgen/targets/bmv2/test/P4Tests.cmake
@@ -72,8 +72,14 @@ if(P4TOOLS_TESTGEN_BMV2_TEST_PTF)
       "BMv2 PTF tests are enabled, but the Python3 module 'google.rpc' can not be found. BMv2 PTF tests will fail."
     )
   endif()
+  # Filter some programs  because they have issues that are not captured with Xfails.
+  set (P4C_V1_TEST_SUITES_P416_PTF ${P4C_V1_TEST_SUITES_P416})
+  list(REMOVE_ITEM P4C_V1_TEST_SUITES_P416_PTF
+       # A particular test (or packet?) combination leads to an infinite loop in the simple switch.
+       "${P4C_SOURCE_DIR}/testdata/p4_16_samples/v1model-special-ops-bmv2.p4"
+  )
   p4tools_add_tests(
-    TESTSUITES "${P4C_V1_TEST_SUITES_P416}"
+    TESTSUITES "${P4C_V1_TEST_SUITES_P416_PTF}"
     TAG "testgen-p4c-bmv2-ptf" DRIVER ${P4TESTGEN_DRIVER}
     TARGET "bmv2" ARCH "v1model" P416_PTF TEST_ARGS "-I${P4C_BINARY_DIR}/p4include --test-backend PTF --packet-size-range 0:12000 ${EXTRA_OPTS} "
   )
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp b/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp
index 3bf759a2e04..6689c8e9097 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.cpp
@@ -1,6 +1,7 @@
 #include "backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.h"
 
 #include <filesystem>
+#include <fstream>
 #include <iomanip>
 #include <map>
 #include <optional>
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.h b/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.h
index 439e990738b..f929c40d10d 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.h
+++ b/backends/p4tools/modules/testgen/targets/ebpf/backend/stf/stf.h
@@ -2,7 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_EBPF_BACKEND_STF_STF_H_
 
 #include <cstddef>
-#include <fstream>
+#include <filesystem>
 #include <optional>
 #include <string>
 #include <vector>
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/expr_stepper.cpp b/backends/p4tools/modules/testgen/targets/ebpf/expr_stepper.cpp
index fcae7ebbfea..6a587836bf3 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/expr_stepper.cpp
@@ -6,7 +6,7 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/irutils.h"
 #include "lib/cstring.h"
 #include "lib/error.h"
@@ -97,7 +97,7 @@ void EBPFExprStepper::evalExternMethodCall(const IR::MethodCallExpression *call,
              // Input must be an IPv4 header.
              ipHdrRef->type->checkedTo<IR::Type_Header>();
 
-             const auto &validVar = state.get(Utils::getHeaderValidity(ipHdrRef));
+             const auto &validVar = state.get(ToolsVariables::getHeaderValidity(ipHdrRef));
              // Check whether the validity bit of the header is false.
              // If yes, do not bother evaluating the checksum.
              auto emitIsTainted = state.hasTaint(validVar);
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp b/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp
index 5f309a82d80..c4bcd55a828 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp
@@ -22,6 +22,7 @@
 #include "backends/p4tools/modules/testgen/lib/concolic.h"
 #include "backends/p4tools/modules/testgen/lib/continuation.h"
 #include "backends/p4tools/modules/testgen/lib/execution_state.h"
+#include "backends/p4tools/modules/testgen/lib/packet_vars.h"
 #include "backends/p4tools/modules/testgen/targets/ebpf/concolic.h"
 
 namespace P4Tools::P4Testgen::EBPF {
@@ -55,7 +56,7 @@ EBPFProgramInfo::EBPFProgramInfo(const IR::P4Program *program,
     // The input packet should be larger than 0.
     targetConstraints =
         new IR::Grt(IR::Type::Boolean::get(), ExecutionState::getInputPacketSizeVar(),
-                    IR::getConstant(ExecutionState::getPacketSizeVarType(), 0));
+                    IR::getConstant(&PacketVars::PACKET_SIZE_VAR_TYPE, 0));
 }
 
 const ordered_map<cstring, const IR::Type_Declaration *> *EBPFProgramInfo::getProgrammableBlocks()
@@ -101,14 +102,16 @@ std::vector<Continuation::Command> EBPFProgramInfo::processDeclaration(
     return cmds;
 }
 
-const IR::Member *EBPFProgramInfo::getTargetInputPortVar() const {
-    return new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                          new IR::PathExpression("*"), "input_port");
+const IR::StateVariable &EBPFProgramInfo::getTargetInputPortVar() const {
+    return *new IR::StateVariable(
+        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+                       new IR::PathExpression("*"), "input_port"));
 }
 
-const IR::Member *EBPFProgramInfo::getTargetOutputPortVar() const {
-    return new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                          new IR::PathExpression("*"), "output_port");
+const IR::StateVariable &EBPFProgramInfo::getTargetOutputPortVar() const {
+    return *new IR::StateVariable(
+        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+                       new IR::PathExpression("*"), "output_port"));
 }
 
 const IR::Expression *EBPFProgramInfo::dropIsActive() const {
@@ -116,14 +119,6 @@ const IR::Expression *EBPFProgramInfo::dropIsActive() const {
         new IR::Member(IR::Type_Boolean::get(), new IR::PathExpression("*accept"), "*"));
 }
 
-const IR::Expression *EBPFProgramInfo::createTargetUninitialized(const IR::Type *type,
-                                                                 bool forceTaint) const {
-    if (forceTaint) {
-        return Utils::getTaintExpression(type);
-    }
-    return IR::getDefaultValue(type);
-}
-
 const IR::Type_Bits *EBPFProgramInfo::getParserErrorType() const { return &PARSER_ERR_BITS; }
 
 }  // namespace P4Tools::P4Testgen::EBPF
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/program_info.h b/backends/p4tools/modules/testgen/targets/ebpf/program_info.h
index 1a92da8aa99..46ac1de7cb2 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/program_info.h
+++ b/backends/p4tools/modules/testgen/targets/ebpf/program_info.h
@@ -36,15 +36,12 @@ class EBPFProgramInfo : public ProgramInfo {
     [[nodiscard]] const ordered_map<cstring, const IR::Type_Declaration *> *getProgrammableBlocks()
         const;
 
-    [[nodiscard]] const IR::Member *getTargetInputPortVar() const override;
+    [[nodiscard]] const IR::StateVariable &getTargetInputPortVar() const override;
 
-    [[nodiscard]] const IR::Member *getTargetOutputPortVar() const override;
+    [[nodiscard]] const IR::StateVariable &getTargetOutputPortVar() const override;
 
     [[nodiscard]] const IR::Expression *dropIsActive() const override;
 
-    [[nodiscard]] const IR::Expression *createTargetUninitialized(const IR::Type *type,
-                                                                  bool forceTaint) const override;
-
     [[nodiscard]] const IR::Type_Bits *getParserErrorType() const override;
 };
 
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/target.cpp b/backends/p4tools/modules/testgen/targets/ebpf/target.cpp
index 60866e414f5..a4b7fe124e1 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/target.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/target.cpp
@@ -5,7 +5,6 @@
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "ir/ir.h"
 #include "lib/cstring.h"
 #include "lib/error.h"
diff --git a/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp b/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp
index b8b500b8b98..e387d6b95bb 100644
--- a/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.cpp
@@ -1,6 +1,7 @@
 #include "backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.h"
 
 #include <algorithm>
+#include <functional>
 #include <iomanip>
 #include <map>
 #include <string>
diff --git a/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.h b/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.h
index 839cd63ff47..47ae08a911d 100644
--- a/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.h
+++ b/backends/p4tools/modules/testgen/targets/pna/backend/metadata/metadata.h
@@ -2,6 +2,7 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_PNA_BACKEND_METADATA_METADATA_H_
 
 #include <cstddef>
+#include <filesystem>
 #include <fstream>
 #include <optional>
 #include <string>
diff --git a/backends/p4tools/modules/testgen/targets/pna/constants.cpp b/backends/p4tools/modules/testgen/targets/pna/constants.cpp
index f6f54fcd461..e545b70e9f1 100644
--- a/backends/p4tools/modules/testgen/targets/pna/constants.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/constants.cpp
@@ -1,6 +1,7 @@
 #include "backends/p4tools/modules/testgen/targets/pna/constants.h"
 
 #include "ir/id.h"
+#include "lib/cstring.h"
 
 namespace P4Tools::P4Testgen::Pna {
 
@@ -10,11 +11,9 @@ const IR::Member PnaConstants::OUTPUT_PORT_VAR = IR::Member(
     new IR::Type_Bits(32, false), new IR::PathExpression("*pna_internal"), "output_port");
 const IR::Member PnaConstants::PARSER_ERROR = IR::Member(
     new IR::Type_Bits(32, false), new IR::PathExpression("*pna_internal"), "parser_error");
-// TODO: Make this a proper zombie variable.
+// TODO: Make this a proper variables variable.
 // We can not use the utilities because of an issue related to the garbage collector.
-const IR::Member PnaZombies::DIRECTION = IR::Member(
-    new IR::Type_Bits(32, false),
-    new IR::Member(new IR::Type_Bits(32, false), new IR::PathExpression("p4t*zombie"), "const"),
-    "parser_error");
+const IR::SymbolicVariable PnaSymbolicVars::DIRECTION =
+    IR::SymbolicVariable(new IR::Type_Bits(32, false), "direction");
 
 }  // namespace P4Tools::P4Testgen::Pna
diff --git a/backends/p4tools/modules/testgen/targets/pna/constants.h b/backends/p4tools/modules/testgen/targets/pna/constants.h
index c2dfed291eb..462bfae1fed 100644
--- a/backends/p4tools/modules/testgen/targets/pna/constants.h
+++ b/backends/p4tools/modules/testgen/targets/pna/constants.h
@@ -24,11 +24,11 @@ class PnaConstants {
     static const IR::Member PARSER_ERROR;
 };
 
-/// Zombies are variables that can be controlled and set by P4Testgen.
-class PnaZombies {
+/// variabless are variables that can be controlled and set by P4Testgen.
+class PnaSymbolicVars {
  public:
     /// The input direction.
-    static const IR::Member DIRECTION;
+    static const IR::SymbolicVariable DIRECTION;
 };
 
 }  // namespace P4Tools::P4Testgen::Pna
diff --git a/backends/p4tools/modules/testgen/targets/pna/dpdk/cmd_stepper.cpp b/backends/p4tools/modules/testgen/targets/pna/dpdk/cmd_stepper.cpp
index a79b0d1fadb..22ebfbe3e04 100644
--- a/backends/p4tools/modules/testgen/targets/pna/dpdk/cmd_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/dpdk/cmd_stepper.cpp
@@ -56,13 +56,13 @@ void PnaDpdkCmdStepper::initializeTargetEnvironment(ExecutionState &nextState) c
     // Initialize the direction metadata variables.
     nextState.set(
         new IR::Member(thirtytwoBitType, new IR::PathExpression("*pre_istd"), "direction"),
-        &PnaZombies::DIRECTION);
+        &PnaSymbolicVars::DIRECTION);
     nextState.set(
         new IR::Member(thirtytwoBitType, new IR::PathExpression("*parser_istd"), "direction"),
-        &PnaZombies::DIRECTION);
+        &PnaSymbolicVars::DIRECTION);
     nextState.set(
         new IR::Member(thirtytwoBitType, new IR::PathExpression("*main_istd"), "direction"),
-        &PnaZombies::DIRECTION);
+        &PnaSymbolicVars::DIRECTION);
 }
 
 std::optional<const Constraint *> PnaDpdkCmdStepper::startParserImpl(
diff --git a/backends/p4tools/modules/testgen/targets/pna/shared_expr_stepper.cpp b/backends/p4tools/modules/testgen/targets/pna/shared_expr_stepper.cpp
index 0ca1dbef4ca..edefbf09784 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_expr_stepper.cpp
@@ -10,7 +10,7 @@
 #include "backends/p4tools/common/core/solver.h"
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/trace_event_types.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/irutils.h"
 #include "lib/cstring.h"
 
@@ -136,7 +136,7 @@ const ExternMethodImpls SharedPnaExprStepper::PNA_EXTERN_METHOD_IMPLS({
          if (state.hasTaint(directionVar)) {
              auto &taintedState = state.clone();
              taintedState.replaceTopBody(
-                 Continuation::Return(Utils::getTaintExpression(n2hValue->type)));
+                 Continuation::Return(ToolsVariables::getTaintExpression(n2hValue->type)));
              result->emplace_back(taintedState);
              return;
          };
diff --git a/backends/p4tools/modules/testgen/targets/pna/shared_program_info.cpp b/backends/p4tools/modules/testgen/targets/pna/shared_program_info.cpp
index 832461fde98..65cd11eb9d6 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_program_info.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_program_info.cpp
@@ -3,7 +3,6 @@
 #include <utility>
 
 #include "backends/p4tools/common/lib/arch_spec.h"
-#include "backends/p4tools/common/lib/util.h"
 #include "ir/id.h"
 #include "ir/ir.h"
 #include "ir/irutils.h"
@@ -31,25 +30,18 @@ const ordered_map<cstring, const IR::Type_Declaration *>
     return &programmableBlocks;
 }
 
-const IR::Member *SharedPnaProgramInfo::getTargetInputPortVar() const {
-    return new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                          new IR::PathExpression("*parser_istd"), "input_port");
+const IR::StateVariable &SharedPnaProgramInfo::getTargetInputPortVar() const {
+    return *new IR::StateVariable(
+        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+                       new IR::PathExpression("*parser_istd"), "input_port"));
 }
 
-const IR::Member *SharedPnaProgramInfo::getTargetOutputPortVar() const {
-    return &PnaConstants::OUTPUT_PORT_VAR;
+const IR::StateVariable &SharedPnaProgramInfo::getTargetOutputPortVar() const {
+    return *new IR::StateVariable(&PnaConstants::OUTPUT_PORT_VAR);
 }
 
 const IR::Expression *SharedPnaProgramInfo::dropIsActive() const { return &PnaConstants::DROP_VAR; }
 
-const IR::Expression *SharedPnaProgramInfo::createTargetUninitialized(const IR::Type *type,
-                                                                      bool forceTaint) const {
-    if (forceTaint) {
-        return Utils::getTaintExpression(type);
-    }
-    return IR::getDefaultValue(type);
-}
-
 const IR::Type_Bits *SharedPnaProgramInfo::getParserErrorType() const { return &PARSER_ERR_BITS; }
 
 const IR::PathExpression *SharedPnaProgramInfo::getBlockParam(cstring blockLabel,
diff --git a/backends/p4tools/modules/testgen/targets/pna/shared_program_info.h b/backends/p4tools/modules/testgen/targets/pna/shared_program_info.h
index 76ede0b33d5..d11ce7b65de 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_program_info.h
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_program_info.h
@@ -27,15 +27,12 @@ class SharedPnaProgramInfo : public ProgramInfo {
     [[nodiscard]] const ordered_map<cstring, const IR::Type_Declaration *> *getProgrammableBlocks()
         const;
 
-    [[nodiscard]] const IR::Member *getTargetInputPortVar() const override;
+    [[nodiscard]] const IR::StateVariable &getTargetInputPortVar() const override;
 
-    [[nodiscard]] const IR::Member *getTargetOutputPortVar() const override;
+    [[nodiscard]] const IR::StateVariable &getTargetOutputPortVar() const override;
 
     [[nodiscard]] const IR::Expression *dropIsActive() const override;
 
-    [[nodiscard]] const IR::Expression *createTargetUninitialized(const IR::Type *type,
-                                                                  bool forceTaint) const override;
-
     [[nodiscard]] const IR::Type_Bits *getParserErrorType() const override;
 
     /// @returns the name of the parameter for a given programmable-block label and the parameter
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 fe4b40c1d38..370716f59da 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_table_stepper.cpp
@@ -9,7 +9,6 @@
 #include <boost/multiprecision/cpp_int.hpp>
 
 #include "backends/p4tools/common/lib/trace_event_types.h"
-#include "backends/p4tools/common/lib/util.h"
 #include "ir/declaration.h"
 #include "ir/id.h"
 #include "ir/irutils.h"
@@ -43,9 +42,9 @@ const IR::Expression *SharedPnaTableStepper::computeTargetMatchType(
     // TODO: We consider optional match types to be a no-op, but we could make them exact matches.
     if (keyProperties.matchType == PnaConstants::MATCH_KIND_OPT) {
         // We can recover from taint by simply not adding the optional match.
-        // Create a new zombie constant that corresponds to the key expression.
+        // Create a new symbolic variable that corresponds to the key expression.
         cstring keyName = properties.tableName + "_key_" + keyProperties.name;
-        const auto ctrlPlaneKey = nextState.createZombieConst(keyExpr->type, keyName);
+        const auto ctrlPlaneKey = nextState.createSymbolicVariable(keyExpr->type, keyName);
         if (keyProperties.isTainted) {
             matches->emplace(keyProperties.name,
                              new Optional(keyProperties.key, ctrlPlaneKey, false));
@@ -75,8 +74,8 @@ const IR::Expression *SharedPnaTableStepper::computeTargetMatchType(
             maxKey = IR::getConstant(keyExpr->type, IR::getMaxBvVal(keyExpr->type));
             keyExpr = minKey;
         } else {
-            minKey = nextState.createZombieConst(keyExpr->type, minName);
-            maxKey = nextState.createZombieConst(keyExpr->type, maxName);
+            minKey = nextState.createSymbolicVariable(keyExpr->type, minName);
+            maxKey = nextState.createSymbolicVariable(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),
@@ -110,14 +109,14 @@ void SharedPnaTableStepper::evalTableActionProfile(
         std::vector<ActionArg> ctrlPlaneArgs;
         for (size_t argIdx = 0; argIdx < parameters->size(); ++argIdx) {
             const auto *parameter = parameters->getParameter(argIdx);
-            // Synthesize a zombie constant here that corresponds to a control plane argument.
+            // Synthesize a symbolic variable here that corresponds to a control plane argument.
             // We get the unique name of the table coupled with the unique name of the action.
             // Getting the unique name is needed to avoid generating duplicate arguments.
             const auto &actionDataVar =
-                Utils::getZombieTableVar(parameter->type, table, "*actionData", idx, argIdx);
+                getTableStateVariable(parameter->type, table, "*actionData", idx, argIdx);
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createZombieConst(parameter->type, keyName);
+            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
             nextState.set(actionDataVar, actionArg);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
@@ -201,14 +200,14 @@ void SharedPnaTableStepper::evalTableActionSelector(
         std::vector<ActionArg> ctrlPlaneArgs;
         for (size_t argIdx = 0; argIdx < parameters->size(); ++argIdx) {
             const auto *parameter = parameters->getParameter(argIdx);
-            // Synthesize a zombie constant here that corresponds to a control plane argument.
+            // Synthesize a symbolic variable here that corresponds to a control plane argument.
             // We get the unique name of the table coupled with the unique name of the action.
             // Getting the unique name is needed to avoid generating duplicate arguments.
             const auto &actionDataVar =
-                Utils::getZombieTableVar(parameter->type, table, "*actionData", idx, argIdx);
+                getTableStateVariable(parameter->type, table, "*actionData", idx, argIdx);
             cstring keyName =
                 properties.tableName + "_param_" + actionName + std::to_string(argIdx);
-            const auto &actionArg = nextState.createZombieConst(parameter->type, keyName);
+            const auto &actionArg = nextState.createSymbolicVariable(parameter->type, keyName);
             nextState.set(actionDataVar, actionArg);
             arguments->push_back(new IR::Argument(actionArg));
             // We also track the argument we synthesize for the control plane.
diff --git a/backends/p4tools/modules/testgen/targets/pna/target.cpp b/backends/p4tools/modules/testgen/targets/pna/target.cpp
index e5681f78af8..d355b29f9e3 100644
--- a/backends/p4tools/modules/testgen/targets/pna/target.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/target.cpp
@@ -4,7 +4,6 @@
 #include <vector>
 
 #include "backends/p4tools/common/core/solver.h"
-#include "backends/p4tools/common/lib/namespace_context.h"
 #include "ir/ir.h"
 #include "lib/cstring.h"
 #include "lib/exceptions.h"
diff --git a/backends/p4tools/modules/testgen/test/gtest_utils.cpp b/backends/p4tools/modules/testgen/test/gtest_utils.cpp
index 37e26e64d17..5600a570a66 100644
--- a/backends/p4tools/modules/testgen/test/gtest_utils.cpp
+++ b/backends/p4tools/modules/testgen/test/gtest_utils.cpp
@@ -58,4 +58,8 @@ void P4ToolsTestCase::ensureInit() {
     initialized = true;
 }
 
+const IR::SymbolicVariable *SymbolicConverter::preorder(IR::Member *member) {
+    return P4Tools::ToolsVariables::getSymbolicVariable(member->type, 0, member->toString());
+}
+
 }  // namespace Test
diff --git a/backends/p4tools/modules/testgen/test/gtest_utils.h b/backends/p4tools/modules/testgen/test/gtest_utils.h
index 767358b0015..96ad0107f44 100644
--- a/backends/p4tools/modules/testgen/test/gtest_utils.h
+++ b/backends/p4tools/modules/testgen/test/gtest_utils.h
@@ -4,6 +4,7 @@
 #include <optional>
 #include <string>
 
+#include "backends/p4tools/common/lib/variables.h"
 #include "frontends/common/options.h"
 #include "ir/ir.h"
 #include "test/frameworks/gtest/googletest/include/gtest/gtest.h"
@@ -39,6 +40,12 @@ class P4ToolsTestCase {
 /// GTest for P4 Tools tests.
 class P4ToolsTest : public ::testing::Test {};
 
+/// Converts IR::Member into symbolic variables.
+class SymbolicConverter : public Transform {
+ public:
+    const IR::SymbolicVariable *preorder(IR::Member *member) override;
+};
+
 }  // namespace Test
 
 #endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TEST_GTEST_UTILS_H_ */
diff --git a/backends/p4tools/modules/testgen/test/lib/taint.cpp b/backends/p4tools/modules/testgen/test/lib/taint.cpp
index 4a8cf65a038..0058ffc8962 100644
--- a/backends/p4tools/modules/testgen/test/lib/taint.cpp
+++ b/backends/p4tools/modules/testgen/test/lib/taint.cpp
@@ -8,7 +8,7 @@
 
 #include "backends/p4tools/common/lib/symbolic_env.h"
 #include "backends/p4tools/common/lib/taint.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "ir/ir.h"
 #include "ir/irutils.h"
 
@@ -20,7 +20,7 @@ namespace Test {
 namespace {
 
 using P4Tools::Taint;
-using P4Tools::Utils;
+using P4Tools::ToolsVariables;
 
 /// Test whether taint propagation works at all.
 /// Input: 8w2 + taint<8>
@@ -35,7 +35,7 @@ TEST_F(TaintTest, Taint01) {
     auto &state = ExecutionState::create(new IR::P4Program());
     const auto &env = state.getSymbolicEnv();
     {
-        const auto *taintExpression = Utils::getTaintExpression(typeBits);
+        const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
         const auto *constantVar = IR::getConstant(typeBits, 2);
         const auto *expr = new IR::Add(constantVar, taintExpression);
         const auto *taintedExpr = Taint::propagateTaint(env.getInternalMap(), expr);
@@ -51,7 +51,7 @@ TEST_F(TaintTest, Taint01) {
         ASSERT_TRUE(taintedExpr->equiv(*expectedExpr));
     }
     {
-        const auto *taintExpression = Utils::getTaintExpression(typeBits);
+        const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
         const auto *expectedExpr = taintExpression;
         ASSERT_TRUE(taintExpression->equiv(*expectedExpr));
     }
@@ -68,7 +68,7 @@ TEST_F(TaintTest, Taint02) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     {
         const auto *expr =
             new IR::Concat(IR::getBitType(16), IR::getConstant(typeBits, 2), taintExpression);
@@ -98,7 +98,7 @@ TEST_F(TaintTest, Taint03) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     {
         const auto *expr =
             new IR::Concat(IR::getBitType(16), IR::getConstant(typeBits, 2), taintExpression);
@@ -128,7 +128,7 @@ TEST_F(TaintTest, Taint04) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     {
         const auto *expr =
             new IR::Concat(IR::getBitType(16), IR::getConstant(typeBits, 2), taintExpression);
@@ -158,7 +158,7 @@ TEST_F(TaintTest, Taint05) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     const auto *constantVar = IR::getConstant(typeBits, 2);
     {
         const auto *expr = new IR::Concat(IR::getBitType(16), taintExpression, constantVar);
@@ -189,7 +189,7 @@ TEST_F(TaintTest, Taint06) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     const auto *constantVar = IR::getConstant(typeBits, 2);
     {
         const auto *expr = new IR::Concat(IR::getBitType(16), constantVar, taintExpression);
@@ -220,7 +220,7 @@ TEST_F(TaintTest, Taint07) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     const auto *constantVar = IR::getConstant(typeBits, 2);
 
     {
@@ -253,7 +253,7 @@ TEST_F(TaintTest, Taint08) {
     const auto &env = state.getSymbolicEnv();
 
     const auto *typeBits = IR::getBitType(8);
-    const auto *taintExpression = Utils::getTaintExpression(typeBits);
+    const auto *taintExpression = ToolsVariables::getTaintExpression(typeBits);
     const auto *constantVar = IR::getConstant(typeBits, 2);
 
     {
@@ -262,7 +262,7 @@ TEST_F(TaintTest, Taint08) {
         const auto *slicedExpr = new IR::Slice(expr, 11, 4);
         slicedExpr = new IR::Slice(slicedExpr, 4, 3);
         const auto *taintedExpr = Taint::propagateTaint(env.getInternalMap(), slicedExpr);
-        const auto *expectedExpr = Utils::getTaintExpression(IR::getBitType(2));
+        const auto *expectedExpr = ToolsVariables::getTaintExpression(IR::getBitType(2));
         ASSERT_TRUE(taintedExpr->equiv(*expectedExpr));
     }
     {
@@ -271,7 +271,7 @@ TEST_F(TaintTest, Taint08) {
         const auto *slicedExpr = new IR::Slice(expr, 19, 12);
         slicedExpr = new IR::Slice(slicedExpr, 2, 0);
         const auto *taintedExpr = Taint::propagateTaint(env.getInternalMap(), slicedExpr);
-        const auto *expectedExpr = Utils::getTaintExpression(IR::getBitType(3));
+        const auto *expectedExpr = ToolsVariables::getTaintExpression(IR::getBitType(3));
         ASSERT_TRUE(taintedExpr->equiv(*expectedExpr));
     }
 }
@@ -285,7 +285,7 @@ TEST_F(TaintTest, Taint08) {
 /// Expected output: taint in most upper and lower 32 bits, taint in middle 64 bits
 TEST_F(TaintTest, Taint09) {
     // Taint64b
-    const auto *taint64b = Utils::getTaintExpression(IR::getBitType(64));
+    const auto *taint64b = ToolsVariables::getTaintExpression(IR::getBitType(64));
     ASSERT_TRUE(Taint::hasTaint({}, taint64b));
 
     ASSERT_TRUE(Taint::hasTaint({}, new IR::Slice(taint64b, 0, 0)));
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 f304ca0adee..13c91c6fda5 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
@@ -12,7 +12,7 @@
 
 #include "backends/p4test/version.h"
 #include "backends/p4tools/common/compiler/midend.h"
-#include "backends/p4tools/common/lib/util.h"
+#include "backends/p4tools/common/lib/variables.h"
 #include "frontends/common/options.h"
 #include "frontends/common/parseInput.h"
 #include "frontends/common/parser_options.h"
@@ -100,9 +100,9 @@ TEST_F(P4AssertsParserTest, Restrictions) {
         true);
     ASSERT_EQ(parsingResult.size(), (unsigned long)1);
     {
-        const auto &expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0,
-                                                           "ingress.ternary_table_mask_h.h.a1");
-        const auto &expr2 = P4Tools::Utils::getZombieConst(
+        const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
+            IR::Type_Bits::get(8), 0, "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");
         const auto *const1 = IR::getConstant(IR::Type_Bits::get(8), 0);
         const auto *const2 = IR::getConstant(IR::Type_Bits::get(8), 64);
@@ -111,15 +111,15 @@ TEST_F(P4AssertsParserTest, Restrictions) {
         ASSERT_TRUE(parsingResult[0][0]->equiv(*operation));
     }
     {
-        const auto &expr1 = P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0,
-                                                           "ingress.ternary_table_key_h.h.a1");
+        const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
+            IR::Type_Bits::get(8), 0, "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::Utils::getZombieConst(IR::Type_Bits::get(8), 0,
-                                                           "ingress.ternary_table_key_h.h.a");
+        const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(
+            IR::Type_Bits::get(8), 0, "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,10 +131,10 @@ 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::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a");
-    const auto &expr2 =
-        P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_2_key_h.h.b");
+    const auto &expr1 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), 0,
+                                                                     "ingress.table_1_key_h.h.a");
+    const auto &expr2 = P4Tools::ToolsVariables::getSymbolicVariable(IR::Type_Bits::get(8), 0,
+                                                                     "ingress.table_2_key_h.h.b");
     const auto *operation = new IR::Equ(expr1, expr2);
     ASSERT_TRUE(parsingResult[0][0]->equiv(*operation));
 }
@@ -144,10 +144,10 @@ 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::Utils::getZombieConst(IR::Type_Bits::get(8), 0,
-                                                "ingress.table_1_arg_ingress.MyAction10");
-    auto expr2 =
-        P4Tools::Utils::getZombieConst(IR::Type_Bits::get(8), 0, "ingress.table_1_key_h.h.a");
+    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);
     ASSERT_TRUE(parsingResult[1][0]->equiv(*operation));
 }
diff --git a/backends/p4tools/modules/testgen/test/transformations/saturation_arithm.cpp b/backends/p4tools/modules/testgen/test/transformations/saturation_arithm.cpp
index 754c1d8de9b..7d9bea1d0a1 100644
--- a/backends/p4tools/modules/testgen/test/transformations/saturation_arithm.cpp
+++ b/backends/p4tools/modules/testgen/test/transformations/saturation_arithm.cpp
@@ -124,6 +124,10 @@ void test(const IR::Expression *expression, const IR::AssignmentStatement *varia
     ASSERT_TRUE(variableValue);
 
     // eliminate saturation arithmetics
+    SymbolicConverter symbolicConverter;
+    expression = expression->apply(symbolicConverter);
+    variableValue = variableValue->apply(symbolicConverter)->checkedTo<IR::AssignmentStatement>();
+
     SaturationTransform transform;
     expression = expression->apply(transform);
 
@@ -134,12 +138,12 @@ void test(const IR::Expression *expression, const IR::AssignmentStatement *varia
     ASSERT_EQ(solver.checkSat({expression}), true);
 
     // getting model
-    Model model = *solver.getModel();
-    ASSERT_EQ(model.size(), 2U);
+    auto symbolMap = solver.getSymbolicMapping();
+    ASSERT_EQ(symbolMap.size(), 2U);
 
-    ASSERT_EQ(model.count(variableValue->left->checkedTo<IR::Member>()), 1U);
+    ASSERT_EQ(symbolMap.count(variableValue->left->checkedTo<IR::SymbolicVariable>()), 1U);
 
-    const auto *value = model.at(variableValue->left->checkedTo<IR::Member>());
+    const auto *value = symbolMap.at(variableValue->left->checkedTo<IR::SymbolicVariable>());
 
     ASSERT_TRUE(variableValue->right->is<IR::Constant>());
     ASSERT_TRUE(value->is<IR::Constant>());
diff --git a/backends/p4tools/modules/testgen/test/z3-solver/asrt_model.cpp b/backends/p4tools/modules/testgen/test/z3-solver/asrt_model.cpp
index 559a074b22a..1033b3c2efb 100644
--- a/backends/p4tools/modules/testgen/test/z3-solver/asrt_model.cpp
+++ b/backends/p4tools/modules/testgen/test/z3-solver/asrt_model.cpp
@@ -99,11 +99,13 @@ class Z3SolverTest : public P4ToolsTest {
         auto *const declVector = test->program->getDeclsByName("mau")->toVector();
         const auto *decl = (*declVector)[0];
         const auto *control = decl->to<IR::P4Control>();
+        SymbolicConverter converter;
         for (const auto *st : control->body->components) {
             if (const auto *as = st->to<IR::IfStatement>()) {
                 const auto *asExpr = as->condition;
                 if (asExpr->is<IR::Lss>()) {
-                    opLss = asExpr->to<IR::Lss>();
+                    // Convert members to symbolic variables.
+                    opLss = asExpr->apply(converter)->checkedTo<IR::Lss>();
                 }
             }
         }
@@ -135,30 +137,30 @@ TEST_F(Z3SolverTest, Assertion2Model) {
     asserts.push_back(opLss);
 
     // getting right variable
-    ASSERT_TRUE(opLss->right->is<IR::Member>());
-    const IR::StateVariable varB = opLss->right->to<IR::Member>();
+    ASSERT_TRUE(opLss->right->is<IR::SymbolicVariable>());
+    const auto *const varB = opLss->right->to<IR::SymbolicVariable>();
 
     // getting numeric and left variable
     ASSERT_TRUE(opLss->left->is<IR::Add>());
     const auto *opAdd = opLss->left->to<IR::Add>();
-    ASSERT_TRUE(opAdd->left->is<IR::Member>());
-    const IR::StateVariable varA = opAdd->left->to<IR::Member>();
+    ASSERT_TRUE(opAdd->left->is<IR::SymbolicVariable>());
+    const auto *const varA = opAdd->left->to<IR::SymbolicVariable>();
     ASSERT_TRUE(opAdd->right->is<IR::Constant>());
     const auto *addToA = opAdd->right->to<IR::Constant>();
 
-    // getting model without check satisfiable
-    EXPECT_THROW(solver.getModel(), Util::CompilerBug);
+    // getting mapping without check satisfiable
+    EXPECT_THROW(Model(solver.getSymbolicMapping()), Util::CompilerBug);
 
     // checking satisfiability
     ASSERT_EQ(solver.checkSat(asserts), true);
-    Model model2 = *solver.getModel();
-    ASSERT_EQ(model2.size(), 2u);
+    auto symbolMap2 = solver.getSymbolicMapping();
+    ASSERT_EQ(symbolMap2.size(), 2U);
 
     // checking variables
-    ASSERT_GT(model2.count(varA), 0u);
-    ASSERT_GT(model2.count(varB), 0u);
-    const auto *valueA = model2.at(varA)->to<IR::Literal>();
-    const auto *valueB = model2.at(varB)->to<IR::Literal>();
+    ASSERT_GT(symbolMap2.count(varA), 0U);
+    ASSERT_GT(symbolMap2.count(varB), 0U);
+    const auto *valueA = symbolMap2.at(varA)->to<IR::Literal>();
+    const auto *valueB = symbolMap2.at(varB)->to<IR::Literal>();
 
     // input expression was hdr.h.a + 4w15 < hdr.h.b
     // lets calculate it: valueA + addToA < valueB
@@ -177,19 +179,19 @@ TEST_F(Z3SolverTest, Assertion2Model) {
     asserts.push_back(opLss);
 
     // try to get model, should have two assertions now
-    Model model3 = *solver.getModel();
-    ASSERT_EQ(model3.size(), 2u);
+    auto symbolMap3 = solver.getSymbolicMapping();
+    ASSERT_EQ(symbolMap3.size(), 2U);
 
     // checking satisfiability
     ASSERT_EQ(solver.checkSat(asserts), true);
-    Model model4 = *solver.getModel();
-    ASSERT_EQ(model4.size(), 2u);
+    auto symbolMap4 = solver.getSymbolicMapping();
+    ASSERT_EQ(symbolMap4.size(), 2U);
 
     // checking variables
-    ASSERT_GT(model4.count(varA), 0u);
-    ASSERT_GT(model4.count(varB), 0u);
-    model4.at(varA)->checkedTo<IR::Literal>();
-    model4.at(varB)->checkedTo<IR::Literal>();
+    ASSERT_GT(symbolMap4.count(varA), 0U);
+    ASSERT_GT(symbolMap4.count(varB), 0U);
+    symbolMap4.at(varA)->checkedTo<IR::Literal>();
+    symbolMap4.at(varB)->checkedTo<IR::Literal>();
 
     // input expression was hdr.h.a + 4w15 < hdr.h.b
     // lets calculate it: valueA + addToA < valueB
diff --git a/backends/p4tools/modules/testgen/test/z3-solver/expressions.cpp b/backends/p4tools/modules/testgen/test/z3-solver/expressions.cpp
index 73699f59028..8f1aedc2a42 100644
--- a/backends/p4tools/modules/testgen/test/z3-solver/expressions.cpp
+++ b/backends/p4tools/modules/testgen/test/z3-solver/expressions.cpp
@@ -115,6 +115,11 @@ void test(const IR::Expression *expression, const IR::AssignmentStatement *varia
     ASSERT_TRUE(expression);
     ASSERT_TRUE(variableValue);
 
+    // Convert members to symbolic variables.
+    SymbolicConverter symbolicConverter;
+    expression = expression->apply(symbolicConverter);
+    variableValue = variableValue->apply(symbolicConverter)->checkedTo<IR::AssignmentStatement>();
+
     // adding assertion
     Z3Solver solver;
 
@@ -122,12 +127,13 @@ void test(const IR::Expression *expression, const IR::AssignmentStatement *varia
     ASSERT_EQ(solver.checkSat({expression}), true);
 
     // getting model
-    Model model = *solver.getModel();
-    ASSERT_EQ(model.size(), 2U);
+    auto symbolMap = solver.getSymbolicMapping();
+
+    ASSERT_EQ(symbolMap.size(), 2U);
 
-    ASSERT_EQ(model.count(variableValue->left->checkedTo<IR::Member>()), 1U);
+    ASSERT_EQ(symbolMap.count(variableValue->left->checkedTo<IR::SymbolicVariable>()), 1U);
 
-    const auto *value = model.at(variableValue->left->checkedTo<IR::Member>());
+    const auto *value = symbolMap.at(variableValue->left->checkedTo<IR::SymbolicVariable>());
 
     if (variableValue->right->is<IR::BoolLiteral>()) {
         ASSERT_TRUE(variableValue->right->is<IR::BoolLiteral>());
diff --git a/backends/p4tools/p4tools.def b/backends/p4tools/p4tools.def
index c03f887e304..4fb1a836632 100644
--- a/backends/p4tools/p4tools.def
+++ b/backends/p4tools/p4tools.def
@@ -1,14 +1,19 @@
 /// Represents a reference to an object in a P4 program.
 ///
-/// This is a thin wrapper around a 'const IR::Member*' to (1) enforce invariants on which forms of
-/// Members can represent state variables and (2) enable the use of IR::StateVariables as map keys.
+/// This is a thin wrapper around a 'const Member*' to (1) enforce invariants on which forms of
+/// Members can represent state variables and (2) enable the use of StateVariables as map keys.
 class StateVariable : Expression {
+    #noconstructor
+
     /// The wrapped member.
     const Member *member;
 
+    /// The expression type is derived from the member.
+    StateVariable(Member member) : Expression(member->getSourceInfo(), member->type), member(member) {}
+
     /// Implicit conversions to allow implementations to be treated like a Member*.
 #emit
-    operator const IR::Member *() const { return member; }
+    operator const Member *() const { return member; }
 #end
     Member const &operator*() const { return *member; }
     Member operator->() const { return member; }
@@ -85,6 +90,27 @@ class TaintExpression : Expression {
     dbprint { out << "TaintedExpression(" << type << ")"; }
 }
 
+/// Signifies that a particular expression is a symbolic variable with a label.
+/// These variables are intended to be consumed by SMT/SAT solvers.
+class SymbolicVariable : Expression {
+#noconstructor
+
+    /// The label of the symbolic variable.
+    cstring label;
+
+    /// A symbolic variable always has a type and no source info.
+    SymbolicVariable(Type type, cstring label) : Expression(type), label(label) {}
+
+    /// Implements comparisons so that SymbolicVariables can be used as map keys.
+    bool operator<(const SymbolicVariable &other) const {
+        return label < other.label;
+    }
+
+    toString { return "|" + label +"(" + type->toString() + ")|"; }
+
+    dbprint { out << "|" + label +"(" << type << ")|"; }
+}
+
 /// This type replaces Type_Varbits and can store information about the current size
 class Extracted_Varbits : Type_Bits {
     /// The assigned size of this varbit (assigned by extract calls).
@@ -114,11 +140,18 @@ class Extracted_Varbits : Type_Bits {
 }
 
 /// Defines a concolic variable that may be part of expressions.
-/// This variable must later be resolved and is converted in a symbolic expression.
-class ConcolicVariable : Expression {
-    /// The name of the concolic method that this variable targets.
-    cstring concolicMethodName;
+/// This variable must later be resolved and is converted into a symbolic expression.
+class ConcolicVariable : SymbolicVariable {
+    #noconstructor
+
+private:
+    static cstring produceLabel(cstring methodName, int srcIdentifier, int concolicId ) {
+        std::stringstream sstr;
+        sstr << methodName << "_" << srcIdentifier << "_" << concolicId;
+        return sstr.str();
+    }
 
+public:
     /// Arguments to the concolic method.
     Vector<Argument> arguments;
 
@@ -131,32 +164,40 @@ class ConcolicVariable : Expression {
     /// Nodes that are associated with this concolic variable. This may be declarations.
     optional inline IndexedVector<Node> associatedNodes;
 
-    /// This is the member representation of this concolic variable.
-    Member concolicMember = nullptr;
+    /// The name of the concolic method that this variable targets.
+    inline cstring concolicMethodName = "";
 
     toString {
         cstring argumentStr;
         cstring sep = "";
-        for (auto arg : *arguments) {
+        for (const auto *arg : *arguments) {
             argumentStr += sep + arg->toString();
             sep = ", ";
         }
-        return "Concolic_" + concolicMethodName + "_" + srcIdentifier + "_" + concolicId + "(" +
-               argumentStr + ")";
+        return "Concolic_" + label + "(" + argumentStr + ")";
     }
 
     dbprint {
-        out << "Concolic_" << concolicMethodName << "_" << srcIdentifier << "_" << concolicId << "("
-            << arguments << ")";
+        out << "Concolic_" << label << "(" << arguments << ")";
     }
 
     visit_children { v.visit(type, "type"); }
 
-    ConcolicVariable {
-        std::stringstream varName;
-        varName << concolicMethodName << "_" << srcIdentifier;
-        concolicMember =
-            new Member(srcInfo, type, new PathExpression(new Path(varName.str().c_str())),
-                       std::to_string(concolicId).c_str());
-    }
+    ConcolicVariable(const Type *type, cstring methodName,
+                     const Vector<Argument> *arguments, int srcIdentifier, int concolicId,
+                     const IndexedVector<Node> &associatedNodes)
+        : SymbolicVariable(type, produceLabel(methodName, srcIdentifier, concolicId)),
+          arguments(arguments),
+          srcIdentifier(srcIdentifier),
+          concolicId(concolicId),
+          associatedNodes(associatedNodes),
+          concolicMethodName(methodName) {}
+
+    ConcolicVariable(const Type *type, cstring methodName,
+                     const Vector<Argument> *arguments, int srcIdentifier, int concolicId)
+        : SymbolicVariable(type, produceLabel(methodName, srcIdentifier, concolicId)),
+          arguments(arguments),
+          srcIdentifier(srcIdentifier),
+          concolicId(concolicId),
+          concolicMethodName(methodName) {}
 }
diff --git a/ir/ir.def b/ir/ir.def
index 16adc32e861..1dd2bf359d5 100644
--- a/ir/ir.def
+++ b/ir/ir.def
@@ -44,8 +44,8 @@
 
   inline      The field (of IR class type) should be defined directly in the object
               rather than being converted to a const T * as described above.
-  NullOK      The field is a ppointer and may be null (verify will check that it is not otherwise)
-  optional    The field may be proveded as an argument to the constructor but need not be.
+  NullOK      The field is a pointer and may be null (verify will check that it is not otherwise)
+  optional    The field may be provided as an argument to the constructor but need not be.
               (overloaded constructors will be created as needed)
 
   Unless there is a '#noconstructor' tag in the class, a constructor