diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel
index 2fb1ac2d..cd5432f8 100644
--- a/p4_symbolic/BUILD.bazel
+++ b/p4_symbolic/BUILD.bazel
@@ -72,3 +72,12 @@ cc_library(
         "@com_google_absl//absl/strings",
     ],
 )
+
+cc_test(
+    name = "z3_util_test",
+    srcs = ["z3_util_test.cc"],
+    deps = [
+        ":z3_util",
+        "@com_google_googletest//:gtest_main",
+    ],
+)
diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc
index 434f0c53..ccf635b1 100644
--- a/p4_symbolic/main.cc
+++ b/p4_symbolic/main.cc
@@ -42,6 +42,7 @@ ABSL_FLAG(std::string, entries, "",
           "if the input p4 program contains no (explicit) tables for which "
           "entries are needed.");
 ABSL_FLAG(std::string, debug, "", "Dump the SMT program for debugging");
+ABSL_FLAG(int, port_count, 2, "Number of used ports (numbered 0 to N-1)");
 ABSL_FLAG(bool, hardcoded_parser, true,
           "Use the hardcoded parser during symbolic evaluation");
 
@@ -53,6 +54,7 @@ absl::Status ParseAndEvaluate() {
   const std::string &bmv2_path = absl::GetFlag(FLAGS_bmv2);
   const std::string &entries_path = absl::GetFlag(FLAGS_entries);
   const std::string &debug_path = absl::GetFlag(FLAGS_debug);
+  const int port_count = absl::GetFlag(FLAGS_port_count);
   bool hardcoded_parser = absl::GetFlag(FLAGS_hardcoded_parser);
 
   RET_CHECK(!p4info_path.empty());
@@ -63,11 +65,14 @@ absl::Status ParseAndEvaluate() {
       p4_symbolic::symbolic::Dataplane dataplane,
       p4_symbolic::ParseToIr(bmv2_path, p4info_path, entries_path));
 
+  // Generate port list.
+  std::vector<int> physical_ports(port_count);
+  for (int i = 0; i < port_count; i++) physical_ports[i] = i;
+
   // Evaluate program symbolically.
   ASSIGN_OR_RETURN(
       const std::unique_ptr<p4_symbolic::symbolic::SolverState> &solver_state,
-      p4_symbolic::symbolic::EvaluateP4Pipeline(dataplane,
-                                                std::vector<int>{0, 1}));
+      p4_symbolic::symbolic::EvaluateP4Pipeline(dataplane, physical_ports));
   // Add constraints for parser.
   if (hardcoded_parser) {
     ASSIGN_OR_RETURN(
@@ -151,6 +156,14 @@ absl::Status ParseAndEvaluate() {
                            "scalars.userMetadata.vrf_is_valid")
                     << std::endl;
         }
+        // Custom metadata field defined in testdata/string-optional/program.p4
+        if (packet_option.value().egress_headers.contains(
+                "scalars.userMetadata.string_field")) {
+          std::cout << "\tscalars.userMetadata.string_field = "
+                    << packet_option.value().egress_headers.at(
+                           "scalars.userMetadata.string_field")
+                    << std::endl;
+        }
       } else {
         std::cout << "Cannot find solution!" << std::endl;
       }
diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel
index ca48e2b2..608ae6ec 100644
--- a/p4_symbolic/symbolic/BUILD.bazel
+++ b/p4_symbolic/symbolic/BUILD.bazel
@@ -103,3 +103,26 @@ end_to_end_test(
     smt_golden_file = "expected/basic.smt2",
     table_entries = "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt",
 )
