diff --git a/p4_symbolic/symbolic/conditional.cc b/p4_symbolic/symbolic/conditional.cc
index 945c18bb1..85815e512 100644
--- a/p4_symbolic/symbolic/conditional.cc
+++ b/p4_symbolic/symbolic/conditional.cc
@@ -66,10 +66,10 @@ absl::StatusOr<SymbolicTableMatches> EvaluateConditional(
           data_plane, get_next_control_for_branch(conditional.else_branch()),
           state, translator, else_guard));
 
-  // Now we have two traces that need merging. The two traces are guaranteed to
-  // contain different table matches (see go/optimized-symbolic-execution).
-  ASSIGN_OR_RETURN(SymbolicTableMatches merged_matches,
-                   util::MergeDisjointTableMatches(if_matches, else_matches));
+  // Now we have two traces that need merging.
+  ASSIGN_OR_RETURN(
+      SymbolicTableMatches merged_matches,
+      util::MergeMatchesOnCondition(condition, if_matches, else_matches));
 
   if (!conditional.optimized_symbolic_execution_info()
            .continue_to_merge_point()) {
diff --git a/p4_symbolic/symbolic/expected/basic.smt2 b/p4_symbolic/symbolic/expected/basic.smt2
index ea71f2374..670ef6d17 100644
--- a/p4_symbolic/symbolic/expected/basic.smt2
+++ b/p4_symbolic/symbolic/expected/basic.smt2
@@ -5,8 +5,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun ipv4.$valid$ () Bool)
 (assert
- (let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
+ (let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
 (assert
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
@@ -34,7 +34,8 @@
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
  (let (($x60 (and $x42 $x46)))
- (let ((?x112 (ite $x60 1 ?x102)))
+ (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
+ (let (($x119 (ite ipv4.$valid$ $x42 false)))
  (let (($x61 (not $x46)))
  (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
  (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
@@ -46,7 +47,7 @@
  (let (($x63 (and (and $x42 $x61) $x50)))
  (let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
  (let (($x41 (= ?x113 (_ bv511 9))))
- (and (and (not $x41) $x42) (= ?x112 (- 1)))))))))))))))))))))))
+ (and (and (not $x41) $x119) (= ?x120 (- 1))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -56,8 +57,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun ipv4.$valid$ () Bool)
 (assert
- (let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
+ (let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
 (assert
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
@@ -85,7 +86,8 @@
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
  (let (($x60 (and $x42 $x46)))
- (let ((?x112 (ite $x60 1 ?x102)))
+ (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
+ (let (($x119 (ite ipv4.$valid$ $x42 false)))
  (let (($x61 (not $x46)))
  (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
  (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
@@ -97,8 +99,8 @@
  (let (($x63 (and (and $x42 $x61) $x50)))
  (let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
  (let (($x41 (= ?x113 (_ bv511 9))))
- (let (($x244 (and (not $x41) $x42)))
- (and $x244 (= ?x112 0)))))))))))))))))))))))
+ (let (($x246 (and (not $x41) $x119)))
+ (and $x246 (= ?x120 0))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -108,8 +110,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun ipv4.$valid$ () Bool)
 (assert
- (let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
+ (let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
 (assert
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
@@ -137,7 +139,8 @@
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
  (let (($x60 (and $x42 $x46)))
- (let ((?x112 (ite $x60 1 ?x102)))
+ (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
+ (let (($x119 (ite ipv4.$valid$ $x42 false)))
  (let (($x61 (not $x46)))
  (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
  (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
@@ -149,7 +152,7 @@
  (let (($x63 (and (and $x42 $x61) $x50)))
  (let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
  (let (($x41 (= ?x113 (_ bv511 9))))
- (and (and (not $x41) $x42) (= ?x112 1))))))))))))))))))))))
+ (and (and (not $x41) $x119) (= ?x120 1)))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -159,8 +162,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun ipv4.$valid$ () Bool)
 (assert
- (let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
+ (let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
 (assert
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
@@ -188,7 +191,8 @@
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
  (let (($x60 (and $x42 $x46)))
- (let ((?x112 (ite $x60 1 ?x102)))
+ (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
+ (let (($x119 (ite ipv4.$valid$ $x42 false)))
  (let (($x61 (not $x46)))
  (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
  (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
@@ -200,7 +204,7 @@
  (let (($x63 (and (and $x42 $x61) $x50)))
  (let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
  (let (($x41 (= ?x113 (_ bv511 9))))
- (and (and (not $x41) $x42) (= ?x112 2))))))))))))))))))))))
+ (and (and (not $x41) $x119) (= ?x120 2)))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -210,8 +214,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun ipv4.$valid$ () Bool)
 (assert
- (let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
+ (let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
 (assert
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
@@ -239,7 +243,8 @@
  (let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x46 (and true $x45)))
  (let (($x60 (and $x42 $x46)))
- (let ((?x112 (ite $x60 1 ?x102)))
+ (let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
+ (let (($x119 (ite ipv4.$valid$ $x42 false)))
  (let (($x61 (not $x46)))
  (let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
  (let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
@@ -251,6 +256,6 @@
  (let (($x63 (and (and $x42 $x61) $x50)))
  (let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
  (let (($x41 (= ?x113 (_ bv511 9))))
- (and (and (not $x41) $x42) (= ?x112 3))))))))))))))))))))))
+ (and (and (not $x41) $x119) (= ?x120 3)))))))))))))))))))))))
 (check-sat)
 
