1 files changed, 6 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index bdceced8..2987fd1d 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -339,7 +339,12 @@ Nondetfunction or (e1: expr) (e2: expr) :=
   | (Eop (Oandimm nmask) (prev:::Enil)),
     (Eop (Oandimm mask)
       ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) =>
-      Eop Oor (e1:::e2:::Enil)
+      let zstart := Int.unsigned start in
+      let zstop := int_highest_bit mask in
+      let mask' := Int.repr (zbitfield_mask zstop zstart) in
+      if Int.eq_dec mask mask'
+      then Eop Oor (e1:::e2:::Enil)
+      else Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.