diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index b245be189959940beb813e991fae05850525287d..41ce1ce83b00e34c46a9999b5b93c3055fd811a4 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -2204,11 +2204,17 @@ let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
      let nf1 = func f1 in
 	 if nf1 == f1 then f else gennew (HCFUS(first, nf1))
   | HCMU (var, f1) ->
-     let nf1 = func f1 in
-	 if nf1 == f1 then f else gennew (HCMU(var, nf1))
+	 if compare var name != 0 then
+       let nf1 = func f1 in
+	   if nf1 == f1 then f else gennew (HCMU(var, nf1))
+	 else
+	   f
   | HCNU (var, f1) ->
-     let nf1 = func f1 in
-	 if nf1 == f1 then f else gennew (HCNU(var, nf1))
+	 if compare var name != 0 then
+       let nf1 = func f1 in
+	   if nf1 == f1 then f else gennew (HCNU(var, nf1))
+	 else
+	   f
 
 
 (** An instantiation of a hash table (of the standard library)