diff --git a/p4_symbolic/symbolic/expected/conditional.smt2 b/p4_symbolic/symbolic/expected/conditional.smt2
index 194deea5c..29458bd67 100644
--- a/p4_symbolic/symbolic/expected/conditional.smt2
+++ b/p4_symbolic/symbolic/expected/conditional.smt2
@@ -4,30 +4,31 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun ethernet.dst_addr () (_ BitVec 48))
 (assert
- (let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59)))
+ (let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
 (assert
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
+ (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
 (assert
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
+ (let (($x39 (ite $x31 $x33 false)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (and (and (not $x52) $x33) (= (- 1) (- 1)))))))))))))
+ (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (and (and (not $x54) $x39) (= (- 1) (- 1))))))))))))))
 (check-sat)
 
 ; 
@@ -36,30 +37,31 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun ethernet.dst_addr () (_ BitVec 48))
 (assert
- (let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59)))
+ (let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
 (assert
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
+ (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
 (assert
  (let (($x34 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
- (let (($x33 (and true $x31)))
- (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (and (and (not $x52) $x34) (= (- 1) (- 1)))))))))))))
+ (let (($x40 (ite $x31 false $x34)))
+ (let ((?x38 (ite $x34 (_ bv511 9) (ite (and true $x31) (_ bv511 9) standard_metadata.egress_spec))))
+ (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x38)))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (and (and (not $x54) $x40) (= (- 1) (- 1))))))))))))))
 (check-sat)
 
 ; 
@@ -68,31 +70,31 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun ethernet.dst_addr () (_ BitVec 48))
 (assert
- (let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59)))
+ (let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
 (assert
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
+ (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
 (assert
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x47 (ite $x42 0 (- 1))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x49 (ite $x44 0 (- 1))))
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not $x41)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (and (and (not $x52) true) (= ?x47 (- 1))))))))))))))
+ (let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (and (and (not $x54) true) (= ?x49 (- 1))))))))))))))
 (check-sat)
 
 ; 
@@ -101,31 +103,31 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun ethernet.dst_addr () (_ BitVec 48))
 (assert
- (let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59)))
+ (let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
 (assert
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
+ (let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
 (assert
- (let (($x40 (= ethernet.dst_addr (_ bv1 48))))
- (let (($x41 (and true $x40)))
- (let (($x42 (and true $x41)))
- (let ((?x47 (ite $x42 0 (- 1))))
+ (let (($x42 (= ethernet.dst_addr (_ bv1 48))))
+ (let (($x43 (and true $x42)))
+ (let (($x44 (and true $x43)))
+ (let ((?x49 (ite $x44 0 (- 1))))
  (let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x33 (and true $x31)))
  (let (($x34 (and true (not $x31))))
- (let ((?x45 (ite (and true (not $x41)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
- (let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
- (let (($x52 (= ?x50 (_ bv511 9))))
- (let (($x95 (and (not $x52) true)))
- (and $x95 (= ?x47 0))))))))))))))
+ (let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
+ (let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
+ (let (($x54 (= ?x52 (_ bv511 9))))
+ (let (($x97 (and (not $x54) true)))
+ (and $x97 (= ?x49 0))))))))))))))
 (check-sat)
 
diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 b/p4_symbolic/symbolic/expected/conditional_sequence.smt2
index 439220010..521c97308 100644
--- a/p4_symbolic/symbolic/expected/conditional_sequence.smt2
+++ b/p4_symbolic/symbolic/expected/conditional_sequence.smt2
@@ -4,17 +4,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f1 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x41 (and true (not (= h1.f1 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x41) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x38 (= h1.f1 ?x37)))
+ (let (($x44 (ite $x38 false (and true (not $x38)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x44) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -23,17 +25,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f2 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x46 (and true (not (= h1.f2 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x46) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x45 (= h1.f2 ?x37)))
+ (let (($x50 (ite $x45 false (and true (not $x45)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x50) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -42,17 +46,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x50 (and true (not (= h1.f3 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x50) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x51 (= h1.f3 ?x37)))
+ (let (($x56 (ite $x51 false (and true (not $x51)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x56) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -61,17 +67,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f4 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x54 (and true (not (= h1.f4 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x54) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x57 (= h1.f4 ?x37)))
+ (let (($x62 (ite $x57 false (and true (not $x57)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x62) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -80,17 +88,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f5 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x58 (and true (not (= h1.f5 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x58) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x63 (= h1.f5 ?x37)))
+ (let (($x68 (ite $x63 false (and true (not $x63)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x68) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -99,17 +109,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f6 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x62 (and true (not (= h1.f6 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x62) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x69 (= h1.f6 ?x37)))
+ (let (($x74 (ite $x69 false (and true (not $x69)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x74) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -118,17 +130,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f7 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x66 (and true (not (= h1.f7 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x66) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x75 (= h1.f7 ?x37)))
+ (let (($x80 (ite $x75 false (and true (not $x75)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x80) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -137,17 +151,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f8 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x70 (and true (not (= h1.f8 (concat (_ bv0 7) (_ bv0 1)))))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x70) (= (- 1) (- 1)))))))
+ (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
+ (let (($x81 (= h1.f8 ?x37)))
+ (let (($x86 (ite $x81 false (and true (not $x81)))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x86) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -156,19 +172,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f1 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
  (let (($x38 (= h1.f1 ?x37)))
- (let (($x40 (and true $x38)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x40) (= (- 1) (- 1)))))))))
+ (let (($x43 (ite $x38 (and true $x38) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x43) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -177,19 +193,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f2 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x43 (= h1.f2 ?x37)))
- (let (($x45 (and true $x43)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x45) (= (- 1) (- 1)))))))))
+ (let (($x45 (= h1.f2 ?x37)))
+ (let (($x49 (ite $x45 (and true $x45) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x49) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -198,19 +214,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x47 (= h1.f3 ?x37)))
- (let (($x49 (and true $x47)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x49) (= (- 1) (- 1)))))))))
+ (let (($x51 (= h1.f3 ?x37)))
+ (let (($x55 (ite $x51 (and true $x51) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x55) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -219,19 +235,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f4 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x51 (= h1.f4 ?x37)))
- (let (($x53 (and true $x51)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x53) (= (- 1) (- 1)))))))))
+ (let (($x57 (= h1.f4 ?x37)))
+ (let (($x61 (ite $x57 (and true $x57) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x61) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -240,19 +256,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f5 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x55 (= h1.f5 ?x37)))
- (let (($x57 (and true $x55)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x57) (= (- 1) (- 1)))))))))
+ (let (($x63 (= h1.f5 ?x37)))
+ (let (($x67 (ite $x63 (and true $x63) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x67) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -261,19 +277,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f6 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x59 (= h1.f6 ?x37)))
- (let (($x61 (and true $x59)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x61) (= (- 1) (- 1)))))))))
+ (let (($x69 (= h1.f6 ?x37)))
+ (let (($x73 (ite $x69 (and true $x69) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x73) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -282,19 +298,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f7 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x63 (= h1.f7 ?x37)))
- (let (($x65 (and true $x63)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x65) (= (- 1) (- 1)))))))))
+ (let (($x75 (= h1.f7 ?x37)))
+ (let (($x79 (ite $x75 (and true $x75) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x79) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -303,19 +319,19 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.f8 () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
  (let ((?x37 (concat (_ bv0 7) (_ bv0 1))))
- (let (($x67 (= h1.f8 ?x37)))
- (let (($x69 (and true $x67)))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (let (($x134 (not $x76)))
- (and (and $x134 $x69) (= (- 1) (- 1)))))))))
+ (let (($x81 (= h1.f8 ?x37)))
+ (let (($x85 (ite $x81 (and true $x81) false)))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (let (($x150 (not $x92)))
+ (and (and $x150 $x85) (= (- 1) (- 1)))))))))
 (check-sat)
 
 ; 
@@ -324,16 +340,16 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.fr () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x74 (and true (and true (= h1.fr (_ bv255 8))))))
- (let ((?x78 (ite $x74 0 (- 1))))
- (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x78 (- 1))))))
+ (let (($x90 (and true (and true (= h1.fr (_ bv255 8))))))
+ (let ((?x94 (ite $x90 0 (- 1))))
+ (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x94 (- 1))))))
 (check-sat)
 
 ; 
@@ -342,14 +358,14 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun h1.fr () (_ BitVec 8))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x90)))
+ (let (($x106 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x106)))
 (assert
- (let (($x92 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x76 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x76 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x92)))))
+ (let (($x108 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x92 (= standard_metadata.egress_spec (_ bv511 9))))
+ (or $x92 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x108)))))
 (assert
- (let (($x74 (and true (and true (= h1.fr (_ bv255 8))))))
- (let ((?x78 (ite $x74 0 (- 1))))
- (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x78 0)))))
+ (let (($x90 (and true (and true (= h1.fr (_ bv255 8))))))
+ (let ((?x94 (ite $x90 0 (- 1))))
+ (and (and (not (= standard_metadata.egress_spec (_ bv511 9))) true) (= ?x94 0)))))
 (check-sat)
diff --git a/p4_symbolic/symbolic/expected/hardcoded.smt2 b/p4_symbolic/symbolic/expected/hardcoded.smt2
index d91998907..76c947da0 100644
--- a/p4_symbolic/symbolic/expected/hardcoded.smt2
+++ b/p4_symbolic/symbolic/expected/hardcoded.smt2
@@ -3,24 +3,25 @@
 (declare-fun standard_metadata.ingress_port () (_ BitVec 9))
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (assert
- (let (($x45 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x45)))
+ (let (($x47 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x47)))
 (assert
  (let ((?x26 (concat (_ bv0 8) (_ bv0 1))))
  (let (($x27 (= standard_metadata.ingress_port ?x26)))
  (let (($x29 (and true $x27)))
  (let (($x30 (and true (not $x27))))
  (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec))))
- (let (($x37 (= ?x35 (_ bv511 9))))
- (or $x37 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9)))))))))))
+ (let (($x39 (= ?x35 (_ bv511 9))))
+ (or $x39 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9)))))))))))
 (assert
  (let ((?x26 (concat (_ bv0 8) (_ bv0 1))))
  (let (($x27 (= standard_metadata.ingress_port ?x26)))
  (let (($x29 (and true $x27)))
+ (let (($x36 (ite $x27 $x29 false)))
  (let (($x30 (and true (not $x27))))
  (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec))))
- (let (($x37 (= ?x35 (_ bv511 9))))
- (and (and (not $x37) $x29) (= (- 1) (- 1))))))))))
+ (let (($x39 (= ?x35 (_ bv511 9))))
+ (and (and (not $x39) $x36) (= (- 1) (- 1)))))))))))
 (check-sat)
 
 ; 
