[P4-Symbolic] Assign egress_spec to egress_port only when the packet …

…is not dropped in ingress. (#931)

Co-authored-by: kishanps <[email protected]>

p4_symbolic/symbolic/expected/basic.smt2

@@ -241,7 +241,7 @@
 (let ((a!10 (ite (and (and true a!1) (and true (= ipv4.dstAddr #x0a0a0000)))
                  #b000000001
                  (ite a!2 #b000000000 (ite a!5 #b000000001 a!9)))))
-  (ite true a!10 standard_metadata.egress_port))))))
+  (ite (not (= a!10 #b111111111)) a!10 standard_metadata.egress_port))))))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.etherType)) true false))
       (a!3 (not (and true
@@ -299,8 +299,8 @@
 (declare-fun ipv4.dstAddr () (_ BitVec 32))
 (declare-fun ethernet.etherType () (_ BitVec 16))
 (assert
- (let (($x136 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x136)))
+ (let (($x137 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x137)))
 (assert
  (let (($x56 (= ipv4.dstAddr (_ bv168427520 32))))
  (let (($x57 (and true $x56)))
@@ -321,7 +321,7 @@
  (let (($x74 (and (and $x53 $x72) $x61)))
  (let (($x71 (and $x53 $x57)))
  (let ((?x124 (ite $x71 (_ bv1 9) (ite $x74 (_ bv0 9) (ite $x78 (_ bv1 9) ?x94)))))
- (let (($x139 (or (or false (= ?x124 (_ bv0 9))) (= ?x124 (_ bv1 9)))))
+ (let (($x140 (or (or false (= ?x124 (_ bv0 9))) (= ?x124 (_ bv1 9)))))
  (let (($x45 (= ?x124 (_ bv511 9))))
- (or $x45 $x139)))))))))))))))))))))))
+ (or $x45 $x140)))))))))))))))))))))))
 (check-sat)

p4_symbolic/symbolic/expected/conditional.smt2

@@ -79,7 +79,7 @@
 (let ((a!4 (ite (and true (and true (= ethernet.dst_addr #x000000000001)))
                 #b000000001
                 (ite a!1 #b111111111 (ite a!2 #b111111111 a!3)))))
-  (ite true a!4 standard_metadata.egress_port)))
+  (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001)))))
       (a!2 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0)))))
@@ -106,8 +106,8 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun ethernet.dst_addr () (_ BitVec 48))
 (assert
- (let (($x63 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x63)))
+ (let (($x64 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64)))
 (assert
  (let (($x33 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
  (let (($x35 (and true $x33)))
@@ -117,7 +117,7 @@
  (let (($x45 (and true $x44)))
  (let (($x46 (and true $x45)))
  (let ((?x54 (ite $x46 (_ bv1 9) ?x49)))
- (let (($x66 (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9)))))
+ (let (($x67 (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9)))))
  (let (($x56 (= ?x54 (_ bv511 9))))
- (or $x56 $x66))))))))))))
+ (or $x56 $x67))))))))))))
 (check-sat)

p4_symbolic/symbolic/expected/conditional_nonlattice.smt2

