diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index b6aac04bff3..cc7c5cf08f6 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -1,3 +1,3 @@
 # The P4Tools repository is owned by the following maintainers.
-backends/p4tools @fruffy @pkotikal @jnfoster @mbudiu-vmw
+backends/p4tools @fruffy @pkotikal @jnfoster
 
diff --git a/backends/p4tools/modules/testgen/CMakeLists.txt b/backends/p4tools/modules/testgen/CMakeLists.txt
index 8fe6a1f7450..23cf886f1de 100644
--- a/backends/p4tools/modules/testgen/CMakeLists.txt
+++ b/backends/p4tools/modules/testgen/CMakeLists.txt
@@ -77,8 +77,8 @@ FetchContent_MakeAvailable(inja)
 # Testgen libraries.
 set(
   TESTGEN_LIBS
-  p4tools-common
-  inja
+  PRIVATE p4tools-common
+  PUBLIC inja
 )
 
 file(GLOB testgen_targets RELATIVE ${CMAKE_CURRENT_SOURCE_DIR}/targets ${CMAKE_CURRENT_SOURCE_DIR}/targets/*)
@@ -114,15 +114,17 @@ configure_file(register.h.in register.h)
 # The library.
 add_p4tools_library(testgen ${TESTGEN_SOURCES})
 # Make sure the testgen library and anything that links to it see both the Z3 and Inja includes.
-# also links to Z3 and inja
 target_link_libraries(testgen PUBLIC p4tools-common inja)
 
 # The executable.
 add_p4tools_executable(p4testgen main.cpp)
 target_link_libraries(
   p4testgen
-  testgen
+  PRIVATE testgen
   ${TESTGEN_LIBS}
+  ${P4C_LIBRARIES}
+  ${P4C_LIB_DEPS}
+  ${CMAKE_THREAD_LIBS_INIT}
 )
 
 add_custom_target(
@@ -148,6 +150,9 @@ if(ENABLE_GTESTS)
     PRIVATE testgen
     PRIVATE gtest
     ${TESTGEN_LIBS}
+    ${P4C_LIBRARIES}
+    ${P4C_LIB_DEPS}
+    ${CMAKE_THREAD_LIBS_INIT}
   )
 
   if(ENABLE_TESTING)
diff --git a/backends/p4tools/modules/testgen/core/target.cpp b/backends/p4tools/modules/testgen/core/target.cpp
index f5b12bfea52..86ba790a5ad 100644
--- a/backends/p4tools/modules/testgen/core/target.cpp
+++ b/backends/p4tools/modules/testgen/core/target.cpp
@@ -38,12 +38,9 @@ const ProgramInfo *TestgenTarget::initProgramImpl(const IR::P4Program *program)
 
 const TestgenTarget &TestgenTarget::get() { return Target::get<TestgenTarget>("testgen"); }
 
-int TestgenTarget::getPortNumWidthBits() { return get().getPortNumWidthBitsImpl(); }
-
 TestBackEnd *TestgenTarget::getTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                           const std::filesystem::path &testPath,
-                                           std::optional<uint32_t> seed) {
-    return get().getTestBackendImpl(programInfo, symbex, testPath, seed);
+                                           const std::filesystem::path &testPath) {
+    return get().getTestBackendImpl(programInfo, symbex, testPath);
 }
 
 const ProgramInfo *TestgenTarget::initProgram(const IR::P4Program *program) {
diff --git a/backends/p4tools/modules/testgen/core/target.h b/backends/p4tools/modules/testgen/core/target.h
index f363a1f268f..ca591dfa7ad 100644
--- a/backends/p4tools/modules/testgen/core/target.h
+++ b/backends/p4tools/modules/testgen/core/target.h
@@ -34,11 +34,7 @@ class TestgenTarget : public Target {
 
     /// Returns the test back end associated with this P4Testgen target.
     static TestBackEnd *getTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                       const std::filesystem::path &testPath,
-                                       std::optional<uint32_t> seed);
-
-    /// The width of a port number, in bits.
-    static int getPortNumWidthBits();
+                                       const std::filesystem::path &testPath);
 
     /// Provides a CmdStepper implementation for this target.
     static CmdStepper *getCmdStepper(ExecutionState &state, AbstractSolver &solver,
@@ -63,14 +59,10 @@ class TestgenTarget : public Target {
     virtual const ProgramInfo *initProgramImpl(const IR::P4Program *program,
                                                const IR::Declaration_Instance *mainDecl) const = 0;
 
-    /// @see getPortNumWidthBits.
-    [[nodiscard]] virtual int getPortNumWidthBitsImpl() const = 0;
-
     /// @see getTestBackend.
     virtual TestBackEnd *getTestBackendImpl(const ProgramInfo &programInfo,
                                             SymbolicExecutor &symbex,
-                                            const std::filesystem::path &testPath,
-                                            std::optional<uint32_t> seed) const = 0;
+                                            const std::filesystem::path &testPath) const = 0;
 
     /// @see getCmdStepper.
     virtual CmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
@@ -86,7 +78,6 @@ class TestgenTarget : public Target {
     /// Utility function. Converts the list of arguments @inputArgs to a list of type declarations
     ///  and appends the result to @v. Any names appearing in the arguments are
     /// resolved with @ns.
-    //
     static void argumentsToTypeDeclarations(const IR::IGeneralNamespace *ns,
                                             const IR::Vector<IR::Argument> *inputArgs,
                                             std::vector<const IR::Type_Declaration *> &resultDecls);
diff --git a/backends/p4tools/modules/testgen/lib/final_state.cpp b/backends/p4tools/modules/testgen/lib/final_state.cpp
index ab1db0add99..5679ae0afc6 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.cpp
+++ b/backends/p4tools/modules/testgen/lib/final_state.cpp
@@ -118,13 +118,13 @@ std::optional<std::reference_wrapper<const FinalState>> FinalState::computeConco
     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) {
+    for (const auto &varTuple : completedModel.get()) {
         model.emplace(varTuple.first, varTuple.second);
     }
     return *new FinalState(solver, state, model);
 }
 
-const Model *FinalState::getCompletedModel() const { return &completedModel; }
+const Model &FinalState::getCompletedModel() const { return completedModel; }
 
 AbstractSolver &FinalState::getSolver() const { return solver; }
 
diff --git a/backends/p4tools/modules/testgen/lib/final_state.h b/backends/p4tools/modules/testgen/lib/final_state.h
index 24376258f1e..a91af516814 100644
--- a/backends/p4tools/modules/testgen/lib/final_state.h
+++ b/backends/p4tools/modules/testgen/lib/final_state.h
@@ -26,7 +26,7 @@ class FinalState {
     std::reference_wrapper<const ExecutionState> state;
 
     /// The final model which has been augmented with environment completions.
-    const Model &completedModel;
+    std::reference_wrapper<const Model> completedModel;
 
     /// The final program trace.
     std::vector<std::reference_wrapper<const TraceEvent>> trace;
@@ -61,7 +61,7 @@ class FinalState {
         const ConcolicVariableMap &resolvedConcolicVariables) const;
 
     /// @returns the model after it was augmented by completions from the symbolic environment.
-    [[nodiscard]] const Model *getCompletedModel() const;
+    [[nodiscard]] const Model &getCompletedModel() const;
 
     /// @returns the solver associated with this final state.
     [[nodiscard]] AbstractSolver &getSolver() const;
diff --git a/backends/p4tools/modules/testgen/lib/test_backend.cpp b/backends/p4tools/modules/testgen/lib/test_backend.cpp
index 1019787d7e3..18eb5be9d4e 100644
--- a/backends/p4tools/modules/testgen/lib/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/lib/test_backend.cpp
@@ -35,7 +35,6 @@ bool TestBackEnd::run(const FinalState &state) {
         // Evaluate the model and extract the input and output packets.
         const auto *executionState = state.getExecutionState();
         const auto *outputPacketExpr = executionState->getPacketBuffer();
-        const auto *completedModel = state.getCompletedModel();
         const auto *outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
         const auto &coverableNodes = programInfo.getCoverableNodes();
         const auto *programTraces = state.getTraces();
@@ -63,7 +62,7 @@ bool TestBackEnd::run(const FinalState &state) {
 
         // Execute concolic functions that may occur in the output packet, the output port,
         // or any path conditions.
-        auto concolicResolver = ConcolicResolver(*completedModel, *executionState,
+        auto concolicResolver = ConcolicResolver(state.getCompletedModel(), *executionState,
                                                  *programInfo.getConcolicMethodImpls());
 
         outputPacketExpr->apply(concolicResolver);
@@ -85,10 +84,10 @@ bool TestBackEnd::run(const FinalState &state) {
         auto replacedState = concolicOptState.value().get();
         executionState = replacedState.getExecutionState();
         outputPacketExpr = executionState->getPacketBuffer();
-        completedModel = replacedState.getCompletedModel();
+        const auto &completedModel = replacedState.getCompletedModel();
         outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
 
-        auto testInfo = produceTestInfo(executionState, completedModel, outputPacketExpr,
+        auto testInfo = produceTestInfo(executionState, &completedModel, outputPacketExpr,
                                         outputPortExpr, programTraces);
 
         // Add a list of tracked branches to the test output, too.
@@ -103,7 +102,7 @@ bool TestBackEnd::run(const FinalState &state) {
             printPerformanceReport(false);
             return needsToTerminate(testCount);
         }
-        const auto *testSpec = createTestSpec(executionState, completedModel, testInfo);
+        const auto *testSpec = createTestSpec(executionState, &completedModel, testInfo);
 
         // Commit an update to the visited statements.
         // Only do this once we are sure we are generating a test.
diff --git a/backends/p4tools/modules/testgen/lib/test_backend.h b/backends/p4tools/modules/testgen/lib/test_backend.h
index 958bd6c185d..5cb75898c2d 100644
--- a/backends/p4tools/modules/testgen/lib/test_backend.h
+++ b/backends/p4tools/modules/testgen/lib/test_backend.h
@@ -1,8 +1,7 @@
 #ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_H_
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_H_
 
-#include <stdint.h>
-
+#include <cstdint>
 #include <functional>
 #include <optional>
 #include <vector>
diff --git a/backends/p4tools/modules/testgen/options.cpp b/backends/p4tools/modules/testgen/options.cpp
index 6fa480cafa2..704cf6f5ceb 100644
--- a/backends/p4tools/modules/testgen/options.cpp
+++ b/backends/p4tools/modules/testgen/options.cpp
@@ -16,7 +16,7 @@
 
 #include "backends/p4tools/modules/testgen/lib/logging.h"
 
-namespace P4Tools {
+namespace P4Tools::P4Testgen {
 
 TestgenOptions &TestgenOptions::get() {
     static TestgenOptions INSTANCE;
@@ -327,4 +327,4 @@ TestgenOptions::TestgenOptions()
         "produce no tests or only tests that contain counter examples.");
 }
 
-}  // namespace P4Tools
+}  // namespace P4Tools::P4Testgen
diff --git a/backends/p4tools/modules/testgen/options.h b/backends/p4tools/modules/testgen/options.h
index 3cc2e1f5bc2..28e40702228 100644
--- a/backends/p4tools/modules/testgen/options.h
+++ b/backends/p4tools/modules/testgen/options.h
@@ -11,7 +11,7 @@
 
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h"
 
-namespace P4Tools {
+namespace P4Tools::P4Testgen {
 
 /// Encapsulates and processes command-line options for P4Testgen.
 class TestgenOptions : public AbstractP4cToolOptions {
@@ -84,6 +84,6 @@ class TestgenOptions : public AbstractP4cToolOptions {
     TestgenOptions();
 };
 
-}  // namespace P4Tools
+}  // namespace P4Tools::P4Testgen
 
 #endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_OPTIONS_H_ */
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/CMakeLists.txt b/backends/p4tools/modules/testgen/targets/bmv2/CMakeLists.txt
index 8bcc04d9ed5..234adee0ba9 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/CMakeLists.txt
+++ b/backends/p4tools/modules/testgen/targets/bmv2/CMakeLists.txt
@@ -34,8 +34,5 @@ execute_process(COMMAND ln -sfn ${P4C_SOURCE_DIR}/backends/bmv2/run-bmv2-test.py
 
 set(
   TESTGEN_LIBS ${TESTGEN_LIBS}
-  ${P4C_LIBRARIES}
-  ${P4C_LIB_DEPS}
-  ${CMAKE_THREAD_LIBS_INIT}
   PARENT_SCOPE
 )
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/constants.h b/backends/p4tools/modules/testgen/targets/bmv2/constants.h
index 5e750e68471..747c40b483d 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/constants.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/constants.h
@@ -34,6 +34,8 @@ class BMv2Constants {
     enum CloneType { I2E = 0, E2E = 1 };
     /// Meter colors are defined in v1model.p4
     enum METER_COLOR { GREEN = 0, YELLOW = 1, RED = 2 };
+    /// Port width in bits.
+    static constexpr int PORT_BIT_WIDTH = 9;
 
     /// Other useful constants
     static constexpr int STF_MIN_PKT_SIZE = 22;
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
index be5a358ca8b..14769fcf9a4 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
@@ -357,8 +357,7 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
             IR::ID & /*methodName*/, const IR::Vector<IR::Argument> *args,
             const ExecutionState &state, SmallStepEvaluator::Result &result) {
              auto &nextState = state.clone();
-             const auto *nineBitType =
-                 IR::getBitType(Bmv2V1ModelTestgenTarget::getPortNumWidthBits());
+             const auto *nineBitType = IR::getBitType(BMv2Constants::PORT_BIT_WIDTH);
              const auto *metadataLabel = args->at(0)->expression;
              if (!(metadataLabel->is<IR::Member>() || metadataLabel->is<IR::PathExpression>())) {
                  TESTGEN_UNIMPLEMENTED("Drop input %1% of type %2% not supported", metadataLabel,
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp b/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp
index a9a9c50a59c..32b971f3b12 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp
@@ -153,7 +153,7 @@ std::vector<Continuation::Command> Bmv2V1ModelProgramInfo::processDeclaration(
     // processing. For example, the egress port.
     if ((archMember->blockName == "Ingress")) {
         auto *egressPortVar =
-            new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+            new IR::Member(IR::getBitType(BMv2Constants::PORT_BIT_WIDTH),
                            new IR::PathExpression("*standard_metadata"), "egress_port");
         auto *portStmt = new IR::AssignmentStatement(egressPortVar, getTargetOutputPortVar());
         cmds.emplace_back(portStmt);
@@ -187,9 +187,9 @@ std::vector<Continuation::Command> Bmv2V1ModelProgramInfo::processDeclaration(
 }
 
 const IR::StateVariable &Bmv2V1ModelProgramInfo::getTargetInputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*standard_metadata"), "ingress_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(BMv2Constants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*standard_metadata"),
+                                                 "ingress_port"));
 }
 
 const IR::Expression *Bmv2V1ModelProgramInfo::getPortConstraint(const IR::StateVariable &portVar) {
@@ -200,9 +200,9 @@ const IR::Expression *Bmv2V1ModelProgramInfo::getPortConstraint(const IR::StateV
 }
 
 const IR::StateVariable &Bmv2V1ModelProgramInfo::getTargetOutputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*standard_metadata"), "egress_spec"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(BMv2Constants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*standard_metadata"),
+                                                 "egress_spec"));
 }
 
 const IR::Expression *Bmv2V1ModelProgramInfo::dropIsActive() const {
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/target.cpp b/backends/p4tools/modules/testgen/targets/bmv2/target.cpp
index bdfb009d62e..c5981999dde 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/target.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/target.cpp
@@ -67,15 +67,12 @@ const Bmv2V1ModelProgramInfo *Bmv2V1ModelTestgenTarget::initProgramImpl(
     return new Bmv2V1ModelProgramInfo(program, programmableBlocks, declIdToGress);
 }
 
-Bmv2TestBackend *Bmv2V1ModelTestgenTarget::getTestBackendImpl(const ProgramInfo &programInfo,
-                                                              SymbolicExecutor &symbex,
-                                                              const std::filesystem::path &testPath,
-                                                              std::optional<uint32_t> seed) const {
-    return new Bmv2TestBackend(programInfo, symbex, testPath, seed);
+Bmv2TestBackend *Bmv2V1ModelTestgenTarget::getTestBackendImpl(
+    const ProgramInfo &programInfo, SymbolicExecutor &symbex,
+    const std::filesystem::path &testPath) const {
+    return new Bmv2TestBackend(programInfo, symbex, testPath);
 }
 
-int Bmv2V1ModelTestgenTarget::getPortNumWidthBitsImpl() const { return 9; }
-
 Bmv2V1ModelCmdStepper *Bmv2V1ModelTestgenTarget::getCmdStepperImpl(
     ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const {
     return new Bmv2V1ModelCmdStepper(state, solver, programInfo);
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/target.h b/backends/p4tools/modules/testgen/targets/bmv2/target.h
index 537dbafc59b..3a3019f6a42 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/target.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/target.h
@@ -29,11 +29,8 @@ class Bmv2V1ModelTestgenTarget : public TestgenTarget {
     const Bmv2V1ModelProgramInfo *initProgramImpl(
         const IR::P4Program *program, const IR::Declaration_Instance *mainDecl) const override;
 
-    [[nodiscard]] int getPortNumWidthBitsImpl() const override;
-
     Bmv2TestBackend *getTestBackendImpl(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                        const std::filesystem::path &testPath,
-                                        std::optional<uint32_t> seed) const override;
+                                        const std::filesystem::path &testPath) const override;
 
     Bmv2V1ModelCmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                              const ProgramInfo &programInfo) const override;
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp b/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp
index c69bc1a6fb8..43eb5fc6b71 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp
@@ -39,8 +39,7 @@ const std::set<std::string> Bmv2TestBackend::SUPPORTED_BACKENDS = {"PTF", "STF",
                                                                    "METADATA"};
 
 Bmv2TestBackend::Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                 const std::filesystem::path &testPath,
-                                 std::optional<uint32_t> seed)
+                                 const std::filesystem::path &testPath)
     : TestBackEnd(programInfo, symbex) {
     cstring testBackendString = TestgenOptions::get().testBackend;
     if (testBackendString.isNullOrEmpty()) {
@@ -50,6 +49,7 @@ Bmv2TestBackend::Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecuto
         exit(EXIT_FAILURE);
     }
 
+    auto seed = TestgenOptions::get().seed;
     if (testBackendString == "PTF") {
         testWriter = new PTF(testPath, seed);
     } else if (testBackendString == "STF") {
diff --git a/backends/p4tools/modules/testgen/targets/bmv2/test_backend.h b/backends/p4tools/modules/testgen/targets/bmv2/test_backend.h
index 68246a5ab18..d8015952152 100644
--- a/backends/p4tools/modules/testgen/targets/bmv2/test_backend.h
+++ b/backends/p4tools/modules/testgen/targets/bmv2/test_backend.h
@@ -36,7 +36,7 @@ class Bmv2TestBackend : public TestBackEnd {
 
  public:
     explicit Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                             const std::filesystem::path &testPath, std::optional<uint32_t> seed);
+                             const std::filesystem::path &testPath);
 
     TestBackEnd::TestInfo produceTestInfo(
         const ExecutionState *executionState, const Model *completedModel,
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/CMakeLists.txt b/backends/p4tools/modules/testgen/targets/ebpf/CMakeLists.txt
index b78df288df4..80639881e1f 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/CMakeLists.txt
+++ b/backends/p4tools/modules/testgen/targets/ebpf/CMakeLists.txt
@@ -27,8 +27,5 @@ execute_process(COMMAND ln -sfn ${P4C_SOURCE_DIR}/backends/ebpf/run-ebpf-test.py
 
 set(
   TESTGEN_LIBS ${TESTGEN_LIBS}
-  ${P4C_LIBRARIES}
-  ${P4C_LIB_DEPS}
-  ${CMAKE_THREAD_LIBS_INIT}
   PARENT_SCOPE
 )
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/constants.h b/backends/p4tools/modules/testgen/targets/ebpf/constants.h
index 5432602099e..05dc347f11e 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/constants.h
+++ b/backends/p4tools/modules/testgen/targets/ebpf/constants.h
@@ -9,6 +9,8 @@ class EBPFConstants {
  public:
     /// eBPF-internal drop variable.
     static const IR::PathExpression ACCEPT_VAR;
+    /// Port width in bits.
+    static constexpr int PORT_BIT_WIDTH = 9;
 };
 
 }  // namespace P4Tools::P4Testgen::EBPF
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp b/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp
index fdf0360b4b6..69171bc01a0 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp
@@ -106,15 +106,13 @@ std::vector<Continuation::Command> EBPFProgramInfo::processDeclaration(
 }
 
 const IR::StateVariable &EBPFProgramInfo::getTargetInputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*"), "input_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(EBPFConstants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*"), "input_port"));
 }
 
 const IR::StateVariable &EBPFProgramInfo::getTargetOutputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*"), "output_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(EBPFConstants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*"), "output_port"));
 }
 
 const IR::Expression *EBPFProgramInfo::dropIsActive() const {
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/target.cpp b/backends/p4tools/modules/testgen/targets/ebpf/target.cpp
index a4b7fe124e1..6c9d07c8afd 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/target.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/target.cpp
@@ -67,15 +67,12 @@ const EBPFProgramInfo *EBPFTestgenTarget::initProgramImpl(
     return new EBPFProgramInfo(program, programmableBlocks);
 }
 
-EBPFTestBackend *EBPFTestgenTarget::getTestBackendImpl(const ProgramInfo &programInfo,
-                                                       SymbolicExecutor &symbex,
-                                                       const std::filesystem::path &testPath,
-                                                       std::optional<uint32_t> seed) const {
-    return new EBPFTestBackend(programInfo, symbex, testPath, seed);
+EBPFTestBackend *EBPFTestgenTarget::getTestBackendImpl(
+    const ProgramInfo &programInfo, SymbolicExecutor &symbex,
+    const std::filesystem::path &testPath) const {
+    return new EBPFTestBackend(programInfo, symbex, testPath);
 }
 
-int EBPFTestgenTarget::getPortNumWidthBitsImpl() const { return 9; }
-
 EBPFCmdStepper *EBPFTestgenTarget::getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                                      const ProgramInfo &programInfo) const {
     return new EBPFCmdStepper(state, solver, programInfo);
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/target.h b/backends/p4tools/modules/testgen/targets/ebpf/target.h
index edfbf597a32..88809c8b109 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/target.h
+++ b/backends/p4tools/modules/testgen/targets/ebpf/target.h
@@ -29,11 +29,8 @@ class EBPFTestgenTarget : public TestgenTarget {
     const EBPFProgramInfo *initProgramImpl(const IR::P4Program *program,
                                            const IR::Declaration_Instance *mainDecl) const override;
 
-    int getPortNumWidthBitsImpl() const override;
-
     EBPFTestBackend *getTestBackendImpl(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                        const std::filesystem::path &testPath,
-                                        std::optional<uint32_t> seed) const override;
+                                        const std::filesystem::path &testPath) const override;
 
     EBPFCmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                       const ProgramInfo &programInfo) const override;
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp b/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp
index 641add1ec5c..1c6ae380dbf 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/targets/ebpf/test_backend.cpp
@@ -31,12 +31,12 @@ const big_int EBPFTestBackend::ZERO_PKT_MAX = 0xffffffff;
 const std::vector<std::string> EBPFTestBackend::SUPPORTED_BACKENDS = {"STF"};
 
 EBPFTestBackend::EBPFTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                 const std::filesystem::path &testPath,
-                                 std::optional<uint32_t> seed)
+                                 const std::filesystem::path &testPath)
     : TestBackEnd(programInfo, symbex) {
     cstring testBackendString = TestgenOptions::get().testBackend;
+
     if (testBackendString == "STF") {
-        testWriter = new STF(testPath.c_str(), seed);
+        testWriter = new STF(testPath.c_str(), TestgenOptions::get().seed);
     } else {
         std::stringstream supportedBackendString;
         bool isFirst = true;
diff --git a/backends/p4tools/modules/testgen/targets/ebpf/test_backend.h b/backends/p4tools/modules/testgen/targets/ebpf/test_backend.h
index 918ecb77df8..da3abbb597b 100644
--- a/backends/p4tools/modules/testgen/targets/ebpf/test_backend.h
+++ b/backends/p4tools/modules/testgen/targets/ebpf/test_backend.h
@@ -35,7 +35,7 @@ class EBPFTestBackend : public TestBackEnd {
 
  public:
     explicit EBPFTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                             const std::filesystem::path &testPath, std::optional<uint32_t> seed);
+                             const std::filesystem::path &testPath);
 
     TestBackEnd::TestInfo produceTestInfo(
         const ExecutionState *executionState, const Model *completedModel,
diff --git a/backends/p4tools/modules/testgen/targets/pna/CMakeLists.txt b/backends/p4tools/modules/testgen/targets/pna/CMakeLists.txt
index afd2c6c6113..052aec3fed5 100644
--- a/backends/p4tools/modules/testgen/targets/pna/CMakeLists.txt
+++ b/backends/p4tools/modules/testgen/targets/pna/CMakeLists.txt
@@ -28,8 +28,5 @@ set(
 
 set(
   TESTGEN_LIBS ${TESTGEN_LIBS}
-  ${P4C_LIBRARIES}
-  ${P4C_LIB_DEPS}
-  ${CMAKE_THREAD_LIBS_INIT}
   PARENT_SCOPE
 )
diff --git a/backends/p4tools/modules/testgen/targets/pna/constants.h b/backends/p4tools/modules/testgen/targets/pna/constants.h
index 462bfae1fed..9f2cdc5d4a4 100644
--- a/backends/p4tools/modules/testgen/targets/pna/constants.h
+++ b/backends/p4tools/modules/testgen/targets/pna/constants.h
@@ -22,6 +22,8 @@ class PnaConstants {
     static const IR::Member OUTPUT_PORT_VAR;
     /// PNA-internal parser error label.
     static const IR::Member PARSER_ERROR;
+    /// Port width in bits.
+    static constexpr int PORT_BIT_WIDTH = 9;
 };
 
 /// variabless are variables that can be controlled and set by P4Testgen.
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 65cd11eb9d6..50cca28146c 100644
--- a/backends/p4tools/modules/testgen/targets/pna/shared_program_info.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/shared_program_info.cpp
@@ -31,9 +31,9 @@ const ordered_map<cstring, const IR::Type_Declaration *>
 }
 
 const IR::StateVariable &SharedPnaProgramInfo::getTargetInputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*parser_istd"), "input_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(PnaConstants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*parser_istd"),
+                                                 "input_port"));
 }
 
 const IR::StateVariable &SharedPnaProgramInfo::getTargetOutputPortVar() const {
diff --git a/backends/p4tools/modules/testgen/targets/pna/target.cpp b/backends/p4tools/modules/testgen/targets/pna/target.cpp
index d355b29f9e3..b430041db1c 100644
--- a/backends/p4tools/modules/testgen/targets/pna/target.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/target.cpp
@@ -57,15 +57,12 @@ const PnaDpdkProgramInfo *PnaDpdkTestgenTarget::initProgramImpl(
     return new PnaDpdkProgramInfo(program, programmableBlocks);
 }
 
-PnaTestBackend *PnaDpdkTestgenTarget::getTestBackendImpl(const ProgramInfo &programInfo,
-                                                         SymbolicExecutor &symbex,
-                                                         const std::filesystem::path &testPath,
-                                                         std::optional<uint32_t> seed) const {
-    return new PnaTestBackend(programInfo, symbex, testPath, seed);
+PnaTestBackend *PnaDpdkTestgenTarget::getTestBackendImpl(
+    const ProgramInfo &programInfo, SymbolicExecutor &symbex,
+    const std::filesystem::path &testPath) const {
+    return new PnaTestBackend(programInfo, symbex, testPath);
 }
 
-int PnaDpdkTestgenTarget::getPortNumWidthBitsImpl() const { return 9; }
-
 PnaDpdkCmdStepper *PnaDpdkTestgenTarget::getCmdStepperImpl(ExecutionState &state,
                                                            AbstractSolver &solver,
                                                            const ProgramInfo &programInfo) const {
diff --git a/backends/p4tools/modules/testgen/targets/pna/target.h b/backends/p4tools/modules/testgen/targets/pna/target.h
index da2feb78073..01885cbf8b5 100644
--- a/backends/p4tools/modules/testgen/targets/pna/target.h
+++ b/backends/p4tools/modules/testgen/targets/pna/target.h
@@ -29,11 +29,8 @@ class PnaDpdkTestgenTarget : public TestgenTarget {
     const PnaDpdkProgramInfo *initProgramImpl(
         const IR::P4Program *program, const IR::Declaration_Instance *mainDecl) const override;
 
-    [[nodiscard]] int getPortNumWidthBitsImpl() const override;
-
     PnaTestBackend *getTestBackendImpl(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                       const std::filesystem::path &testPath,
-                                       std::optional<uint32_t> seed) const override;
+                                       const std::filesystem::path &testPath) const override;
 
     PnaDpdkCmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                          const ProgramInfo &programInfo) const override;
diff --git a/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp b/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp
index 362dc743faa..fbcf3ef22ab 100644
--- a/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp
+++ b/backends/p4tools/modules/testgen/targets/pna/test_backend.cpp
@@ -32,7 +32,7 @@ namespace P4Tools::P4Testgen::Pna {
 const std::set<std::string> PnaTestBackend::SUPPORTED_BACKENDS = {"METADATA"};
 
 PnaTestBackend::PnaTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                               const std::filesystem::path &testPath, std::optional<uint32_t> seed)
+                               const std::filesystem::path &testPath)
     : TestBackEnd(programInfo, symbex) {
     cstring testBackendString = TestgenOptions::get().testBackend;
     if (testBackendString.isNullOrEmpty()) {
@@ -43,7 +43,7 @@ PnaTestBackend::PnaTestBackend(const ProgramInfo &programInfo, SymbolicExecutor
     }
 
     if (testBackendString == "METADATA") {
-        testWriter = new Metadata(testPath.c_str(), seed);
+        testWriter = new Metadata(testPath.c_str(), TestgenOptions::get().seed);
     } else {
         P4C_UNIMPLEMENTED(
             "Test back end %1% not implemented for this target. Supported back ends are %2%.",
diff --git a/backends/p4tools/modules/testgen/targets/pna/test_backend.h b/backends/p4tools/modules/testgen/targets/pna/test_backend.h
index c7fbef017ca..e3c9bdad975 100644
--- a/backends/p4tools/modules/testgen/targets/pna/test_backend.h
+++ b/backends/p4tools/modules/testgen/targets/pna/test_backend.h
@@ -28,7 +28,7 @@ class PnaTestBackend : public TestBackEnd {
 
  public:
     explicit PnaTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                            const std::filesystem::path &testPath, std::optional<uint32_t> seed);
+                            const std::filesystem::path &testPath);
 
     TestBackEnd::TestInfo produceTestInfo(
         const ExecutionState *executionState, const Model *completedModel,
diff --git a/backends/p4tools/modules/testgen/testgen.cpp b/backends/p4tools/modules/testgen/testgen.cpp
index 9cf671c16c6..ad354fd6ecd 100644
--- a/backends/p4tools/modules/testgen/testgen.cpp
+++ b/backends/p4tools/modules/testgen/testgen.cpp
@@ -55,31 +55,8 @@ SymbolicExecutor *pickExecutionEngine(const TestgenOptions &testgenOptions,
     return new DepthFirstSearch(solver, *programInfo);
 }
 
-int Testgen::mainImpl(const IR::P4Program *program) {
-    // Register all available testgen targets.
-    // These are discovered by CMAKE, which fills out the register.h.in file.
-    registerTestgenTargets();
-
-    const auto *programInfo = TestgenTarget::initProgram(program);
-    if (programInfo == nullptr) {
-        ::error("Program not supported by target device and architecture.");
-        return EXIT_FAILURE;
-    }
-    if (::errorCount() > 0) {
-        ::error("Testgen: Encountered errors during preprocessing. Exiting");
-        return EXIT_FAILURE;
-    }
-
-    // Print basic information for each test.
-    enableInformationLogging();
-
-    // Get the options and the seed.
-    const auto &testgenOptions = TestgenOptions::get();
-    auto seed = Utils::getCurrentSeed();
-    if (seed) {
-        printFeature("test_info", 4, "============ Program seed %1% =============\n", *seed);
-    }
-
+int generateAbstractTests(const TestgenOptions &testgenOptions, const ProgramInfo *programInfo,
+                          SymbolicExecutor &symbex) {
     // Get the filename of the input file and remove the extension
     // This assumes that inputFile is not null.
     auto const inputFile = P4CContext::get().options().file;
@@ -91,13 +68,9 @@ int Testgen::mainImpl(const IR::P4Program *program) {
         std::filesystem::create_directories(testDir);
         testPath = testDir / testPath;
     }
-    // Need to declare the solver here to ensure its lifetime.
-    Z3Solver solver;
-    auto *symExec = pickExecutionEngine(testgenOptions, programInfo, solver);
-
-    // Define how to handle the final state for each test. This is target defined.
-    auto *testBackend = TestgenTarget::getTestBackend(*programInfo, *symExec, testPath, seed);
     // Each test back end has a different run function.
+    auto *testBackend = TestgenTarget::getTestBackend(*programInfo, symbex, testPath);
+    // Define how to handle the final state for each test. This is target defined.
     // We delegate execution to the symbolic executor.
     auto callBack = [testBackend](auto &&finalState) {
         return testBackend->run(std::forward<decltype(finalState)>(finalState));
@@ -105,14 +78,14 @@ int Testgen::mainImpl(const IR::P4Program *program) {
 
     try {
         // Run the symbolic executor with given exploration strategy.
-        symExec->run(callBack);
+        symbex.run(callBack);
     } catch (...) {
         if (testgenOptions.trackBranches) {
             // Print list of the selected branches and store all information into
             // dumpFolder/selectedBranches.txt file.
             // This printed list could be used for repeat this bug in arguments of --input-branches
             // command line. For example, --input-branches "1,1".
-            symExec->printCurrentTraceAndBranches(std::cerr);
+            symbex.printCurrentTraceAndBranches(std::cerr);
         }
         throw;
     }
@@ -125,8 +98,39 @@ int Testgen::mainImpl(const IR::P4Program *program) {
             "Unable to generate tests with given inputs. Double-check provided options and "
             "parameters.\n");
     }
-
     return ::errorCount() == 0 ? EXIT_SUCCESS : EXIT_FAILURE;
 }
 
+int Testgen::mainImpl(const IR::P4Program *program) {
+    // Register all available testgen targets.
+    // These are discovered by CMAKE, which fills out the register.h.in file.
+    registerTestgenTargets();
+
+    const auto *programInfo = TestgenTarget::initProgram(program);
+    if (programInfo == nullptr) {
+        ::error("Program not supported by target device and architecture.");
+        return EXIT_FAILURE;
+    }
+    if (::errorCount() > 0) {
+        ::error("Testgen: Encountered errors during preprocessing. Exiting");
+        return EXIT_FAILURE;
+    }
+
+    // Print basic information for each test.
+    enableInformationLogging();
+
+    // Get the options and the seed.
+    const auto &testgenOptions = TestgenOptions::get();
+    auto seed = Utils::getCurrentSeed();
+    if (seed) {
+        printFeature("test_info", 4, "============ Program seed %1% =============\n", *seed);
+    }
+
+    // Need to declare the solver here to ensure its lifetime.
+    Z3Solver solver;
+    auto *symbex = pickExecutionEngine(testgenOptions, programInfo, solver);
+
+    return generateAbstractTests(testgenOptions, programInfo, *symbex);
+}
+
 }  // namespace P4Tools::P4Testgen