@@ -28,23 +29,24 @@
 (declare-fun standard_metadata.ingress_port () (_ BitVec 9))
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (assert
- (let (($x45 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x45)))
+ (let (($x47 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x47)))
 (assert
  (let ((?x26 (concat (_ bv0 8) (_ bv0 1))))
  (let (($x27 (= standard_metadata.ingress_port ?x26)))
  (let (($x29 (and true $x27)))
  (let (($x30 (and true (not $x27))))
  (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec))))
- (let (($x37 (= ?x35 (_ bv511 9))))
- (or $x37 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9)))))))))))
+ (let (($x39 (= ?x35 (_ bv511 9))))
+ (or $x39 (or (or false (= ?x35 (_ bv0 9))) (= ?x35 (_ bv1 9)))))))))))
 (assert
  (let (($x30 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
  (let ((?x26 (concat (_ bv0 8) (_ bv0 1))))
  (let (($x27 (= standard_metadata.ingress_port ?x26)))
+ (let (($x37 (ite $x27 false $x30)))
  (let (($x29 (and true $x27)))
  (let ((?x35 (ite $x30 ?x26 (ite $x29 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec))))
- (let (($x37 (= ?x35 (_ bv511 9))))
- (and (and (not $x37) $x30) (= (- 1) (- 1))))))))))
+ (let (($x39 (= ?x35 (_ bv511 9))))
+ (and (and (not $x39) $x37) (= (- 1) (- 1)))))))))))
 (check-sat)
 
diff --git a/p4_symbolic/symbolic/expected/table_hit_1.smt2 b/p4_symbolic/symbolic/expected/table_hit_1.smt2
index 8860c77ca..12f996338 100644
--- a/p4_symbolic/symbolic/expected/table_hit_1.smt2
+++ b/p4_symbolic/symbolic/expected/table_hit_1.smt2
@@ -5,38 +5,41 @@
 (declare-fun ethernet.ether_type () (_ BitVec 16))
 (declare-fun ethernet.src_addr () (_ BitVec 48))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
- (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+ (let (($x92 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x87 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x82 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x77 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x68 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68)))
+ (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92))))))))))
 (assert
  (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
- (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
- (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
- (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (or $x49 $x93))))))))))))
+ (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (or $x56 $x95))))))))))))))
 (assert
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
  (let ((?x38 (ite $x31 0 (- 1))))
  (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
- (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (and (and (not $x49) true) (= ?x38 (- 1)))))))))))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (and (and (not $x56) true) (= ?x38 (- 1))))))))))))))
 (check-sat)
 
 ; 
@@ -46,39 +49,42 @@
 (declare-fun ethernet.ether_type () (_ BitVec 16))
 (declare-fun ethernet.src_addr () (_ BitVec 48))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
- (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+ (let (($x92 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x87 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x82 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x77 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x68 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68)))
+ (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92))))))))))
 (assert
  (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
- (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
- (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
- (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (or $x49 $x93))))))))))))
+ (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (or $x56 $x95))))))))))))))
 (assert
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
  (let ((?x38 (ite $x31 0 (- 1))))
  (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
- (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (let (($x206 (and (not $x49) true)))
- (and $x206 (= ?x38 0)))))))))))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (let (($x208 (and (not $x56) true)))
+ (and $x208 (= ?x38 0))))))))))))))
 (check-sat)
 
 ; 
@@ -88,39 +94,43 @@
 (declare-fun ethernet.ether_type () (_ BitVec 16))
 (declare-fun ethernet.src_addr () (_ BitVec 48))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
- (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+ (let (($x92 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x87 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x82 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x77 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x68 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68)))
+ (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92))))))))))
 (assert
  (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
- (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
- (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
- (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (or $x49 $x93))))))))))))
+ (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (or $x56 $x95))))))))))))))
 (assert
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
  (let ((?x38 (ite $x31 0 (- 1))))
- (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
- (let ((?x51 (ite $x48 0 (- 1))))
+ (let ((?x50 (ite $x43 (ite $x48 0 (- 1)) (- 1))))
+ (let (($x49 (ite $x43 $x44 false)))
  (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
  (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (and (and (not $x49) $x44) (= ?x51 (- 1))))))))))))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (and (and (not $x56) $x49) (= ?x50 (- 1))))))))))))))))
 (check-sat)
 
 ; 
@@ -130,38 +140,42 @@
 (declare-fun ethernet.ether_type () (_ BitVec 16))
 (declare-fun ethernet.src_addr () (_ BitVec 48))
 (assert
- (let (($x90 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x85 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x80 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x75 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x62 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x67 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x62) $x66)))
- (or (or (or (or (or $x67 $x70) $x75) $x80) $x85) $x90))))))))))
+ (let (($x92 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x87 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x82 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x77 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x68 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x69 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64) $x68)))
+ (or (or (or (or (or $x69 $x72) $x77) $x82) $x87) $x92))))))))))
 (assert
  (let ((?x36 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
- (let (($x44 (and true (and (distinct (ite $x31 0 (- 1)) (- 1)) true))))
+ (let ((?x38 (ite $x31 0 (- 1))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x54 (ite $x48 (_ bv3 9) (ite $x31 (_ bv2 9) ?x36))))
- (let (($x73 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
- (let (($x93 (or (or (or (or $x73 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (or $x49 $x93))))))))))))
+ (let (($x75 (or (or (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))) (= ?x54 (_ bv2 9))) (= ?x54 (_ bv3 9)))))
+ (let (($x95 (or (or (or (or $x75 (= ?x54 (_ bv4 9))) (= ?x54 (_ bv5 9))) (= ?x54 (_ bv6 9))) (= ?x54 (_ bv7 9)))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (or $x56 $x95))))))))))))))
 (assert
  (let (($x29 (= ethernet.ether_type (_ bv16 16))))
  (let (($x30 (and true $x29)))
  (let (($x31 (and true $x30)))
  (let ((?x38 (ite $x31 0 (- 1))))
- (let (($x44 (and true (and (distinct ?x38 (- 1)) true))))
+ (let (($x43 (and (distinct ?x38 (- 1)) true)))
+ (let (($x44 (and true $x43)))
  (let (($x48 (and $x44 (and true (= ethernet.src_addr (_ bv256 48))))))
- (let ((?x51 (ite $x48 0 (- 1))))
+ (let ((?x50 (ite $x43 (ite $x48 0 (- 1)) (- 1))))
+ (let (($x49 (ite $x43 $x44 false)))
  (let ((?x41 (ite $x31 (_ bv2 9) (ite (and true (not $x30)) (_ bv511 9) standard_metadata.egress_spec))))
  (let ((?x54 (ite $x48 (_ bv3 9) ?x41)))
- (let (($x49 (= ?x54 (_ bv511 9))))
- (and (and (not $x49) $x44) (= ?x51 0)))))))))))))
+ (let (($x56 (= ?x54 (_ bv511 9))))
+ (and (and (not $x56) $x49) (= ?x50 0)))))))))))))))
 (check-sat)
 
