Cloning: disregard invalidated writes when comparing effects (closes #468)

src/mlw/ity.ml

@@ -1162,6 +1162,11 @@ let eff_union e1 e2 =
             (Mreg.set_diff e.eff_writes e.eff_covers));
   e
 
+let eff_fusion e1 e2 =
+  let e = eff_union e1 e2 in
+  {e with eff_writes = Mreg.set_inter e.eff_writes e.eff_covers;
+          eff_taints = Mreg.set_inter e.eff_taints e.eff_covers}
+
 let eff_contaminate e1 e2 =
   if not e1.eff_ghost then e2 else
   if Sxs.is_empty e1.eff_raises then e2 else

src/mlw/ity.mli

@@ -401,6 +401,7 @@ val eff_ghostify_weak : bool -> effect -> effect     (* only if has no effect *)
 
 val eff_union_seq : effect -> effect -> effect  (* checks for stale variables *)
 val eff_union_par : effect -> effect -> effect  (* no stale-variable check *)
+val eff_fusion    : effect -> effect -> effect  (* drop invalidated writes *)
 
 val mask_adjust : effect -> ity -> mask -> mask
 

src/mlw/pmodule.ml

@@ -1158,7 +1158,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       if mask_spill ss.rs_cty.cty_mask rs.rs_cty.cty_mask then
         raise (BadInstance (BadI_rs_mask rs.rs_name));
       let eff = eff_ghostify (rs_ghost rs) cty.cty_effect in
-      let eff' = eff_union_par eff ss.rs_cty.cty_effect in
+      let eff' = eff_fusion eff ss.rs_cty.cty_effect in
       if not (eff_equal eff eff') then begin
         (* Format.eprintf "@[%a@]@\n" print_cty cty; *)
         (* Format.eprintf "@[%a@]@\n" print_cty ss.rs_cty; *)