diff --git a/p4_symbolic/symbolic/expected/table_hit_2.smt2 b/p4_symbolic/symbolic/expected/table_hit_2.smt2
new file mode 100644
index 00000000..684383af
--- /dev/null
+++ b/p4_symbolic/symbolic/expected/table_hit_2.smt2
@@ -0,0 +1,341 @@
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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))))))))))))))
+(assert
+ (let (($x37 (and true (and true (= h1.f1 (_ bv255 8))))))
+ (let ((?x41 (ite $x37 0 (- 1))))
+ (let (($x49 (= ?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 (($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))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 (($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))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
+ (let ((?x51 (ite $x48 0 (- 1))))
+ (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))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 (($x48 (and $x45 (and true (= h1.f2 (_ bv255 8))))))
+ (let ((?x51 (ite $x48 0 (- 1))))
+ (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)))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 ((?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 (($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))))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 ((?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 (($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)))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 (($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))))))))))))
+(check-sat)
+
+; 
+(set-info :status unknown)
+(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
+(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
+(declare-fun h1.f1 () (_ BitVec 8))
+(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))))))))))
+(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 (($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))))))))))))
+(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 (($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))))))))))))
+(check-sat)
+