@@ -93,7 +93,7 @@
 (let ((a!7 (ite (and true (and true (= ethernet.dst_addr #x000000000001)))
                 #b000000001
                 (ite a!1 #b111111111 (ite a!3 #b111111111 a!6)))))
-  (ite true a!7 standard_metadata.egress_port))))
+  (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port))))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001)))))
       (a!2 (and true
@@ -134,29 +134,29 @@
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (declare-fun ethernet.dst_addr () (_ BitVec 48))
 (assert
- (let (($x172 (= standard_metadata.ingress_port (_ bv19 9))))
- (let (($x167 (= standard_metadata.ingress_port (_ bv18 9))))
- (let (($x162 (= standard_metadata.ingress_port (_ bv17 9))))
- (let (($x157 (= standard_metadata.ingress_port (_ bv16 9))))
- (let (($x152 (= standard_metadata.ingress_port (_ bv15 9))))
- (let (($x147 (= standard_metadata.ingress_port (_ bv14 9))))
- (let (($x142 (= standard_metadata.ingress_port (_ bv13 9))))
- (let (($x137 (= standard_metadata.ingress_port (_ bv12 9))))
- (let (($x132 (= standard_metadata.ingress_port (_ bv11 9))))
- (let (($x127 (= standard_metadata.ingress_port (_ bv10 9))))
- (let (($x122 (= standard_metadata.ingress_port (_ bv9 9))))
- (let (($x117 (= standard_metadata.ingress_port (_ bv8 9))))
- (let (($x112 (= standard_metadata.ingress_port (_ bv7 9))))
- (let (($x107 (= standard_metadata.ingress_port (_ bv6 9))))
- (let (($x102 (= standard_metadata.ingress_port (_ bv5 9))))
- (let (($x97 (= standard_metadata.ingress_port (_ bv4 9))))
- (let (($x92 (= standard_metadata.ingress_port (_ bv3 9))))
- (let (($x87 (= standard_metadata.ingress_port (_ bv2 9))))
- (let (($x82 (= standard_metadata.ingress_port (_ bv1 9))))
- (let (($x88 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x82) $x87)))
- (let (($x123 (or (or (or (or (or (or (or $x88 $x92) $x97) $x102) $x107) $x112) $x117) $x122)))
- (let (($x158 (or (or (or (or (or (or (or $x123 $x127) $x132) $x137) $x142) $x147) $x152) $x157)))
- (or (or (or $x158 $x162) $x167) $x172))))))))))))))))))))))))
+ (let (($x173 (= standard_metadata.ingress_port (_ bv19 9))))
+ (let (($x168 (= standard_metadata.ingress_port (_ bv18 9))))
+ (let (($x163 (= standard_metadata.ingress_port (_ bv17 9))))
+ (let (($x158 (= standard_metadata.ingress_port (_ bv16 9))))
+ (let (($x153 (= standard_metadata.ingress_port (_ bv15 9))))
+ (let (($x148 (= standard_metadata.ingress_port (_ bv14 9))))
+ (let (($x143 (= standard_metadata.ingress_port (_ bv13 9))))
+ (let (($x138 (= standard_metadata.ingress_port (_ bv12 9))))
+ (let (($x133 (= standard_metadata.ingress_port (_ bv11 9))))
+ (let (($x128 (= standard_metadata.ingress_port (_ bv10 9))))
+ (let (($x123 (= standard_metadata.ingress_port (_ bv9 9))))
+ (let (($x118 (= standard_metadata.ingress_port (_ bv8 9))))
+ (let (($x113 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x108 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x103 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x98 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x93 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x88 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x83 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x89 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x83) $x88)))
+ (let (($x124 (or (or (or (or (or (or (or $x89 $x93) $x98) $x103) $x108) $x113) $x118) $x123)))
+ (let (($x159 (or (or (or (or (or (or (or $x124 $x128) $x133) $x138) $x143) $x148) $x153) $x158)))
+ (or (or (or $x159 $x163) $x168) $x173))))))))))))))))))))))))
 (assert
  (let (($x39 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4)))))
  (let (($x33 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4)))))