diff --git a/p4_symbolic/symbolic/expected/table_hit_2.smt2 b/p4_symbolic/symbolic/expected/table_hit_2.smt2
index 684383afe..68790db9e 100644
--- a/p4_symbolic/symbolic/expected/table_hit_2.smt2
+++ b/p4_symbolic/symbolic/expected/table_hit_2.smt2
@@ -6,41 +6,43 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
- (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
- (let (($x49 (= ?x41 (- 1))))
- (let (($x50 (and true $x49)))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
+ (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
- (let (($x49 (= ?x41 (- 1))))
+ (let (($x54 (= ?x41 (- 1))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct ?x41 (- 1)) true))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true $x49)))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) true) $x49))))))))))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) true) $x54)))))))))))))
 (check-sat)
 
 ; 
@@ -51,38 +53,43 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct ?x41 (- 1)) true))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= ?x41 (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) true) (= ?x41 0))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) true) (= ?x41 0))))))))))))))
 (check-sat)
 
 ; 
@@ -93,39 +100,45 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
- (let (($x45 (and true (and (distinct ?x41 (- 1)) true))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let ((?x51 (ite $x48 0 (- 1))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let ((?x65 (ite $x54 (- 1) (ite $x44 (ite $x48 0 (- 1)) (- 1)))))
+ (let (($x64 (ite $x54 false (ite $x44 $x45 false))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x50 (and true (= ?x41 (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) $x45) (= ?x51 (- 1))))))))))))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) $x64) (= ?x65 (- 1)))))))))))))))))
 (check-sat)
 
 ; 
@@ -136,39 +149,45 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
- (let (($x45 (and true (and (distinct ?x41 (- 1)) true))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let ((?x51 (ite $x48 0 (- 1))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let ((?x65 (ite $x54 (- 1) (ite $x44 (ite $x48 0 (- 1)) (- 1)))))
+ (let (($x64 (ite $x54 false (ite $x44 $x45 false))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x50 (and true (= ?x41 (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) $x45) (= ?x51 0)))))))))))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) $x64) (= ?x65 0))))))))))))))))
 (check-sat)
 
 ; 
@@ -179,39 +198,45 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
- (let (($x50 (and true (= ?x41 (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x59 (ite $x56 0 (- 1))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x60 (ite $x54 (ite $x58 0 (- 1)) (- 1))))
+ (let (($x59 (ite $x54 $x55 false)))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct ?x41 (- 1)) true))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) $x50) (= ?x59 (- 1))))))))))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) $x59) (= ?x60 (- 1)))))))))))))))))
 (check-sat)
 
 ; 
@@ -222,39 +247,45 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x41 (ite $x37 0 (- 1))))
- (let (($x50 (and true (= ?x41 (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x59 (ite $x56 0 (- 1))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x60 (ite $x54 (ite $x58 0 (- 1)) (- 1))))
+ (let (($x59 (ite $x54 $x55 false)))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct ?x41 (- 1)) true))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) $x50) (= ?x59 0)))))))))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) $x59) (= ?x60 0))))))))))))))))
 (check-sat)
 
 ; 
@@ -265,37 +296,43 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) true) (= (- 1) (- 1))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) true) (= (- 1) (- 1)))))))))))))))
 (check-sat)
 
 ; 
