[P4-Symbolic] Remove disjointness check on set of tables that get eva…

…luate in each branch of a conditional.
sonic-net · Nov 26, 2024 · b4e7210 · b4e7210
1 parent 161cec5
commit b4e7210
Show file tree

Hide file tree

Showing 12 changed files with 730 additions and 629 deletions.
diff --git 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
@@ -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
@@ -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)