@@ -173,11 +173,11 @@
  (let (($x64 (and true $x63)))
  (let (($x65 (and true $x64)))
  (let ((?x73 (ite $x65 (_ bv1 9) ?x68)))
- (let (($x95 (or (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))) (= ?x73 (_ bv3 9)))))
- (let (($x115 (or (or (or (or $x95 (= ?x73 (_ bv4 9))) (= ?x73 (_ bv5 9))) (= ?x73 (_ bv6 9))) (= ?x73 (_ bv7 9)))))
- (let (($x135 (or (or (or (or $x115 (= ?x73 (_ bv8 9))) (= ?x73 (_ bv9 9))) (= ?x73 (_ bv10 9))) (= ?x73 (_ bv11 9)))))
- (let (($x155 (or (or (or (or $x135 (= ?x73 (_ bv12 9))) (= ?x73 (_ bv13 9))) (= ?x73 (_ bv14 9))) (= ?x73 (_ bv15 9)))))
- (let (($x175 (or (or (or (or $x155 (= ?x73 (_ bv16 9))) (= ?x73 (_ bv17 9))) (= ?x73 (_ bv18 9))) (= ?x73 (_ bv19 9)))))
+ (let (($x96 (or (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))) (= ?x73 (_ bv3 9)))))
+ (let (($x116 (or (or (or (or $x96 (= ?x73 (_ bv4 9))) (= ?x73 (_ bv5 9))) (= ?x73 (_ bv6 9))) (= ?x73 (_ bv7 9)))))
+ (let (($x136 (or (or (or (or $x116 (= ?x73 (_ bv8 9))) (= ?x73 (_ bv9 9))) (= ?x73 (_ bv10 9))) (= ?x73 (_ bv11 9)))))
+ (let (($x156 (or (or (or (or $x136 (= ?x73 (_ bv12 9))) (= ?x73 (_ bv13 9))) (= ?x73 (_ bv14 9))) (= ?x73 (_ bv15 9)))))
+ (let (($x176 (or (or (or (or $x156 (= ?x73 (_ bv16 9))) (= ?x73 (_ bv17 9))) (= ?x73 (_ bv18 9))) (= ?x73 (_ bv19 9)))))
  (let (($x75 (= ?x73 (_ bv511 9))))
- (or $x75 $x175)))))))))))))))))))))))
+ (or $x75 $x176)))))))))))))))))))))))
 (check-sat)

p4_symbolic/symbolic/expected/conditional_sequence.smt2

