diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml index 8fd1f68135254e104f961b5a58680c8df63ef81e..85d08bcabeaf8f13ceba5442f5eaa76fa0ac5440 100644 --- a/src/lib/CoAlgMisc.ml +++ b/src/lib/CoAlgMisc.ml @@ -1017,10 +1017,15 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f = FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ]) *) | C.HCMU (name, f1) -> - let () = C.HcFHt.replace vset.(s) f name in - let unfold = C.hc_replace hcF name f f1 in - let appendvars = List.append newvars [name] in - detClosure appendvars nomTbl hcF fset vset atset nomset s unfold + begin + if C.hc_freeIn name f1 + then + C.HcFHt.replace vset.(s) f name + else (); + let unfold = C.hc_replace hcF name f f1 in + let appendvars = List.append newvars [name] in + detClosure appendvars nomTbl hcF fset vset atset nomset s unfold + end | C.HCNU (name, f1) -> let unfold = C.hc_replace hcF name f f1 in detClosure_ nomTbl hcF fset vset atset nomset s unfold