+
+end_to_end_test(
+    name = "string_optional_test",
+    output_golden_file = "expected/string_optional.txt",
+    p4_program = "//p4_symbolic/testdata:string-optional/program.p4",
+    port_count = 3,
+    smt_golden_file = "expected/string_optional.smt2",
+    table_entries = "//p4_symbolic/testdata:string-optional/entries.pb.txt",
+)
+
+cc_test(
+    name = "values_test",
+    srcs = ["values_test.cc"],
+    deps = [
+        ":symbolic",
+        "//gutil:status_matchers",
+        "//gutil:testing",
+        "//p4_pdpi:ir_cc_proto",
+        "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/strings",
+        "@com_google_googletest//:gtest_main",
+    ],
+)
diff --git a/p4_symbolic/symbolic/expected/string_optional.smt2 b/p4_symbolic/symbolic/expected/string_optional.smt2
new file mode 100644
index 00000000..af847f33
--- /dev/null
+++ b/p4_symbolic/symbolic/expected/string_optional.smt2
@@ -0,0 +1,382 @@
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let ((?x56 (ite (and (and true (and $x43 (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let (($x66 (and true $x65)))
+ (let ((?x76 (ite $x66 0 (ite (and true true) 1 (- 1)))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (and (and (not $x51) true) (= ?x76 (- 1))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let ((?x56 (ite (and (and true (and $x43 (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let (($x66 (and true $x65)))
+ (let ((?x76 (ite $x66 0 (ite (and true true) 1 (- 1)))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (let (($x144 (and (not $x51) true)))
+ (and $x144 (= ?x76 0))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let ((?x56 (ite (and (and true (and $x43 (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let (($x66 (and true $x65)))
+ (let ((?x76 (ite $x66 0 (ite (and true true) 1 (- 1)))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (and (and (not $x51) true) (= ?x76 1)))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let (($x41 (and true (= standard_metadata.ingress_port (concat (_ bv0 7) (_ bv2 2))))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))))
+ (let (($x42 (and true $x32)))
+ (let ((?x62 (ite $x42 0 (ite (and true $x36) 1 (ite (and true $x41) 2 (- 1))))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let ((?x56 (ite (and (and true (and (not $x32) (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true (not $x32)) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (and (and (not $x51) true) (= ?x62 (- 1)))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let (($x41 (and true (= standard_metadata.ingress_port (concat (_ bv0 7) (_ bv2 2))))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))))
+ (let (($x42 (and true $x32)))
+ (let ((?x62 (ite $x42 0 (ite (and true $x36) 1 (ite (and true $x41) 2 (- 1))))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let ((?x56 (ite (and (and true (and (not $x32) (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true (not $x32)) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (let (($x144 (and (not $x51) true)))
+ (and $x144 (= ?x62 0)))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let (($x41 (and true (= standard_metadata.ingress_port (concat (_ bv0 7) (_ bv2 2))))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))))
+ (let (($x42 (and true $x32)))
+ (let ((?x62 (ite $x42 0 (ite (and true $x36) 1 (ite (and true $x41) 2 (- 1))))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let ((?x56 (ite (and (and true (and (not $x32) (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true (not $x32)) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (and (and (not $x51) true) (= ?x62 1))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let (($x41 (and true (= standard_metadata.ingress_port (concat (_ bv0 7) (_ bv2 2))))))
+ (let (($x36 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv1 1))))))
+ (let (($x32 (and true (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))))
+ (let (($x42 (and true $x32)))
+ (let ((?x62 (ite $x42 0 (ite (and true $x36) 1 (ite (and true $x41) 2 (- 1))))))
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let ((?x56 (ite (and (and true (and (not $x32) (not $x36))) $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true (not $x32)) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (and (and (not $x51) true) (= ?x62 2))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
+(assert
+ (let (($x85 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x86 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x80) $x85)))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) $x86)))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (or $x51 (or (or (or false (= ?x77 (_ bv0 9))) (= ?x77 (_ bv1 9))) (= ?x77 (_ bv2 9)))))))))))))))))))))
+(assert
+ (let ((?x34 (concat (_ bv0 8) (_ bv1 1))))
+ (let ((?x39 (concat (_ bv0 7) (_ bv2 2))))
+ (let ((?x29 (concat (_ bv0 8) (_ bv0 1))))
+ (let (($x41 (and true (= standard_metadata.ingress_port ?x39))))
+ (let (($x32 (and true (= standard_metadata.ingress_port ?x29))))
+ (let (($x43 (not $x32)))
+ (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port ?x34)))))))
+ (let ((?x56 (ite (and $x48 $x41) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
+ (let (($x36 (and true (= standard_metadata.ingress_port ?x34))))
+ (let (($x42 (and true $x32)))
+ (let ((?x63 (ite $x42 ?x39 (ite (and (and true $x43) $x36) ?x34 ?x56))))
+ (let (($x65 (and true (= ?x63 ?x39))))
+ (let ((?x75 (ite (and (and true (not $x65)) true) ?x34 standard_metadata.egress_spec)))
+ (let (($x66 (and true $x65)))
+ (let ((?x77 (ite $x66 ?x29 ?x75)))
+ (let (($x51 (= ?x77 (_ bv511 9))))
+ (and (and (not $x51) true) (= (- 1) (- 1))))))))))))))))))))
+(check-sat)
+
diff --git a/p4_symbolic/symbolic/expected/string_optional.txt b/p4_symbolic/symbolic/expected/string_optional.txt
new file mode 100644
index 00000000..72409dad
--- /dev/null
+++ b/p4_symbolic/symbolic/expected/string_optional.txt
@@ -0,0 +1,42 @@
+Finding packet for table MyIngress.optional_match and row -1
+Cannot find solution!
+
+Finding packet for table MyIngress.optional_match and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+	scalars.userMetadata.string_field = VALUE-0
+
+Finding packet for table MyIngress.optional_match and row 1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000010
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-2
+
+Finding packet for table MyIngress.set_field_table and row -1
+Cannot find solution!
+
+Finding packet for table MyIngress.set_field_table and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+	scalars.userMetadata.string_field = VALUE-0
+
+Finding packet for table MyIngress.set_field_table and row 1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-1
+
+Finding packet for table MyIngress.set_field_table and row 2
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000010
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-2
+
+Finding packet for table tbl_program92 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000010
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-2
+
diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2
new file mode 100644
index 00000000..5142be5e
--- /dev/null
+++ b/p4_symbolic/symbolic/expected/vrf.smt2
@@ -0,0 +1,696 @@
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let ((?x153 (ite (and $x84 $x95) 0 (ite (and $x84 $x101) 3 (ite (and $x84 $x107) 2 (- 1))))))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x67 (ite ipv4.$valid$ (ite $x82 (ite $x108 1 ?x153) (- 1)) (- 1))))
+ (let (($x66 (ite ipv4.$valid$ (ite $x82 $x84 false) false)))
+ (let (($x122 (and $x84 (and (and (and (not $x90) (not $x95)) (not $x101)) (not $x107)))))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 (and (and (not $x90) (not $x95)) (not $x101))) $x107)))
+ (let (($x115 (and (and $x84 (and (not $x90) (not $x95))) $x101)))
+ (let ((?x144 (ite $x115 ?x130 (ite $x119 ?x130 (ite $x122 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x111 (and (and $x84 (not $x90)) $x95)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) ?x144))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x66) (= ?x67 (- 1))))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let ((?x153 (ite (and $x84 $x95) 0 (ite (and $x84 $x101) 3 (ite (and $x84 $x107) 2 (- 1))))))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x67 (ite ipv4.$valid$ (ite $x82 (ite $x108 1 ?x153) (- 1)) (- 1))))
+ (let (($x66 (ite ipv4.$valid$ (ite $x82 $x84 false) false)))
+ (let (($x122 (and $x84 (and (and (and (not $x90) (not $x95)) (not $x101)) (not $x107)))))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 (and (and (not $x90) (not $x95)) (not $x101))) $x107)))
+ (let (($x115 (and (and $x84 (and (not $x90) (not $x95))) $x101)))
+ (let ((?x144 (ite $x115 ?x130 (ite $x119 ?x130 (ite $x122 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x111 (and (and $x84 (not $x90)) $x95)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) ?x144))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (let (($x341 (and (not $x49) $x66)))
+ (and $x341 (= ?x67 0))))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let ((?x153 (ite (and $x84 $x95) 0 (ite (and $x84 $x101) 3 (ite (and $x84 $x107) 2 (- 1))))))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x67 (ite ipv4.$valid$ (ite $x82 (ite $x108 1 ?x153) (- 1)) (- 1))))
+ (let (($x66 (ite ipv4.$valid$ (ite $x82 $x84 false) false)))
+ (let (($x122 (and $x84 (and (and (and (not $x90) (not $x95)) (not $x101)) (not $x107)))))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 (and (and (not $x90) (not $x95)) (not $x101))) $x107)))
+ (let (($x115 (and (and $x84 (and (not $x90) (not $x95))) $x101)))
+ (let ((?x144 (ite $x115 ?x130 (ite $x119 ?x130 (ite $x122 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x111 (and (and $x84 (not $x90)) $x95)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) ?x144))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x66) (= ?x67 1)))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let ((?x153 (ite (and $x84 $x95) 0 (ite (and $x84 $x101) 3 (ite (and $x84 $x107) 2 (- 1))))))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x67 (ite ipv4.$valid$ (ite $x82 (ite $x108 1 ?x153) (- 1)) (- 1))))
+ (let (($x66 (ite ipv4.$valid$ (ite $x82 $x84 false) false)))
+ (let (($x122 (and $x84 (and (and (and (not $x90) (not $x95)) (not $x101)) (not $x107)))))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 (and (and (not $x90) (not $x95)) (not $x101))) $x107)))
+ (let (($x115 (and (and $x84 (and (not $x90) (not $x95))) $x101)))
+ (let ((?x144 (ite $x115 ?x130 (ite $x119 ?x130 (ite $x122 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x111 (and (and $x84 (not $x90)) $x95)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) ?x144))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x66) (= ?x67 2)))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let ((?x153 (ite (and $x84 $x95) 0 (ite (and $x84 $x101) 3 (ite (and $x84 $x107) 2 (- 1))))))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x67 (ite ipv4.$valid$ (ite $x82 (ite $x108 1 ?x153) (- 1)) (- 1))))
+ (let (($x66 (ite ipv4.$valid$ (ite $x82 $x84 false) false)))
+ (let (($x122 (and $x84 (and (and (and (not $x90) (not $x95)) (not $x101)) (not $x107)))))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 (and (and (not $x90) (not $x95)) (not $x101))) $x107)))
+ (let (($x115 (and (and $x84 (and (not $x90) (not $x95))) $x101)))
+ (let ((?x144 (ite $x115 ?x130 (ite $x119 ?x130 (ite $x122 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x111 (and (and $x84 (not $x90)) $x95)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) ?x144))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x66) (= ?x67 3)))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x83 (ite ipv4.$valid$ (ite $x62 0 (ite (and $x50 $x61) 1 (- 1))) (- 1))))
+ (let (($x68 (ite ipv4.$valid$ $x50 false)))
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let ((?x80 (ite $x62 ?x79 (ite (and (and $x50 (not $x56)) $x61) ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let (($x65 (and (and $x50 (not $x56)) $x61)))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x68) (= ?x83 (- 1)))))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x83 (ite ipv4.$valid$ (ite $x62 0 (ite (and $x50 $x61) 1 (- 1))) (- 1))))
+ (let (($x68 (ite ipv4.$valid$ $x50 false)))
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let ((?x80 (ite $x62 ?x79 (ite (and (and $x50 (not $x56)) $x61) ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let (($x65 (and (and $x50 (not $x56)) $x61)))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x68) (= ?x83 0))))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x83 (ite ipv4.$valid$ (ite $x62 0 (ite (and $x50 $x61) 1 (- 1))) (- 1))))
+ (let (($x68 (ite ipv4.$valid$ $x50 false)))
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let ((?x80 (ite $x62 ?x79 (ite (and (and $x50 (not $x56)) $x61) ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let (($x65 (and (and $x50 (not $x56)) $x61)))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) $x68) (= ?x83 1))))))))))))))))))))))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun scalars.userMetadata.vrf () (_ BitVec 10))
+(declare-fun ipv4.srcAddr () (_ BitVec 32))
+(declare-fun ipv4.$valid$ () Bool)
+(declare-fun ipv4.dstAddr () (_ BitVec 32))
+(declare-fun scalars.userMetadata.vrf_is_valid () (_ BitVec 1))
+(assert
+ (let (($x175 (= standard_metadata.ingress_port (_ bv1 9))))
+ (and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x175))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (or $x49 (or (or false (= ?x164 (_ bv0 9))) (= ?x164 (_ bv1 9))))))))))))))))))))))))))))))))))
+(assert
+ (let ((?x73 (concat (_ bv0 9) (_ bv0 1))))
+ (let (($x61 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
+ (let (($x50 (and true ipv4.$valid$)))
+ (let (($x65 (and (and $x50 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x61)))
+ (let ((?x79 (concat (_ bv0 9) (_ bv1 1))))
+ (let (($x56 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
+ (let (($x62 (and $x50 $x56)))
+ (let ((?x80 (ite $x62 ?x79 (ite $x65 ?x73 scalars.userMetadata.vrf))))
+ (let (($x89 (= ?x80 ?x73)))
+ (let (($x107 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x89)))
+ (let (($x101 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x80 ?x79))))
+ (let (($x95 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x89)))
+ (let (($x90 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x89)))
+ (let (($x109 (not $x90)))
+ (let (($x113 (and $x109 (not $x95))))
+ (let (($x117 (and $x113 (not $x101))))
+ (let ((?x75 (ite true (_ bv1 1) (_ bv0 1))))
+ (let ((?x76 (ite $x65 ?x75 (ite true (ite false (_ bv1 1) (_ bv0 1)) scalars.userMetadata.vrf_is_valid))))
+ (let ((?x81 (ite $x62 ?x75 ?x76)))
+ (let (($x82 (bvuge ?x81 (_ bv1 1))))
+ (let (($x84 (and $x50 $x82)))
+ (let ((?x124 (ite (and $x84 (and $x117 (not $x107))) (_ bv511 9) standard_metadata.egress_spec)))
+ (let ((?x130 (concat (_ bv0 8) (_ bv1 1))))
+ (let (($x119 (and (and $x84 $x117) $x107)))
+ (let (($x115 (and (and $x84 $x113) $x101)))
+ (let (($x111 (and (and $x84 $x109) $x95)))
+ (let (($x108 (and $x84 $x90)))
+ (let ((?x164 (ite $x108 ?x130 (ite $x111 (concat (_ bv0 8) (_ bv0 1)) (ite $x115 ?x130 (ite $x119 ?x130 ?x124))))))
+ (let (($x49 (= ?x164 (_ bv511 9))))
+ (and (and (not $x49) true) (= (- 1) (- 1)))))))))))))))))))))))))))))))))
+(check-sat)
+
diff --git a/p4_symbolic/symbolic/expected/vrf.txt b/p4_symbolic/symbolic/expected/vrf.txt
new file mode 100644
index 00000000..355f0642
--- /dev/null
+++ b/p4_symbolic/symbolic/expected/vrf.txt
@@ -0,0 +1,83 @@
+Finding packet for table packet_ingress.ipv4_lpm_table and row -1
+Cannot find solution!
+
+Finding packet for table packet_ingress.ipv4_lpm_table and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+	ipv4.srcAddr = #x29210000
+	ipv4.dstAddr = #x0a0a0002
+	ethernet.dstAddr = #x000000000000
+	scalars.userMetadata.vrf = VRF1
+	scalars.userMetadata.vrf_is_valid = #b1
+
+Finding packet for table packet_ingress.ipv4_lpm_table and row 1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x29210000
+	ipv4.dstAddr = #x0a0a0000
+	ethernet.dstAddr = #x000000000000
+	scalars.userMetadata.vrf = VRF1
+	scalars.userMetadata.vrf_is_valid = #b1
+
+Finding packet for table packet_ingress.ipv4_lpm_table and row 2
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x29210000
+	ipv4.dstAddr = #x0a1a0000
+	ethernet.dstAddr = #x00000000000a
+	scalars.userMetadata.vrf = VRF1
+	scalars.userMetadata.vrf_is_valid = #b1
+
+Finding packet for table packet_ingress.ipv4_lpm_table and row 3
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x00210100
+	ipv4.dstAddr = #x14140000
+	ethernet.dstAddr = #x160000000016
+	scalars.userMetadata.vrf = VRF2
+	scalars.userMetadata.vrf_is_valid = #b1
+
+Finding packet for table packet_ingress.set_vrf_table and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x00000909
+	ipv4.dstAddr = #x00000000
+	ethernet.dstAddr = #x000000000000
+	scalars.userMetadata.vrf = VRF1
+	scalars.userMetadata.vrf_is_valid = #b0
+
+Finding packet for table packet_ingress.set_vrf_table and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x00210100
+	ipv4.dstAddr = #x14140000
+	ethernet.dstAddr = #x160000000016
+	scalars.userMetadata.vrf = VRF2
+	scalars.userMetadata.vrf_is_valid = #b1
+
+Finding packet for table packet_ingress.set_vrf_table and row 1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x21210000
+	ipv4.dstAddr = #x0a0a0000
+	ethernet.dstAddr = #x000000000000
+	scalars.userMetadata.vrf = VRF1
+	scalars.userMetadata.vrf_is_valid = #b1
+
+Finding packet for table tbl_vrf133 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000001
+	ipv4.srcAddr = #x21210000
+	ipv4.dstAddr = #x0a0a0000
+	ethernet.dstAddr = #x000000000000
+	scalars.userMetadata.vrf = VRF1
+	scalars.userMetadata.vrf_is_valid = #b1
+
diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc
index dfbc0ee8..effe5f8d 100644
--- a/p4_symbolic/symbolic/table.cc
+++ b/p4_symbolic/symbolic/table.cc
@@ -205,8 +205,15 @@ absl::StatusOr<z3::expr> EvaluateSingleMatch(
 
     case p4::config::v1::MatchField::OPTIONAL: {
       if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch;
+      // According to the P4Runtime spec, "for don't care matches, the P4Runtime
+      // client must omit the field's entire FieldMatch entry when building the
+      // match repeated field of the TableEntry message". Therefore, if the
+      // match value is present for an optional match type, it must be a
+      // concrete value.
       ASSIGN_OR_RETURN(z3::expr value_expression,
-                       values::FormatBmv2Value(match.optional().value()));
+                       values::FormatP4RTValue(
+                           field_name, match_definition.type_name().name(),
+                           match.optional().value(), translator));
       return operators::Eq(field_expression, value_expression);
     }
 