@@ -306,36 +343,42 @@
 (declare-fun h1.f2 () (_ BitVec 8))
 (declare-fun h1.f3 () (_ BitVec 8))
 (assert
- (let (($x94 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x89 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x84 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x79 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x74 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x70 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x66 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x71 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x66) $x70)))
- (or (or (or (or (or $x71 $x74) $x79) $x84) $x89) $x94))))))))))
+ (let (($x100 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x95 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x76 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x72 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x77 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x72) $x76)))
+ (or (or (or (or (or $x77 $x80) $x85) $x90) $x95) $x100))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x77 (or (or (or (or false (= ?x61 (_ bv0 9))) (= ?x61 (_ bv1 9))) (= ?x61 (_ bv2 9))) (= ?x61 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x61 (_ bv4 9))) (= ?x61 (_ bv5 9))) (= ?x61 (_ bv6 9))) (= ?x61 (_ bv7 9)))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (or $x39 $x97))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x83 (or (or (or (or false (= ?x63 (_ bv0 9))) (= ?x63 (_ bv1 9))) (= ?x63 (_ bv2 9))) (= ?x63 (_ bv3 9)))))
+ (let (($x103 (or (or (or (or $x83 (= ?x63 (_ bv4 9))) (= ?x63 (_ bv5 9))) (= ?x63 (_ bv6 9))) (= ?x63 (_ bv7 9)))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (or $x39 $x103)))))))))))))))
 (assert
  (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
  (let ((?x43 (ite $x37 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec))))
- (let (($x45 (and true (and (distinct (ite $x37 0 (- 1)) (- 1)) true))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x44 (and (distinct ?x41 (- 1)) true)))
+ (let (($x45 (and true $x44)))
  (let (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
- (let (($x50 (and true (= (ite $x37 0 (- 1)) (- 1)))))
- (let (($x56 (and $x50 (and true (= h1.f3 (_ bv255 8))))))
- (let ((?x61 (ite $x56 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
- (let (($x39 (= ?x61 (_ bv511 9))))
- (and (and (not $x39) true) (= (- 1) (- 1))))))))))))
+ (let (($x54 (= ?x41 (- 1))))
+ (let (($x55 (and true $x54)))
+ (let (($x58 (and $x55 (and true (= h1.f3 (_ bv255 8))))))
+ (let ((?x63 (ite $x58 (_ bv3 9) (ite $x48 (_ bv2 9) ?x43))))
+ (let (($x39 (= ?x63 (_ bv511 9))))
+ (and (and (not $x39) true) (= (- 1) (- 1)))))))))))))))
 (check-sat)
 
diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2
index 2bf13d320..c60829860 100644
--- a/p4_symbolic/symbolic/expected/vrf.smt2
+++ b/p4_symbolic/symbolic/expected/vrf.smt2
@@ -8,8 +8,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -30,7 +30,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -38,7 +39,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -53,13 +54,15 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80))))
  (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90)))
  (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1))))))
  (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90)))
  (let (($x109 (and $x85 $x91)))
- (let ((?x157 (ite $x109 1 ?x149)))
+ (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1))))
+ (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false)))
  (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108)))))
  (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108)))
  (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102)))
@@ -67,7 +70,7 @@
  (let (($x112 (and (and $x85 (not $x91)) $x96)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x85) (= ?x157 (- 1)))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x69) (= ?x70 (- 1)))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -80,8 +83,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -102,7 +105,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -110,7 +114,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -125,13 +129,15 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80))))
  (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90)))
  (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1))))))
  (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90)))
  (let (($x109 (and $x85 $x91)))
- (let ((?x157 (ite $x109 1 ?x149)))
+ (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1))))
+ (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false)))
  (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108)))))
  (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108)))
  (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102)))
@@ -139,8 +145,8 @@
  (let (($x112 (and (and $x85 (not $x91)) $x96)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (let (($x307 (and (not $x52) $x85)))
- (and $x307 (= ?x157 0)))))))))))))))))))))))))))))))
+ (let (($x309 (and (not $x52) $x69)))
+ (and $x309 (= ?x70 0)))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -153,8 +159,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -175,7 +181,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -183,7 +190,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -198,13 +205,15 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80))))
  (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90)))
  (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1))))))
  (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90)))
  (let (($x109 (and $x85 $x91)))
- (let ((?x157 (ite $x109 1 ?x149)))
+ (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1))))
+ (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false)))
  (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108)))))
  (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108)))
  (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102)))
@@ -212,7 +221,7 @@
  (let (($x112 (and (and $x85 (not $x91)) $x96)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x85) (= ?x157 1))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x69) (= ?x70 1))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -225,8 +234,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -247,7 +256,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -255,7 +265,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -270,13 +280,15 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80))))
  (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90)))
  (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1))))))
  (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90)))
  (let (($x109 (and $x85 $x91)))
- (let ((?x157 (ite $x109 1 ?x149)))
+ (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1))))
+ (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false)))
  (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108)))))
  (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108)))
  (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102)))
