diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index bb942a6aa519791451d9c75707fab9ab7e51dd30..c669295f3a2dd51a676a2bca57584101b31e9e3d 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -2216,6 +2216,44 @@ let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
      else
        f
 
+let rec hc_freeIn variable (f: hcFormula) =
+  match f.HC.node with
+  | HCTRUE
+  | HCFALSE
+  | HCAP _
+  | HCNOT _
+  | HCCONST _
+  | HCCONSTN _ -> false
+  | HCVAR s ->
+     if compare variable s == 0
+     then true
+     else false
+  | HCAT (s, f1) ->
+     hc_freeIn variable f1
+  | HCOR (f1, f2)
+  | HCAND (f1, f2) ->
+     hc_freeIn variable f1 || hc_freeIn variable f2
+  | HCEX (_, f1)
+  | HCAX (_, f1)
+  | HCENFORCES (_, f1)
+  | HCALLOWS (_, f1)
+  | HCMORETHAN  (_, _, f1)
+  | HCMAXEXCEPT  (_, _, f1)
+  | HCATLEASTPROB (_, f1)
+  | HCLESSPROBFAIL (_, f1)
+  | HCID f1 ->
+     hc_freeIn variable f1
+  | HCNORM (f1, f2)
+  | HCNORMN (f1, f2)
+  | HCCHC (f1, f2) ->
+     hc_freeIn variable f1 || hc_freeIn variable f2
+  | HCFUS (first, f1) ->
+     hc_freeIn variable f1
+  | HCMU (var, f1)
+  | HCNU (var, f1) ->
+     (* Do we need to exclude bound variables here? *)
+     hc_freeIn variable f1
+
 
 (** An instantiation of a hash table (of the standard library)
     for hash-consed formulae. The test for equality
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 43f294e057be5c2a57944fba11d4327101fae593..68525e4a12a8a0d1a046d4562c8a939e4f59aeab 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -165,5 +165,6 @@ module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml =
 
 val hc_formula : HcFormula.t -> formula -> hcFormula
 val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
+val hc_freeIn : string -> hcFormula -> bool
 
 module HcFHt : (Hashtbl.S with type key = hcFormula)