diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 63e59e9be9c783c9c4c157749d01fb0f6861e295..edf5ba91fe76053c9ac37a839af9b1af9d0e15c8 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1783,7 +1783,8 @@ let hash_hcFormula_node f =
   | HCTRUE -> 0
   | HCFALSE -> 1
   | HCAP s
-  | HCNOT s -> base * Hashtbl.hash s + 1
+  | HCNOT s
+  | HCVAR s -> base * Hashtbl.hash s + 1
   | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
   | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
   | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
@@ -1802,6 +1803,8 @@ let hash_hcFormula_node f =
   | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
   | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
   | HCID (f1) -> base * f1.HC.hkey + 20
+  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
+  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
 
 (** Determines the "real" formula of a formula node.
     @param f A formula node.
@@ -1812,6 +1815,7 @@ let toFml_hcFormula_node f =
   | HCTRUE -> TRUE
   | HCFALSE -> FALSE
   | HCAP s -> AP s
+  | HCVAR s -> VAR s
   | HCNOT s -> NOT (AP s)
   | HCAT (s, f1) -> AT (s, f1.HC.fml)
   | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
@@ -1831,6 +1835,8 @@ let toFml_hcFormula_node f =
   | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
   | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
   | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
+  | HCMU (var, f1) -> MU (var, f1.HC.fml)
+  | HCNU (var, f1) -> NU (var, f1.HC.fml)
 
 (** Determines the negation (in negation normal form) of a formula node.
     @param f A formula node.
@@ -1885,6 +1891,7 @@ let rec hc_formula hcF f =
   | TRUE -> HcFormula.hashcons hcF HCTRUE
   | FALSE -> HcFormula.hashcons hcF HCFALSE
   | AP s -> HcFormula.hashcons hcF (HCAP s)
+  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
   | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
   | AT (s, f1) ->
       let tf1 = hc_formula hcF f1 in
@@ -1946,6 +1953,12 @@ let rec hc_formula hcF f =
   | FUS (first, f1) ->
       let tf1 = hc_formula hcF f1 in
       HcFormula.hashcons hcF (HCFUS (first, tf1))
+  | MU (var, f1) ->
+	 let tf1 = hc_formula hcF f1 in
+	 HcFormula.hashcons hcF (HCMU (var, tf1))
+  | NU (var, f1) ->
+	 let tf1 = hc_formula hcF f1 in
+	 HcFormula.hashcons hcF (HCNU (var, tf1))
   | AF _
   | EF _
   | AG _