@@ -284,7 +296,7 @@
  (let (($x112 (and (and $x85 (not $x91)) $x96)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x85) (= ?x157 2))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x69) (= ?x70 2))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -297,8 +309,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -319,7 +331,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -327,7 +340,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -342,13 +355,15 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let (($x102 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x81 ?x80))))
  (let (($x96 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x90)))
  (let ((?x149 (ite (and $x85 $x96) 0 (ite (and $x85 $x102) 3 (ite (and $x85 $x108) 2 (- 1))))))
  (let (($x91 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x90)))
  (let (($x109 (and $x85 $x91)))
- (let ((?x157 (ite $x109 1 ?x149)))
+ (let ((?x70 (ite ipv4.$valid$ (ite $x83 (ite $x109 1 ?x149) (- 1)) (- 1))))
+ (let (($x69 (ite ipv4.$valid$ (ite $x83 $x85 false) false)))
  (let (($x123 (and $x85 (and (and (and (not $x91) (not $x96)) (not $x102)) (not $x108)))))
  (let (($x120 (and (and $x85 (and (and (not $x91) (not $x96)) (not $x102))) $x108)))
  (let (($x116 (and (and $x85 (and (not $x91) (not $x96))) $x102)))
@@ -356,7 +371,7 @@
  (let (($x112 (and (and $x85 (not $x91)) $x96)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) ?x142))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x85) (= ?x157 3))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x69) (= ?x70 3))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -369,8 +384,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -391,7 +406,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -399,13 +415,14 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
  (let (($x53 (and true ipv4.$valid$)))
  (let (($x59 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
  (let (($x65 (and $x53 $x59)))
- (let ((?x79 (ite $x65 0 (ite (and $x53 $x64) 1 (- 1)))))
+ (let ((?x84 (ite ipv4.$valid$ (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))) (- 1))))
+ (let (($x71 (ite ipv4.$valid$ $x53 false)))
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x68 (and (and $x53 (not $x59)) $x64)))
  (let ((?x80 (concat (_ bv0 9) (_ bv1 1))))
@@ -421,7 +438,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -429,7 +447,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x53) (= ?x79 (- 1))))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x71) (= ?x84 (- 1))))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -442,8 +460,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -464,7 +482,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -472,13 +491,14 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
  (let (($x53 (and true ipv4.$valid$)))
  (let (($x59 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
  (let (($x65 (and $x53 $x59)))
- (let ((?x79 (ite $x65 0 (ite (and $x53 $x64) 1 (- 1)))))
+ (let ((?x84 (ite ipv4.$valid$ (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))) (- 1))))
+ (let (($x71 (ite ipv4.$valid$ $x53 false)))
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x68 (and (and $x53 (not $x59)) $x64)))
  (let ((?x80 (concat (_ bv0 9) (_ bv1 1))))
@@ -494,7 +514,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -502,7 +523,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x53) (= ?x79 0)))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x71) (= ?x84 0)))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -515,8 +536,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -537,7 +558,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -545,13 +567,14 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
  (let (($x53 (and true ipv4.$valid$)))
  (let (($x59 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32)))))
  (let (($x65 (and $x53 $x59)))
- (let ((?x79 (ite $x65 0 (ite (and $x53 $x64) 1 (- 1)))))
+ (let ((?x84 (ite ipv4.$valid$ (ite $x65 0 (ite (and $x53 $x64) 1 (- 1))) (- 1))))
+ (let (($x71 (ite ipv4.$valid$ $x53 false)))
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x68 (and (and $x53 (not $x59)) $x64)))
  (let ((?x80 (concat (_ bv0 9) (_ bv1 1))))
@@ -567,7 +590,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -575,7 +599,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) $x53) (= ?x79 1)))))))))))))))))))))))))))))))
+ (and (and (not $x52) $x71) (= ?x84 1)))))))))))))))))))))))))))))))))
 (check-sat)
 
 ; 
@@ -588,8 +612,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1))
 (assert
- (let (($x86 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x86)))
+ (let (($x169 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x169)))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -610,7 +634,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -618,7 +643,7 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9))))))))))))))))))))))))))))))))
+ (or $x52 (or (or false (= ?x158 (_ bv0 9))) (= ?x158 (_ bv1 9)))))))))))))))))))))))))))))))))
 (assert
  (let ((?x50 (concat (_ bv0 9) (_ bv0 1))))
  (let (($x64 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32)))))
@@ -639,7 +664,8 @@
  (let ((?x47 (ite false (_ bv1 1) (_ bv0 1))))
  (let ((?x76 (ite true (_ bv1 1) (_ bv0 1))))
  (let ((?x82 (ite $x65 ?x76 (ite $x68 ?x76 (ite true ?x47 scalars.local_metadata_t.vrf_is_valid)))))
- (let (($x85 (and $x53 (bvuge ?x82 (_ bv1 1)))))
+ (let (($x83 (bvuge ?x82 (_ bv1 1))))
+ (let (($x85 (and $x53 $x83)))
  (let ((?x125 (ite (and $x85 (and $x118 (not $x108))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x120 (and (and $x85 $x118) $x108)))
  (let (($x116 (and (and $x85 $x114) $x102)))
@@ -647,5 +673,5 @@
  (let (($x109 (and $x85 $x91)))
  (let ((?x158 (ite $x109 (_ bv1 9) (ite $x112 (_ bv0 9) (ite $x116 (_ bv1 9) (ite $x120 (_ bv1 9) ?x125))))))
  (let (($x52 (= ?x158 (_ bv511 9))))
- (and (and (not $x52) true) (= (- 1) (- 1)))))))))))))))))))))))))))))))
+ (and (and (not $x52) true) (= (- 1) (- 1))))))))))))))))))))))))))))))))
 (check-sat)
diff --git a/p4_symbolic/symbolic/expected/vrf.txt b/p4_symbolic/symbolic/expected/vrf.txt
index c2573bf90..297fffc02 100644
--- a/p4_symbolic/symbolic/expected/vrf.txt
+++ b/p4_symbolic/symbolic/expected/vrf.txt
@@ -6,7 +6,7 @@ Finding packet for table packet_ingress.ipv4_lpm_table and row 0
 	standard_metadata.ingress_port = #b000000000
 	standard_metadata.egress_spec = #b000000000
 	ipv4.srcAddr = #x29210000
-	ipv4.dstAddr = #x0a0a0080
+	ipv4.dstAddr = #x0a0a0004
 	ethernet.dstAddr = #x000000000000
 	scalars.local_metadata_t.vrf = VRF1
 	scalars.local_metadata_t.vrf_is_valid = #b1
@@ -44,8 +44,8 @@ Finding packet for table packet_ingress.ipv4_lpm_table and row 3
 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 = #x21000809
+	standard_metadata.egress_spec = #b000000000
+	ipv4.srcAddr = #x20000909
 	ipv4.dstAddr = #x00000000
 	ethernet.dstAddr = #x000000000000
 	scalars.local_metadata_t.vrf = VRF1
