diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel
index df9137da..dfef495f 100644
--- a/p4_symbolic/symbolic/BUILD.bazel
+++ b/p4_symbolic/symbolic/BUILD.bazel
@@ -75,6 +75,7 @@ cc_library(
         "@com_google_absl//absl/container:btree",
         "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/numeric:bits",
+        "@com_google_absl//absl/numeric:int128",
         "@com_google_absl//absl/status",
         "@com_google_absl//absl/status:statusor",
         "@com_google_absl//absl/strings",
diff --git a/p4_symbolic/symbolic/context.h b/p4_symbolic/symbolic/context.h
index c8083006..ba1af0dc 100644
--- a/p4_symbolic/symbolic/context.h
+++ b/p4_symbolic/symbolic/context.h
@@ -103,6 +103,7 @@ struct ConcreteContext {
   ConcretePerPacketState ingress_headers;
   ConcretePerPacketState parsed_headers;
   ConcretePerPacketState egress_headers;
+  TableEntries table_entries;
   ConcreteTrace trace;  // Expected trace in the program.
 
   std::string to_string(bool verbose = false) const;
diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc
index 4285cbbd..b79a615a 100644
--- a/p4_symbolic/symbolic/symbolic.cc
+++ b/p4_symbolic/symbolic/symbolic.cc
@@ -28,7 +28,6 @@
 #include "absl/status/statusor.h"
 #include "absl/strings/string_view.h"
 #include "absl/types/optional.h"
-#include "glog/logging.h"
 #include "gutil/status.h"
 #include "p4/v1/p4runtime.pb.h"
 #include "p4_pdpi/internal/ordered_map.h"
@@ -224,19 +223,22 @@ absl::StatusOr<std::optional<ConcreteContext>> Solve(SolverState &state) {
   z3::check_result check_result = state.solver->check();
   switch (check_result) {
     case z3::unsat:
-    case z3::unknown:
+    case z3::unknown: {
       return absl::nullopt;
+    }
 
-    case z3::sat:
-      z3::model packet_model = state.solver->get_model();
+    case z3::sat: {
+      z3::model model = state.solver->get_model();
       ASSIGN_OR_RETURN(ConcreteContext result,
-                       util::ExtractFromModel(state.context, packet_model,
-                                              state.translator));
+                       util::ExtractFromModel(model, state));
       return result;
+    }
+
+    default: {
+      return gutil::InternalErrorBuilder()
+             << "Invalid Z3 check() result: " << check_result;
+    }
   }
-  LOG(DFATAL) << "invalid Z3 check() result: "
-              << static_cast<int>(check_result);
-  return absl::nullopt;
 }
 
 absl::StatusOr<std::optional<ConcreteContext>> Solve(
diff --git a/p4_symbolic/symbolic/table_entry.cc b/p4_symbolic/symbolic/table_entry.cc
index 08c4494f..3612268d 100644
--- a/p4_symbolic/symbolic/table_entry.cc
+++ b/p4_symbolic/symbolic/table_entry.cc
@@ -16,17 +16,21 @@
 
 #include <algorithm>
 #include <cstddef>
+#include <cstdint>
 #include <optional>
 #include <string>
 #include <utility>
 
 #include "absl/container/btree_map.h"
 #include "absl/container/flat_hash_map.h"
+#include "absl/numeric/bits.h"
+#include "absl/numeric/int128.h"
 #include "absl/status/status.h"
 #include "absl/status/statusor.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/string_view.h"
+#include "glog/logging.h"
 #include "gutil/collections.h"
 #include "gutil/status.h"
 #include "p4/config/v1/p4info.pb.h"
@@ -36,6 +40,7 @@
 #include "p4_symbolic/symbolic/operators.h"
 #include "p4_symbolic/symbolic/util.h"
 #include "p4_symbolic/symbolic/values.h"
+#include "p4_symbolic/z3_util.h"
 #include "z3++.h"
 
 namespace p4_symbolic::symbolic {
@@ -44,13 +49,56 @@ using MatchType = p4::config::v1::MatchField::MatchType;
 
 namespace {
 
-// A static mapping between the PI match type to the type string.
-const absl::flat_hash_map<MatchType, std::string> match_type_to_str = {
-    {MatchType::MatchField_MatchType_EXACT, "exact"},
-    {MatchType::MatchField_MatchType_LPM, "lpm"},
-    {MatchType::MatchField_MatchType_TERNARY, "ternary"},
-    {MatchType::MatchField_MatchType_OPTIONAL, "optional"},
-};
+// Evaluates and returns the PDPI IR value for the `bv_expr` of a match field.
+absl::StatusOr<pdpi::IrValue> EvalZ3BitvectorToIrValue(
+    const z3::expr &bv_expr, const z3::model &model,
+    const std::optional<std::string> &field_name, const std::string &type_name,
+    const pdpi::Format &format, const values::P4RuntimeTranslator &translator) {
+  int bitwidth = bv_expr.get_sort().bv_size();
+  const std::string value =
+      model.eval(bv_expr, /*model_completion=*/true).to_string();
+  return values::TranslateZ3ValueStringToIrValue(value, bitwidth, field_name,
+                                                 type_name, translator, format);
+}
+
+// Evaluates the given bit-vector and converts it to prefix length. Returns an
+// error if the evaluated value is not a valid prefix-length mask.
+absl::StatusOr<unsigned int> EvalZ3BitvectorToPrefixLength(
+    const z3::expr &bv_expr, const z3::model &model) {
+  // Check if the size of the bit-vector is within 128 bits.
+  size_t bitwidth = bv_expr.get_sort().bv_size();
+  if (bitwidth > 128) {
+    return gutil::UnimplementedErrorBuilder()
+           << "Only values representable with 128-bit unsigned integers are "
+              "currently supported for prefix lengths. Found bit-width: "
+           << bitwidth;
+  }
+
+  ASSIGN_OR_RETURN(absl::uint128 int_value,
+                   EvalZ3BitvectorToUInt128(bv_expr, model));
+
+  // Note that (uint128(1) << 128) != 0. Here we handle the corner case
+  // separately.
+  absl::uint128 mask;
+  if (bitwidth == 128) {
+    mask = absl::Uint128Max();
+  } else {
+    mask = (absl::uint128(1) << bitwidth) - 1;
+  }
+
+  // Check if `int_value` is of the form 1*0*.
+  if (((~int_value) & (~int_value + 1) & mask) != 0) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Bit-vector value '" << int_value
+           << "' is not a valid prefix length.";
+  }
+
+  absl::uint128 suffix = ~int_value & mask;
+  uint64_t low64 = absl::Uint128Low64(suffix);
+  uint64_t high64 = absl::Uint128High64(suffix);
+  int suffix_length = absl::bit_width(low64) + absl::bit_width(high64);
+  return bitwidth - suffix_length;
+}
 
 // Translates the given `value` read from the `match` of an entry in the given
 // `table` into a Z3 expression.
@@ -356,6 +404,14 @@ const pdpi::IrTableEntry &TableEntry::GetPdpiIrTableEntry() const {
 absl::StatusOr<SymbolicMatchInfo> TableEntry::GetSymbolicMatchInfo(
     absl::string_view match_name, const ir::Table &table,
     const ir::P4Program &program) const {
+  // A static mapping between the PI match type to the type string.
+  static const absl::flat_hash_map<MatchType, std::string> match_type_to_str = {
+      {MatchType::MatchField_MatchType_EXACT, "exact"},
+      {MatchType::MatchField_MatchType_LPM, "lpm"},
+      {MatchType::MatchField_MatchType_TERNARY, "ternary"},
+      {MatchType::MatchField_MatchType_OPTIONAL, "optional"},
+  };
+
   // Check if the match exists in the table definition.
   if (!table.table_definition().match_fields_by_name().contains(match_name)) {
     return gutil::NotFoundErrorBuilder()
@@ -741,4 +797,181 @@ absl::Status InitializeSymbolicActions(
   return absl::OkStatus();
 }
 
+// Returns a concrete table entry extracted from the given `symbolic_entry`
+// based on the given `model` and `translator`.
+absl::StatusOr<TableEntry> ExtractConcreteEntryFromModel(
+    const TableEntry &entry, const z3::model &model,
+    const ir::P4Program &program, const values::P4RuntimeTranslator &translator,
+    z3::context &z3_context) {
+  if (entry.IsConcrete()) {
+    // Return the input entry if it is already concrete.
+    return entry;
+  } else if (!entry.IsSymbolic()) {
+    // Check if the input entry is symbolic.
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Attempting to extract from an entry that is neither concrete "
+              "nor symbolic.";
+  }
+
+  // Check if the table specified by the symbolic entry exists.
+  const std::string &table_name = entry.GetTableName();
+  auto it = program.tables().find(table_name);
+  if (it == program.tables().end()) {
+    return gutil::NotFoundErrorBuilder()
+           << "Table '" << table_name << "' not found.";
+  }
+  const ir::Table &table = it->second;
+
+  // Get the symbolic sketch.
+  const pdpi::IrTableEntry &sketch = entry.GetPdpiIrTableEntry();
+
+  // Construct the concrete IR entry.
+  // By assigning the symbolic sketch to the concrete IR entry, we keep things
+  // that are not under the control of P4-Symbolic intact (e.g., table_name,
+  // priority, meter_config, counter_data, meter_counter_data,
+  // controller_metadata).
+  ir::TableEntry ir_entry;
+  pdpi::IrTableEntry &pdpi_ir_entry = *ir_entry.mutable_concrete_entry();
+  pdpi_ir_entry = sketch;
+  pdpi_ir_entry.clear_matches();
+  pdpi_ir_entry.clear_action();
+  pdpi_ir_entry.clear_action_set();
+
+  // Set matches.
+  for (const pdpi::IrMatch &symbolic_match : sketch.matches()) {
+    bool wildcard = false;
+    pdpi::IrMatch concrete_match;
+
+    // Set match name.
+    const std::string &match_name = symbolic_match.name();
+    concrete_match.set_name(match_name);
+
+    // Evaluate and set match values.
+    ASSIGN_OR_RETURN(
+        SymbolicMatchVariables match_variables,
+        entry.GetMatchValues(match_name, table, program, z3_context));
+    ASSIGN_OR_RETURN(std::string field_name,
+                     util::GetFieldNameFromMatch(match_name, table));
+    ASSIGN_OR_RETURN(pdpi::IrMatchFieldDefinition match_definition,
+                     util::GetMatchDefinition(match_name, table));
+    const std::string &type_name =
+        match_definition.match_field().type_name().name();
+    ASSIGN_OR_RETURN(pdpi::IrValue value,
+                     EvalZ3BitvectorToIrValue(
+                         match_variables.value, model, field_name, type_name,
+                         match_definition.format(), translator));
+
+    switch (match_variables.match_type) {
+      case MatchType::MatchField_MatchType_EXACT: {
+        *concrete_match.mutable_exact() = std::move(value);
+        break;
+      }
+      case MatchType::MatchField_MatchType_LPM: {
+        *concrete_match.mutable_lpm()->mutable_value() = std::move(value);
+        ASSIGN_OR_RETURN(int prefix_length, EvalZ3BitvectorToPrefixLength(
+                                                match_variables.mask, model));
+        concrete_match.mutable_lpm()->set_prefix_length(prefix_length);
+        if (prefix_length == 0) wildcard = true;
+        break;
+      }
+      case MatchType::MatchField_MatchType_TERNARY: {
+        ASSIGN_OR_RETURN(pdpi::IrValue mask,
+                         EvalZ3BitvectorToIrValue(
+                             match_variables.mask, model, field_name, type_name,
+                             match_definition.format(), translator));
+        *concrete_match.mutable_ternary()->mutable_value() = std::move(value);
+        *concrete_match.mutable_ternary()->mutable_mask() = std::move(mask);
+        ASSIGN_OR_RETURN(absl::uint128 mask_value,
+                         EvalZ3BitvectorToUInt128(match_variables.mask, model));
+        if (mask_value == 0) wildcard = true;
+        break;
+      }
+      case MatchType::MatchField_MatchType_OPTIONAL: {
+        *concrete_match.mutable_optional()->mutable_value() = std::move(value);
+        ASSIGN_OR_RETURN(int prefix_length, EvalZ3BitvectorToPrefixLength(
+                                                match_variables.mask, model));
+        const size_t bitwidth = match_variables.value.get_sort().bv_size();
+        if (prefix_length != 0 && prefix_length != bitwidth) {
+          return gutil::InternalErrorBuilder()
+                 << "The mask must be either all-1s or all-0s for optional "
+                    "matches. Found prefix length "
+                 << prefix_length;
+        }
+        if (prefix_length == 0) wildcard = true;
+        break;
+      }
+      default: {
+        return gutil::InvalidArgumentErrorBuilder()
+               << "Invalid match type, must be one of [exact, lpm, ternary, "
+                  "optional]. Found: "
+               << match_variables.match_type;
+      }
+    }
+
+    if (!wildcard) {
+      *pdpi_ir_entry.add_matches() = std::move(concrete_match);
+    }
+  }
+
+  // Check if the table is a WCMP table.
+  if (table.table_definition().has_action_profile_id()) {
+    return gutil::UnimplementedErrorBuilder()
+           << "Table entries with symbolic action sets are not supported "
+              "at the moment.";
+  }
+
+  // Set the invoked action of the entry.
+  std::optional<std::string> previous_action_applied;
+
+  for (const auto &action_ref : table.table_definition().entry_actions()) {
+    const std::string &action_name = action_ref.action().preamble().name();
+    ASSIGN_OR_RETURN(z3::expr action_invocation,
+                     entry.GetActionInvocation(action_name, table, z3_context));
+    ASSIGN_OR_RETURN(bool action_applied, EvalZ3Bool(action_invocation, model));
+    if (!action_applied) continue;
+
+    // Make sure only one action is applied for each entry.
+    if (previous_action_applied) {
+      return gutil::InternalErrorBuilder()
+             << "More than one action is applied for an entry in a non-WCMP "
+                "table: '"
+             << *previous_action_applied << "' and '" << action_name << "'";
+    }
+    previous_action_applied = action_name;
+
+    // Check and get the action in P4-Symbolic IR.
+    auto it = program.actions().find(action_name);
+    if (it == program.actions().end()) {
+      return gutil::NotFoundErrorBuilder()
+             << "Action '" << action_name << "' not found.";
+    }
+    const ir::Action &action = it->second;
+
+    // Set action name.
+    pdpi_ir_entry.mutable_action()->set_name(action_name);
+
+    // Set action parameters.
+    for (const auto &[param_name, param_definition] :
+         Ordered(action.action_definition().params_by_name())) {
+      // Set action parameter name.
+      pdpi::IrActionInvocation::IrActionParam &ir_param =
+          *pdpi_ir_entry.mutable_action()->add_params();
+      ir_param.set_name(param_name);
+      // Set action parameter value.
+      ASSIGN_OR_RETURN(
+          z3::expr param,
+          entry.GetActionParameter(param_name, action, table, z3_context));
+      ASSIGN_OR_RETURN(
+          pdpi::IrValue value,
+          EvalZ3BitvectorToIrValue(param, model, /*field_name=*/std::nullopt,
+                                   param_definition.param().type_name().name(),
+                                   param_definition.format(), translator));
+      *ir_param.mutable_value() = std::move(value);
+    }
+  }
+
+  // Build and return the concrete table entry.
+  return TableEntry(entry.GetIndex(), ir_entry);
+}
+
 }  // namespace p4_symbolic::symbolic
diff --git a/p4_symbolic/symbolic/table_entry.h b/p4_symbolic/symbolic/table_entry.h
index c90af2e4..90ad8ef5 100644
--- a/p4_symbolic/symbolic/table_entry.h
+++ b/p4_symbolic/symbolic/table_entry.h
@@ -163,6 +163,13 @@ absl::Status InitializeSymbolicActions(const TableEntry &entry,
                                        z3::solver &solver,
                                        values::P4RuntimeTranslator &translator);
 
+// Returns a concrete table entry extracted from the given `symbolic_entry`
+// based on the given `model` and `translator`.
+absl::StatusOr<TableEntry> ExtractConcreteEntryFromModel(
+    const TableEntry &symbolic_entry, const z3::model &model,
+    const ir::P4Program &program, const values::P4RuntimeTranslator &translator,
+    z3::context &z3_context);
+
 }  // namespace p4_symbolic::symbolic
 
 #endif  // PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_
diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc
index 702929eb..11f98091 100644
--- a/p4_symbolic/symbolic/util.cc
+++ b/p4_symbolic/symbolic/util.cc
@@ -31,10 +31,12 @@
 #include "glog/logging.h"
 #include "gutil/status.h"
 #include "p4_pdpi/internal/ordered_map.h"
+#include "p4_pdpi/ir.pb.h"
 #include "p4_symbolic/ir/ir.pb.h"
 #include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/operators.h"
 #include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/table_entry.h"
 #include "p4_symbolic/symbolic/values.h"
 #include "p4_symbolic/z3_util.h"
 #include "z3++.h"
@@ -120,45 +122,64 @@ SymbolicTableMatch DefaultTableMatch(z3::context &z3_context) {
   };
 }
 
-absl::StatusOr<ConcreteContext> ExtractFromModel(
-    const SymbolicContext &context, z3::model model,
-    const values::P4RuntimeTranslator &translator) {
+absl::StatusOr<ConcreteContext> ExtractFromModel(const z3::model &model,
+                                                 const SolverState &state) {
   // Extract ports.
-  std::string ingress_port = model.eval(context.ingress_port, true).to_string();
-  std::string egress_port = model.eval(context.egress_port, true).to_string();
+  std::string ingress_port =
+      model.eval(state.context.ingress_port, true).to_string();
+  std::string egress_port =
+      model.eval(state.context.egress_port, true).to_string();
 
   // Extract the ingress, parsed, and egress headers.
   ConcretePerPacketState ingress_headers;
-  for (const auto &[name, expr] : context.ingress_headers) {
+  for (const auto &[name, expr] : state.context.ingress_headers) {
     ASSIGN_OR_RETURN(auto translated_value,
                      values::TranslateZ3ValueStringToP4RT(
                          model.eval(expr, true).to_string(), name,
-                         /*type_name=*/std::nullopt, translator));
+                         /*type_name=*/std::nullopt, state.translator));
     ingress_headers[name] = std::move(translated_value.first);
   }
   ConcretePerPacketState parsed_headers;
-  for (const auto &[name, expr] : context.parsed_headers) {
+  for (const auto &[name, expr] : state.context.parsed_headers) {
     ASSIGN_OR_RETURN(auto translated_value,
                      values::TranslateZ3ValueStringToP4RT(
                          model.eval(expr, true).to_string(), name,
-                         /*type_name=*/std::nullopt, translator));
+                         /*type_name=*/std::nullopt, state.translator));
     parsed_headers[name] = std::move(translated_value.first);
   }
   ConcretePerPacketState egress_headers;
-  for (const auto &[name, expr] : context.egress_headers) {
+  for (const auto &[name, expr] : state.context.egress_headers) {
     ASSIGN_OR_RETURN(auto translated_value,
                      values::TranslateZ3ValueStringToP4RT(
                          model.eval(expr, true).to_string(), name,
-                         /*type_name=*/std::nullopt, translator));
+                         /*type_name=*/std::nullopt, state.translator));
     egress_headers[name] = std::move(translated_value.first);
   }
 
+  // Extract the table entries.
+  TableEntries concrete_entries;
+  for (const auto &[table_name, entries_per_table] :
+       state.context.table_entries) {
+    for (const TableEntry &entry : entries_per_table) {
+      if (entry.IsSymbolic()) {
+        ASSIGN_OR_RETURN(TableEntry concrete_entry,
+                         ExtractConcreteEntryFromModel(
+                             entry, model, state.program, state.translator,
+                             *state.context.z3_context));
+        concrete_entries[table_name].push_back(std::move(concrete_entry));
+      } else {
+        concrete_entries[table_name].push_back(entry);
+      }
+    }
+  }
+
   // Extract the trace (matches on every table).
-  ASSIGN_OR_RETURN(bool dropped, EvalZ3Bool(context.trace.dropped, model));
+  ASSIGN_OR_RETURN(bool dropped,
+                   EvalZ3Bool(state.context.trace.dropped, model));
   ASSIGN_OR_RETURN(bool got_cloned,
-                   EvalZ3Bool(context.trace.got_cloned, model));
+                   EvalZ3Bool(state.context.trace.got_cloned, model));
   absl::btree_map<std::string, ConcreteTableMatch> matched_entries;
-  for (const auto &[table, match] : context.trace.matched_entries) {
+  for (const auto &[table, match] : state.context.trace.matched_entries) {
     ASSIGN_OR_RETURN(bool matched, EvalZ3Bool(match.matched, model));
     ASSIGN_OR_RETURN(int entry_index, EvalZ3Int(match.entry_index, model));
     matched_entries[table] = ConcreteTableMatch{
@@ -168,14 +189,15 @@ absl::StatusOr<ConcreteContext> ExtractFromModel(
   }
 
   return ConcreteContext{
-      .ingress_port = ingress_port,
-      .egress_port = egress_port,
-      .ingress_headers = ingress_headers,
-      .parsed_headers = parsed_headers,
-      .egress_headers = egress_headers,
+      .ingress_port = std::move(ingress_port),
+      .egress_port = std::move(egress_port),
+      .ingress_headers = std::move(ingress_headers),
+      .parsed_headers = std::move(parsed_headers),
+      .egress_headers = std::move(egress_headers),
+      .table_entries = std::move(concrete_entries),
       .trace =
           ConcreteTrace{
-              .matched_entries = matched_entries,
+              .matched_entries = std::move(matched_entries),
               .dropped = dropped,
               .got_cloned = got_cloned,
           },
@@ -277,6 +299,40 @@ std::string GetHeaderValidityFieldName(absl::string_view header_name) {
   return absl::StrCat(header_name, ".", kValidPseudoField);
 }
 
+// Returns the header field name of the match with the given `match_name` in the
+// given `table`.
+absl::StatusOr<std::string> GetFieldNameFromMatch(absl::string_view match_name,
+                                                  const ir::Table &table) {
+  const auto &match_name_to_field =
+      table.table_implementation().match_name_to_field();
+  auto it = match_name_to_field.find(match_name);
+  if (it == match_name_to_field.end()) {
+    return gutil::NotFoundErrorBuilder()
+           << "Match '" << match_name
+           << "' not found in the implementation of table '"
+           << table.table_definition().preamble().name() << "'";
+  }
+  const ir::FieldValue &matched_field = it->second;
+  return absl::StrFormat("%s.%s", matched_field.header_name(),
+                         matched_field.field_name());
+}
+
+// Returns the match field definition with the given `match_name` in the given
+// `table`.
+absl::StatusOr<pdpi::IrMatchFieldDefinition> GetMatchDefinition(
+    absl::string_view match_name, const ir::Table &table) {
+  const auto &match_fields_by_name =
+      table.table_definition().match_fields_by_name();
+  auto it = match_fields_by_name.find(match_name);
+  if (it == match_fields_by_name.end()) {
+    return gutil::NotFoundErrorBuilder()
+           << "Match '" << match_name
+           << "' not found in the definition of table '"
+           << table.table_definition().preamble().name() << "'";
+  }
+  return it->second;
+}
+
 }  // namespace util
 }  // namespace symbolic
 }  // namespace p4_symbolic
diff --git a/p4_symbolic/symbolic/util.h b/p4_symbolic/symbolic/util.h
index fdf42cbb..02dc5bc2 100644
--- a/p4_symbolic/symbolic/util.h
+++ b/p4_symbolic/symbolic/util.h
@@ -23,9 +23,10 @@
 #include "absl/status/statusor.h"
 #include "absl/strings/string_view.h"
 #include "google/protobuf/map.h"
+#include "p4_pdpi/ir.pb.h"
 #include "p4_symbolic/ir/ir.pb.h"
 #include "p4_symbolic/symbolic/context.h"
-#include "p4_symbolic/symbolic/values.h"
+#include "p4_symbolic/symbolic/symbolic.h"
 #include "z3++.h"
 
 namespace p4_symbolic {
@@ -45,9 +46,8 @@ SymbolicTableMatch DefaultTableMatch(z3::context &z3_context);
 
 // Extract a concrete context by evaluating every component's corresponding
 // expression in the model.
-absl::StatusOr<ConcreteContext> ExtractFromModel(
-    const SymbolicContext &context, z3::model model,
-    const values::P4RuntimeTranslator &translator);
+absl::StatusOr<ConcreteContext> ExtractFromModel(const z3::model &model,
+                                                 const SolverState &state);
 
 // Merges two maps of table matches into a single map. A field in the returned
 // map has the value of `true_matches` if the condition is true, and the
@@ -77,6 +77,16 @@ absl::StatusOr<int> GetFieldBitwidth(absl::string_view header_name,
 // Returns the full valid field name of the given header.
 std::string GetHeaderValidityFieldName(absl::string_view header_name);
 
+// Returns the header field name of the match with the given `match_name` in the
+// given `table`.
+absl::StatusOr<std::string> GetFieldNameFromMatch(absl::string_view match_name,
+                                                  const ir::Table &table);
+
+// Returns the match field definition with the given `match_name` in the given
+// `table`.
+absl::StatusOr<pdpi::IrMatchFieldDefinition> GetMatchDefinition(
+    absl::string_view match_name, const ir::Table &table);
+
 }  // namespace util
 }  // namespace symbolic
 }  // namespace p4_symbolic
diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc
index 35d6c566..de6c3388 100644
--- a/p4_symbolic/symbolic/values.cc
+++ b/p4_symbolic/symbolic/values.cc
@@ -120,7 +120,7 @@ absl::StatusOr<z3::expr> FormatP4RTValue(
 }
 
 absl::StatusOr<std::pair<std::string, bool>> TranslateZ3ValueStringToP4RT(
-    const std::string &value, const std::string &field_name,
+    const std::string &value, const std::optional<std::string> &field_name,
     const std::optional<std::string> &type_name,
     const P4RuntimeTranslator &translator, std::optional<pdpi::Format> format) {
   // Use `type_name` as the default field type.
@@ -129,9 +129,11 @@ absl::StatusOr<std::pair<std::string, bool>> TranslateZ3ValueStringToP4RT(
 
   // If `field_name` is found in the mapping to P4Runtime translated field
   // types, use the field type based on the `field_name`.
-  if (auto it = translator.fields_p4runtime_type.find(field_name);
-      it != translator.fields_p4runtime_type.end()) {
-    field_type = it->second;
+  if (field_name.has_value() && !field_name->empty()) {
+    if (auto it = translator.fields_p4runtime_type.find(*field_name);
+        it != translator.fields_p4runtime_type.end()) {
+      field_type = it->second;
+    }
   }
 
   // Get the allocator based on the field type.
@@ -158,15 +160,16 @@ absl::StatusOr<std::pair<std::string, bool>> TranslateZ3ValueStringToP4RT(
   uint64_t int_value = Z3ValueStringToInt(value);
   ASSIGN_OR_RETURN(std::string p4rt_value, allocator.IdToString(int_value),
                    _.SetPrepend()
-                       << "Failed to translate dataplane value of field '"
-                       << field_name << "' to P4Runtime representation: ");
+                       << "Failed to translate dataplane value of type '"
+                       << field_type << "' to P4Runtime representation: ");
   return std::make_pair(p4rt_value, true);
 }
 
 absl::StatusOr<pdpi::IrValue> TranslateZ3ValueStringToIrValue(
-    const std::string &value, int bitwidth, const std::string &field_name,
-    const std::string &type_name, const P4RuntimeTranslator &translator,
-    const pdpi::Format &format) {
+    const std::string &value, int bitwidth,
+    const std::optional<std::string> &field_name,
+    const std::optional<std::string> &type_name,
+    const P4RuntimeTranslator &translator, const pdpi::Format &format) {
   ASSIGN_OR_RETURN(auto translated_value,
                    values::TranslateZ3ValueStringToP4RT(
                        value, field_name, type_name, translator, format));
diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h
index b6f58bb2..4e66d04e 100644
--- a/p4_symbolic/symbolic/values.h
+++ b/p4_symbolic/symbolic/values.h
@@ -143,7 +143,7 @@ absl::StatusOr<z3::expr> FormatP4RTValue(
 // for the actual translation. Otherwise (e.g., for action parameters or entry
 // field matches that provide a type name), `type_name` is used instead.
 absl::StatusOr<std::pair<std::string, bool>> TranslateZ3ValueStringToP4RT(
-    const std::string &value, const std::string &field_name,
+    const std::string &value, const std::optional<std::string> &field_name,
     const std::optional<std::string> &type_name,
     const P4RuntimeTranslator &translator,
     std::optional<pdpi::Format> format = std::nullopt);
@@ -158,9 +158,10 @@ absl::StatusOr<std::pair<std::string, bool>> TranslateZ3ValueStringToP4RT(
 // for the actual translation. Otherwise (e.g., for action parameters or entry
 // field matches that provide a type name), `type_name` is used instead.
 absl::StatusOr<pdpi::IrValue> TranslateZ3ValueStringToIrValue(
-    const std::string &value, int bitwidth, const std::string &field_name,
-    const std::string &type_name, const P4RuntimeTranslator &translator,
-    const pdpi::Format &format);
+    const std::string &value, int bitwidth,
+    const std::optional<std::string> &field_name,
+    const std::optional<std::string> &type_name,
+    const P4RuntimeTranslator &translator, const pdpi::Format &format);
 
 } // namespace values
 } // namespace symbolic
diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel
index 455b8405..725c79f4 100644
--- a/p4_symbolic/tests/BUILD.bazel
+++ b/p4_symbolic/tests/BUILD.bazel
@@ -45,6 +45,7 @@ cc_test(
         "//gutil:status_matchers",
         "//gutil:test_artifact_writer",
         "//p4_symbolic:test_util",
+        "//p4_symbolic:z3_util",
         "//p4_symbolic/ir",
         "//p4_symbolic/ir:ir_cc_proto",
         "//p4_symbolic/ir:parser",
@@ -53,6 +54,7 @@ cc_test(
         "//p4_symbolic/symbolic",
         "@com_github_google_glog//:glog",
         "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
+        "@com_github_z3prover_z3//:api",
         "@com_google_absl//absl/strings",
         "@com_google_absl//absl/time",
         "@com_google_googletest//:gtest_main",
diff --git a/p4_symbolic/tests/symbolic_table_entries_test.cc b/p4_symbolic/tests/symbolic_table_entries_test.cc
index 43cdba15..7a4d9722 100644
--- a/p4_symbolic/tests/symbolic_table_entries_test.cc
+++ b/p4_symbolic/tests/symbolic_table_entries_test.cc
@@ -13,6 +13,7 @@
 // limitations under the License.
 
 #include <memory>
+#include <optional>
 #include <string>
 #include <utility>
 #include <vector>
@@ -32,10 +33,13 @@
 #include "p4_symbolic/ir/parser.h"
 #include "p4_symbolic/ir/table_entries.h"
 #include "p4_symbolic/sai/sai.h"
+#include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/symbolic.h"
 #include "p4_symbolic/symbolic/table_entry.h"
 #include "p4_symbolic/symbolic/values.h"
 #include "p4_symbolic/test_util.h"
+#include "p4_symbolic/z3_util.h"
+#include "z3++.h"
 
 namespace p4_symbolic {
 namespace {
@@ -111,17 +115,66 @@ TEST_F(SymbolicTableEntriesIPv4BasicTest, OneSymbolicEntryPerTable) {
     std::string banner =
         absl::StrCat("== ", table_name, " ",
                      std::string(80 - table_name.size() - 4, '='), "\n");
-    EXPECT_OK(artifact_writer_.AppendToTestArtifact("table_entries.textproto",
-                                                    banner));
+    EXPECT_OK(artifact_writer_.AppendToTestArtifact(
+        "input_table_entries.textproto", banner));
     for (const auto& entry : entries) {
       EXPECT_OK(artifact_writer_.AppendToTestArtifact(
-          "table_entries.textproto", entry.GetP4SymbolicIrTableEntry()));
+          "input_table_entries.textproto", entry.GetP4SymbolicIrTableEntry()));
     }
   }
   EXPECT_OK(
       artifact_writer_.StoreTestArtifact("program.textproto", state->program));
   EXPECT_OK(artifact_writer_.StoreTestArtifact(
       "all_smt_formulae.txt", state->GetHeadersAndSolverConstraintsSMT()));
+
+  // Define criteria to hit the ipv4_lpm table and have the packet forwarded.
+  constexpr absl::string_view table_name = "MyIngress.ipv4_lpm";
+  ASSERT_OK_AND_ASSIGN(
+      z3::expr egress_spec_of_ingress_packet,
+      state->context.ingress_headers.Get("standard_metadata.egress_spec"));
+  ASSERT_TRUE(state->context.trace.matched_entries.contains(table_name));
+  const symbolic::SymbolicTableMatch& lpm_table =
+      state->context.trace.matched_entries.at(table_name);
+  symbolic::Assertion criteria =
+      [&egress_spec_of_ingress_packet,
+       &lpm_table](const symbolic::SymbolicContext& ctx) -> z3::expr {
+    // TODO: Remove this once cl/550894398 is submitted.
+    z3::expr ingress_constraint = (egress_spec_of_ingress_packet == 0);
+    return lpm_table.matched && !ctx.trace.dropped && ctx.egress_port == 3 &&
+           ingress_constraint;
+  };
+  EXPECT_OK(artifact_writer_.StoreTestArtifact(
+      "criteria.smt.txt", symbolic::DebugSMT(state, criteria)));
+
+  // Solve for a concrete solution given the criteria.
+  ASSERT_OK_AND_ASSIGN(std::optional<symbolic::ConcreteContext> solution,
+                       symbolic::Solve(*state, criteria));
+  ASSERT_TRUE(solution.has_value());
+
+  // Dump the concrete context.
+  EXPECT_OK(artifact_writer_.StoreTestArtifact(
+      "solution.txt", solution->to_string(/*verbose=*/true)));
+  // Dump the table entries.
+  for (const auto& [table_name, entries] : solution->table_entries) {
+    std::string banner =
+        absl::StrCat("== ", table_name, " ",
+                     std::string(80 - table_name.size() - 4, '='), "\n");
+    EXPECT_OK(artifact_writer_.AppendToTestArtifact(
+        "concrete_table_entries.textproto", banner));
+    for (const auto& entry : entries) {
+      EXPECT_OK(artifact_writer_.AppendToTestArtifact(
+          "concrete_table_entries.textproto",
+          entry.GetP4SymbolicIrTableEntry()));
+    }
+  }
+
+  // Check properties of the solution.
+  EXPECT_EQ(Z3ValueStringToInt(solution->egress_port), 3);
+  EXPECT_FALSE(solution->trace.dropped);
+  ASSERT_EQ(solution->trace.matched_entries.size(), 1);
+  ASSERT_TRUE(solution->trace.matched_entries.contains(table_name));
+  EXPECT_TRUE(solution->trace.matched_entries.at(table_name).matched);
+  EXPECT_EQ(solution->trace.matched_entries.at(table_name).entry_index, 0);
 }
 
 }  // namespace