diff --git a/p4_symbolic/symbolic/test.bzl b/p4_symbolic/symbolic/test.bzl
index eeb3c13d..8ae621e1 100644
--- a/p4_symbolic/symbolic/test.bzl
+++ b/p4_symbolic/symbolic/test.bzl
@@ -31,6 +31,7 @@ def end_to_end_test(
         output_golden_file,
         smt_golden_file,
         table_entries = None,
+        port_count = 2,
         p4_deps = []):
     """Macro that defines our end to end tests.
     Given a p4 program, this macro runs our main binary
@@ -103,6 +104,7 @@ def end_to_end_test(
             ("--p4info=$(location %s)" % p4info_file),
             ("--entries=$(location %s)" % table_entries if table_entries else ""),
             ("--debug=$(location %s)" % smt_output_file),
+            ("--port_count=%d" % port_count),
             ("&> $(location %s)" % test_output_file),
         ]),
     )
diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc
index 8dfbfe3c..4056e899 100644
--- a/p4_symbolic/symbolic/values.cc
+++ b/p4_symbolic/symbolic/values.cc
@@ -56,47 +56,6 @@ unsigned int FindBitsize(uint64_t value) {
   return (bitsize > 1 ? bitsize : 1);  // At least 1 bit.
 }
 
-// Turns the given z3 extracted value (as a string) to a uint64_t.
-// Z3 returns an extracted value as either a binary, hex, or int strings
-// dependening on the size of the value and the formatting flags it is
-// initialized with.
-uint64_t StringToInt(std::string value) {
-  static std::unordered_map<char, std::string> hex_to_bin = {
-      {'0', "0000"}, {'1', "0001"}, {'2', "0010"}, {'3', "0011"},
-      {'4', "0100"}, {'5', "0101"}, {'6', "0110"}, {'7', "0111"},
-      {'8', "1000"}, {'9', "1001"}, {'a', "1010"}, {'b', "1011"},
-      {'c', "1100"}, {'d', "1101"}, {'e', "1110"}, {'f', "1111"}};
-
-  bool value_is_hex = absl::StartsWith(value, "#x");
-  bool value_is_binary = absl::StartsWith(value, "#b");
-
-  // Boolean or integer values.
-  if (!value_is_hex && !value_is_binary) {
-    if (value == "true") {
-      return 1;
-    } else if (value == "false") {
-      return 0;
-    } else {
-      return std::stoull(value);
-    }
-  }
-
-  // Make sure value is a binary string without leading base prefix.
-  std::string binary;
-  if (value_is_hex) {
-    // Turn hex to binary.
-    absl::string_view stripped_value = absl::StripPrefix(value, "#x");
-    for (char c : stripped_value) {
-      absl::StrAppend(&binary, hex_to_bin.at(c));
-    }
-  } else if (value_is_binary) {
-    // Strip leading #b for binary strings.
-    binary = absl::StripPrefix(value, "#b");
-  }
-
-  return std::stoull(binary);
-}
-
 }  // namespace
 
 absl::StatusOr<pdpi::IrValue> ParseIrValue(const std::string &value) {
@@ -180,7 +139,7 @@ absl::StatusOr<std::string> TranslateValueToP4RT(
       translator.p4runtime_translation_allocators.at(field_type_name);
 
   // Turn the value from a string to an int.
-  uint64_t int_value = StringToInt(value);
+  uint64_t int_value = Z3ValueStringToInt(value);
   return allocator.IdToString(int_value);
 }
 
@@ -191,7 +150,6 @@ uint64_t IdAllocator::AllocateId(const std::string &string_value) {
   if (this->string_to_id_map_.count(string_value)) {
     return this->string_to_id_map_.at(string_value);
   }
-
   // Allocate new bitvector value and store it in mapping.
   uint64_t int_value = this->counter_++;
   this->string_to_id_map_.insert({string_value, int_value});
diff --git a/p4_symbolic/symbolic/values_test.cc b/p4_symbolic/symbolic/values_test.cc
new file mode 100644
index 00000000..14d4a604
--- /dev/null
+++ b/p4_symbolic/symbolic/values_test.cc
@@ -0,0 +1,41 @@
+#include "p4_symbolic/symbolic/values.h"
+
+#include "absl/container/flat_hash_map.h"
+#include "absl/strings/str_cat.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include "gutil/status_matchers.h"
+#include "gutil/testing.h"
+#include "p4_pdpi/ir.pb.h"
+
+namespace p4_symbolic::symbolic::values {
+namespace {
+
+TEST(TranslateValueToP4RT, ReverseTranslatedValuesAreEqualToTheOriginalOnes) {
+  constexpr int kNumIds = 256;
+  const std::string kFieldName = "dummy_field_name";
+  const std::string kFieldType = "dummy_field_type";
+
+  // Prepare the translator and expected values.
+  P4RuntimeTranslator translator;
+  absl::flat_hash_map<std::string, std::string> z3_value_to_id;
+  for (int i = 0; i < kNumIds; i++) {
+    const std::string id = absl::StrCat("id-", i);
+    pdpi::IrValue ir_value;
+    ir_value.set_str(id);
+    ASSERT_OK_AND_ASSIGN(z3::expr expr, FormatP4RTValue(kFieldName, kFieldType,
+                                                        ir_value, &translator));
+    z3_value_to_id[expr.to_string()] = id;
+  }
+
+  // Check that the reverse translation is as expected.
+  for (const auto& [z3_value, expected_id] : z3_value_to_id) {
+    ASSERT_OK_AND_ASSIGN(
+        const std::string actual_id,
+        TranslateValueToP4RT(kFieldName, z3_value, translator));
+    ASSERT_THAT(actual_id, testing::Eq(expected_id));
+  }
+}
+
+}  // namespace
+}  // namespace p4_symbolic::symbolic::values
diff --git a/p4_symbolic/testdata/string-optional/entries.pb.txt b/p4_symbolic/testdata/string-optional/entries.pb.txt
new file mode 100644
index 00000000..13d1f278
--- /dev/null
+++ b/p4_symbolic/testdata/string-optional/entries.pb.txt
@@ -0,0 +1,111 @@
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 44279369
+      match {
+        field_id: 1
+        exact {
+          value: "\00"
+        }
+      }
+      action {
+        action {
+          action_id: 21593668
+          params {
+            param_id: 1
+            value: "VALUE-0"
+          }
+        }
+      }
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 44279369
+      match {
+        field_id: 1
+        exact {
+          value: "\01"
+        }
+      }
+      action {
+        action {
+          action_id: 21593668
+          params {
+            param_id: 1
+            value: "VALUE-1"
+          }
+        }
+      }
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 44279369
+      match {
+        field_id: 1
+        exact {
+          value: "\02"
+        }
+      }
+      action {
+        action {
+          action_id: 21593668
+          params {
+            param_id: 1
+            value: "VALUE-2"
+          }
+        }
+      }
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 47867719
+      match {
+        field_id: 1
+        optional {
+          value: "VALUE-0"
+        }
+      }
+      action {
+        action {
+          action_id: 21735938
+          params {
+            param_id: 1
+            value: "\00"
+          }
+        }
+      }
+      priority: 2
+    }
+  }
+}
+updates {
+  type: INSERT
+  entity {
+    table_entry {
+      table_id: 47867719
+      action {
+        action {
+          action_id: 21735938
+          params {
+            param_id: 1
+            value: "\01"
+          }
+        }
+      }
+      priority: 1
+    }
+  }
+}
diff --git a/p4_symbolic/testdata/string-optional/program.p4 b/p4_symbolic/testdata/string-optional/program.p4
new file mode 100644
index 00000000..1f7f65b0
--- /dev/null
+++ b/p4_symbolic/testdata/string-optional/program.p4
@@ -0,0 +1,106 @@
+// Copyright 2024 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+/* -*- P4_16 -*- */
+#include <core.p4>
+#include <v1model.p4>
+
+@p4runtime_translation("", string)
+type bit<9> string_field_t;
+
+struct metadata {
+  string_field_t string_field;
+}
+struct headers {}
+
+parser UselessParser(packet_in packet,
+                out headers hdr,
+                inout metadata meta,
+                inout standard_metadata_t standard_metadata) {
+    state start {
+        transition accept;
+    }
+}
+
+control UselessChecksum(inout headers hdr, inout metadata meta) {
+    apply {  }
+}
+
+control UselessEgress(inout headers hdr,
+                 inout metadata meta,
+                 inout standard_metadata_t standard_metadata) {
+    apply { }
+}
+
+control UselessComputeChecksum(inout headers  hdr, inout metadata meta) {
+    apply { }
+}
+
+control UselessDeparser(packet_out packet, in headers hdr) {
+    apply { }
+}
+
+// Forwarding Code
+control MyIngress(inout headers hdr,
+                  inout metadata meta,
+                  inout standard_metadata_t standard_metadata) {
+
+    action set_egress_spec(bit<9> port) {
+        standard_metadata.egress_spec = port;
+    }
+
+    action set_field(string_field_t f) {
+      meta.string_field = f;
+    }
+
+    table set_field_table {
+      key = {
+        standard_metadata.ingress_port : exact;
+      }
+      actions = {
+        @proto_id(1) set_field;
+        @proto_id(2) NoAction;
+      }
+      size = 1024;
+      default_action = NoAction;
+    }
+
+    table optional_match {
+        key = {
+            meta.string_field: optional;
+        }
+        actions = {
+            @proto_id(1) set_egress_spec;
+            @proto_id(2) NoAction;
+        }
+        size = 1024;
+        default_action = NoAction;
+    }
+
+    apply {
+        meta.string_field = (string_field_t)0;
+        set_field_table.apply();
+        optional_match.apply();
+    }
+}
+
+// Switch
+V1Switch(
+    UselessParser(),
+    UselessChecksum(),
+    MyIngress(),
+    UselessEgress(),
+    UselessComputeChecksum(),
+    UselessDeparser()
+) main;
diff --git a/p4_symbolic/testdata/vrf-routing/vrf.p4 b/p4_symbolic/testdata/vrf-routing/vrf.p4
index 10d99600..cb2770e7 100644
--- a/p4_symbolic/testdata/vrf-routing/vrf.p4
+++ b/p4_symbolic/testdata/vrf-routing/vrf.p4
@@ -22,7 +22,7 @@ typedef bit<9> egress_spec_t;
 typedef bit<48> mac_addr_t;
 typedef bit<32> ipv4_addr_t;
 
-@p4runtime_translation("", string) 
+@p4runtime_translation("", string)
 type bit<10> vrf_t;
 
 header ethernet_t {
diff --git a/p4_symbolic/z3_util.cc b/p4_symbolic/z3_util.cc
index b290e893..391627a7 100644
--- a/p4_symbolic/z3_util.cc
+++ b/p4_symbolic/z3_util.cc
@@ -47,4 +47,23 @@ absl::StatusOr<z3::expr> HexStringToZ3Bitvector(const std::string& hex_string,
   return Z3Context().bv_val(decimal.c_str(), *bitwidth);
 }
 
+uint64_t Z3ValueStringToInt(const std::string& value) {
+  if (absl::StartsWith(value, "#x")) {
+    return std::stoull(value.substr(2), /*idx=*/nullptr, /*base=*/16);
+  }
+  if (absl::StartsWith(value, "#b")) {
+    return std::stoull(value.substr(2), /*idx=*/nullptr, /*base=*/2);
+  }
+
+  // Boolean or integer values.
+  if (value == "true") {
+    return 1;
+  } else if (value == "false") {
+    return 0;
+  } else {
+    // Must be a base 10 number.
+    return std::stoull(value, /*idx=*/nullptr, /*base=*/10);
+  }
+}
+
 }  // namespace p4_symbolic
diff --git a/p4_symbolic/z3_util.h b/p4_symbolic/z3_util.h
index f993babc..16a2179b 100644
--- a/p4_symbolic/z3_util.h
+++ b/p4_symbolic/z3_util.h
@@ -34,6 +34,16 @@ absl::StatusOr<z3::expr> HexStringToZ3Bitvector(
     const std::string& hex_string,
     absl::optional<int> bitwidth = absl::nullopt);
 
+// -- Misc. --------------------------------------------------------------------
+
+// Turns the given z3 extracted value (as a string) to a uint64_t.
+// Z3 returns an extracted value as either a binary, hex, or decimal strings
+// dependening on the size of the value and the formatting flags it is
+// initialized with.
+// Note: This function assumes that the input is well-formatted and the result
+// fits in uint64_t (otherwise an exception will be thrown).
+uint64_t Z3ValueStringToInt(const std::string& value);
+
 // == END OF PUBLIC INTERFACE ==================================================
 
 template <size_t num_bits>
diff --git a/p4_symbolic/z3_util_test.cc b/p4_symbolic/z3_util_test.cc
new file mode 100644
index 00000000..88de5194
--- /dev/null
+++ b/p4_symbolic/z3_util_test.cc
@@ -0,0 +1,31 @@
+#include "p4_symbolic/z3_util.h"
+
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+
+namespace p4_symbolic {
+namespace {
+
+TEST(Z3ValueStringToInt, WorksForBoolStrings) {
+  ASSERT_EQ(Z3ValueStringToInt("true"), 1);
+  ASSERT_EQ(Z3ValueStringToInt("false"), 0);
+}
+
+TEST(Z3ValueStringToInt, WorksForBinaryStrings) {
+  ASSERT_EQ(Z3ValueStringToInt("#b10"), 2);
+  ASSERT_EQ(Z3ValueStringToInt("#b01"), 1);
+}
+
+TEST(Z3ValueStringToInt, WorksForHexStrings) {
+  ASSERT_EQ(Z3ValueStringToInt("#x10"), 16);
+  ASSERT_EQ(Z3ValueStringToInt("#xff"), 255);
+  ASSERT_EQ(Z3ValueStringToInt("#x9"), 9);
+}
+
+TEST(Z3ValueStringToInt, WorksForDecimalStrings) {
+  ASSERT_EQ(Z3ValueStringToInt("10"), 10);
+  ASSERT_EQ(Z3ValueStringToInt("900"), 900);
+}
+
+}  // namespace
+}  // namespace p4_symbolic