@@ -66,7 +66,7 @@ Finding packet for table packet_ingress.set_vrf_table and row 1
 	standard_metadata.ingress_port = #b000000000
 	standard_metadata.egress_spec = #b000000001
 	ipv4.srcAddr = #x21210000
-	ipv4.dstAddr = #x0a000000
+	ipv4.dstAddr = #x0a140000
 	ethernet.dstAddr = #x00000000000a
 	scalars.local_metadata_t.vrf = VRF1
 	scalars.local_metadata_t.vrf_is_valid = #b1
@@ -76,7 +76,7 @@ Finding packet for table tbl_vrf133 and row -1
 	standard_metadata.ingress_port = #b000000000
 	standard_metadata.egress_spec = #b000000001
 	ipv4.srcAddr = #x21210000
-	ipv4.dstAddr = #x0a000000
-	ethernet.dstAddr = #x000000000000
+	ipv4.dstAddr = #x0a140000
+	ethernet.dstAddr = #x00000000000a
 	scalars.local_metadata_t.vrf = VRF1
-	scalars.local_metadata_t.vrf_is_valid = #b0
+	scalars.local_metadata_t.vrf_is_valid = #b1
diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc
index 39d0ed24f..ab5add35a 100644
--- a/p4_symbolic/symbolic/table.cc
+++ b/p4_symbolic/symbolic/table.cc
@@ -484,15 +484,17 @@ absl::StatusOr<SymbolicTableMatches> EvaluateTable(
   for (const auto &[action, next_control] : sorted_action_to_next_control) {
     if (next_control != merge_point) {
       if (action == ir::TableHitAction() || action == ir::TableMissAction()) {
-        z3::expr branch_guard = action == ir::TableHitAction()
-                                    ? (match_index != kDefaultActionEntryIndex)
-                                    : (match_index == kDefaultActionEntryIndex);
+        z3::expr branch_condition =
+            action == ir::TableHitAction()
+                ? (match_index != kDefaultActionEntryIndex)
+                : (match_index == kDefaultActionEntryIndex);
         ASSIGN_OR_RETURN(
             SymbolicTableMatches branch_matches,
             control::EvaluateControl(data_plane, next_control, state,
-                                     translator, guard && branch_guard));
-        ASSIGN_OR_RETURN(merged_matches, util::MergeDisjointTableMatches(
-                                             merged_matches, branch_matches));
+                                     translator, guard && branch_condition));
+        ASSIGN_OR_RETURN(merged_matches,
+                         util::MergeMatchesOnCondition(
+                             branch_condition, branch_matches, merged_matches));
       } else {
         return absl::UnimplementedError(
             absl::Substitute("Conditional on executed table action is not "
diff --git a/p4_symbolic/symbolic/test.bzl b/p4_symbolic/symbolic/test.bzl
index b0b58d53c..ea6166a68 100644
--- a/p4_symbolic/symbolic/test.bzl
+++ b/p4_symbolic/symbolic/test.bzl
@@ -105,8 +105,6 @@ def end_to_end_test(
             ("--entries=$(location %s)" % table_entries if table_entries else ""),
             ("--debug=$(location %s)" % smt_output_file),
             ("--port_count=%d" % port_count),
-            # Redirect stderr to stdout, so we can capture both.
-            "2>&1",
             # Use `tee` to simultaneously capture output in file yet still print it to stdout, to
             # ease debugging.
             ("| tee $(location %s)" % test_output_file),
diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc
index 4e1e69033..e17ac707f 100644
--- a/p4_symbolic/symbolic/util.cc
+++ b/p4_symbolic/symbolic/util.cc
@@ -21,6 +21,7 @@
 #include "absl/status/status.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/substitute.h"
+#include "glog/logging.h"
 #include "p4_pdpi/utils/ir.h"
 #include "p4_symbolic/symbolic/operators.h"
 #include "p4_symbolic/z3_util.h"
@@ -139,18 +140,12 @@ absl::StatusOr<SymbolicTableMatches> MergeMatchesOnCondition(
     const SymbolicTableMatches &false_matches) {
   SymbolicTableMatches merged;
 
-  // Add all tables matches in true_trace.
+  // Merge all tables matches in true_trace (including ones in both traces).
   for (const auto &[name, true_match] : true_matches) {
-    // The table should not be applied in the other branch.
-    if (false_matches.contains(name)) {
-      return absl::InternalError(
-          absl::Substitute("Table '$0' was symbolically executed both in true "
-                           "and false branches, this is not expected",
-                           name));
-    }
-
-    // Get the default match for the false branch.
-    const SymbolicTableMatch false_match = DefaultTableMatch();
+    // Find match in other trace (or use default).
+    const SymbolicTableMatch false_match = false_matches.contains(name)
+                                               ? false_matches.at(name)
+                                               : DefaultTableMatch();
 
     // Merge this match.
     ASSIGN_OR_RETURN(
@@ -165,14 +160,12 @@ absl::StatusOr<SymbolicTableMatches> MergeMatchesOnCondition(
                          }});
   }
 
-  // Add all tables matches in false_matches.
+  // Merge all tables matches in false_matches only.
   for (const auto &[name, false_match] : false_matches) {
-    // The table should not be applied in the other branch.
     if (true_matches.contains(name)) {
-      return absl::InternalError(
-          absl::Substitute("Table '$0' was symbolically executed both in true "
-                           "and false branches, this is not expected",
-                           name));
+      // Already covered.
+      LOG(WARNING) << "Table '" << name << "' is evaluated more than once.";
+      continue;
     }
 
     // Get the default match for the true branch.