@@ -90,7 +90,7 @@
 (egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth
 (egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta
 (egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp
-(egress) standard_metadata.egress_port: (ite true
+(egress) standard_metadata.egress_port: (ite (not (= standard_metadata.egress_spec #b111111111))
      standard_metadata.egress_spec
      (ite (and true true (= h1.fr #xff))
           #b000000001
@@ -113,11 +113,11 @@
 (declare-fun standard_metadata.ingress_port () (_ BitVec 9))
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (assert
- (let (($x108 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x108)))
+ (let (($x109 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x109)))
 (assert
- (let (($x110 (= standard_metadata.egress_spec (_ bv1 9))))
- (let (($x111 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x110)))
+ (let (($x111 (= standard_metadata.egress_spec (_ bv1 9))))
+ (let (($x112 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x111)))
  (let (($x94 (= standard_metadata.egress_spec (_ bv511 9))))
- (or $x94 $x111)))))
+ (or $x94 $x112)))))
 (check-sat)

p4_symbolic/symbolic/expected/hardcoded.smt2

@@ -58,7 +58,8 @@
       (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0)))
                 (concat #x00 #b1)
                 standard_metadata.egress_spec)))
-  (ite true (ite a!1 (concat #x00 #b0) a!2) standard_metadata.egress_port))
+(let ((a!3 (not (= (ite a!1 (concat #x00 #b0) a!2) #b111111111))))
+  (ite a!3 (ite a!1 (concat #x00 #b0) a!2) standard_metadata.egress_port)))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0)))))
       (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0)))
@@ -81,15 +82,15 @@
 (declare-fun standard_metadata.ingress_port () (_ BitVec 9))
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (assert
- (let (($x49 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x49)))
+ (let (($x50 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x50)))
 (assert
  (let ((?x28 (concat (_ bv0 8) (_ bv0 1))))
  (let (($x29 (= standard_metadata.ingress_port ?x28)))
  (let (($x31 (and true $x29)))
  (let (($x32 (and true (not $x29))))
  (let ((?x37 (ite $x32 ?x28 (ite $x31 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec))))
- (let (($x52 (or (or false (= ?x37 (_ bv0 9))) (= ?x37 (_ bv1 9)))))
+ (let (($x53 (or (or false (= ?x37 (_ bv0 9))) (= ?x37 (_ bv1 9)))))
  (let (($x41 (= ?x37 (_ bv511 9))))
- (or $x41 $x52)))))))))
+ (or $x41 $x53)))))))))
 (check-sat)

p4_symbolic/symbolic/expected/reflector.smt2

@@ -54,7 +54,10 @@
 (egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth
 (egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta
 (egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp
-(egress) standard_metadata.egress_port: (ite true
+(egress) standard_metadata.egress_port: (ite (not (= (ite true
+                  standard_metadata.ingress_port
+                  standard_metadata.egress_spec)
+             #b111111111))
      (ite true standard_metadata.ingress_port standard_metadata.egress_spec)
      standard_metadata.egress_port)
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
@@ -75,11 +78,11 @@
 (declare-fun standard_metadata.ingress_port () (_ BitVec 9))
 (declare-fun standard_metadata.egress_spec () (_ BitVec 9))
 (assert
- (let (($x37 (= standard_metadata.ingress_port (_ bv1 9))))
- (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x37)))
+ (let (($x38 (= standard_metadata.ingress_port (_ bv1 9))))
+ (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x38)))
 (assert
  (let ((?x27 (ite true standard_metadata.ingress_port standard_metadata.egress_spec)))
- (let (($x40 (or (or false (= ?x27 (_ bv0 9))) (= ?x27 (_ bv1 9)))))
+ (let (($x41 (or (or false (= ?x27 (_ bv0 9))) (= ?x27 (_ bv1 9)))))
  (let (($x29 (= ?x27 (_ bv511 9))))
- (or $x29 $x40)))))
+ (or $x29 $x41)))))
 (check-sat)

p4_symbolic/symbolic/expected/string_optional.smt2

@@ -94,11 +94,12 @@
                 a!3)))
 (let ((a!5 (and true (and true (= a!4 (concat #b0000000 #b10)))))
       (a!6 (not (and true (= a!4 (concat #b0000000 #b10))))))
-  (ite true
-       (ite a!5
-            #b000000000
-            (ite (and true a!6 true) #b000000001 standard_metadata.egress_spec))
-       standard_metadata.egress_port)))))
+(let ((a!7 (ite a!5
+                #b000000000
+                (ite (and true a!6 true)
+                     #b000000001
+                     standard_metadata.egress_spec))))
+  (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port))))))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (and true
                 (not (and true (= standard_metadata.ingress_port #b000000000)))
@@ -160,7 +161,7 @@
  (let ((?x79 (ite (and (and true (not $x70)) true) (_ bv1 9) standard_metadata.egress_spec)))
  (let (($x71 (and true $x70)))
  (let ((?x81 (ite $x71 (_ bv0 9) ?x79)))
- (let (($x88 (or (or (or false (= ?x81 (_ bv0 9))) (= ?x81 (_ bv1 9))) (= ?x81 (_ bv2 9)))))
+ (let (($x89 (or (or (or false (= ?x81 (_ bv0 9))) (= ?x81 (_ bv1 9))) (= ?x81 (_ bv2 9)))))
  (let (($x51 (= ?x81 (_ bv511 9))))
- (or $x51 $x88)))))))))))))))))))))
+ (or $x51 $x89)))))))))))))))))))))
 (check-sat)

p4_symbolic/symbolic/expected/table.smt2

@@ -62,7 +62,7 @@
                      (and true (= standard_metadata.ingress_port #b000000000)))
                 #b000000001
                 (ite a!1 #b000000000 standard_metadata.egress_spec))))
-  (ite true a!2 standard_metadata.egress_port)))
+  (ite (not (= a!2 #b111111111)) a!2 standard_metadata.egress_port)))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (and true
                 (not (and true (= standard_metadata.ingress_port #b000000000)))
@@ -97,7 +97,7 @@
  (let (($x28 (and true $x27)))
  (let (($x32 (and true $x28)))
  (let ((?x46 (ite $x32 (_ bv1 9) (ite (and $x34 $x31) (_ bv0 9) standard_metadata.egress_spec))))
- (let (($x52 (or (or false (= ?x46 (_ bv0 9))) (= ?x46 (_ bv1 9)))))
+ (let (($x53 (or (or false (= ?x46 (_ bv0 9))) (= ?x46 (_ bv1 9)))))
  (let (($x37 (= ?x46 (_ bv511 9))))
- (or $x37 $x52)))))))))))
+ (or $x37 $x53)))))))))))
 (check-sat)

p4_symbolic/symbolic/expected/table_hit_1.smt2

@@ -82,14 +82,13 @@
 (let ((a!3 (ite (and true (and true (= ethernet.ether_type #x0010)))
                 #b000000010
                 (ite a!2 #b111111111 standard_metadata.egress_spec))))
-  (ite true
-       (ite (and true
-                 (distinct a!1 (- 1))
-                 true
-                 (= ethernet.src_addr #x000000000100))
-            #b000000011
-            a!3)
-       standard_metadata.egress_port)))
+(let ((a!4 (ite (and true
+                     (distinct a!1 (- 1))
+                     true
+                     (= ethernet.src_addr #x000000000100))
+                #b000000011
+                a!3)))
+  (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port))))
 (egress) standard_metadata.egress_rid: standard_metadata.egress_rid
 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (and true (= ethernet.ether_type #x0010))) 0 (- 1)))
       (a!2 (and true (not (and true (= ethernet.ether_type #x0010))))))
@@ -117,15 +116,15 @@
 (declare-fun ethernet.ether_type () (_ BitVec 16))
 (declare-fun ethernet.src_addr () (_ BitVec 48))
 (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 (($x95 (= standard_metadata.ingress_port (_ bv7 9))))
+ (let (($x90 (= standard_metadata.ingress_port (_ bv6 9))))
+ (let (($x85 (= standard_metadata.ingress_port (_ bv5 9))))
+ (let (($x80 (= standard_metadata.ingress_port (_ bv4 9))))
+ (let (($x75 (= standard_metadata.ingress_port (_ bv3 9))))
+ (let (($x71 (= standard_metadata.ingress_port (_ bv2 9))))
+ (let (($x67 (= standard_metadata.ingress_port (_ bv1 9))))
+ (let (($x72 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x67) $x71)))
+ (or (or (or (or (or $x72 $x75) $x80) $x85) $x90) $x95))))))))))
 (assert
  (let ((?x38 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec)))
  (let (($x31 (= ethernet.ether_type (_ bv16 16))))
@@ -136,8 +135,8 @@
  (let (($x46 (and true $x45)))
  (let (($x50 (and $x46 (and true (= ethernet.src_addr (_ bv256 48))))))
  (let ((?x56 (ite $x50 (_ bv3 9) (ite $x33 (_ bv2 9) ?x38))))
- (let (($x77 (or (or (or (or false (= ?x56 (_ bv0 9))) (= ?x56 (_ bv1 9))) (= ?x56 (_ bv2 9))) (= ?x56 (_ bv3 9)))))
- (let (($x97 (or (or (or (or $x77 (= ?x56 (_ bv4 9))) (= ?x56 (_ bv5 9))) (= ?x56 (_ bv6 9))) (= ?x56 (_ bv7 9)))))
+ (let (($x78 (or (or (or (or false (= ?x56 (_ bv0 9))) (= ?x56 (_ bv1 9))) (= ?x56 (_ bv2 9))) (= ?x56 (_ bv3 9)))))
+ (let (($x98 (or (or (or (or $x78 (= ?x56 (_ bv4 9))) (= ?x56 (_ bv5 9))) (= ?x56 (_ bv6 9))) (= ?x56 (_ bv7 9)))))
  (let (($x58 (= ?x56 (_ bv511 9))))
- (or $x58 $x97))))))))))))))
+ (or $x58 $x98))))))))))))))
 (check-sat)