diff --git a/src/lib/MiscSolver.ml b/src/lib/MiscSolver.ml
index 9d5501f43290d457e936f6e12288d7cd0cc85572..c0435faf5b228b38097da1ca0cc639d62abb6974 100644
--- a/src/lib/MiscSolver.ml
+++ b/src/lib/MiscSolver.ml
@@ -335,6 +335,7 @@ let foldBS f bs init =
   done;
   !res
 
+(*
 
 (** Represents a set of annotated formulae as a bit vector.
     All sets contain the formula True, that is bstrue,
@@ -543,7 +544,7 @@ let blitBSa (src : annbitset) (trg : bitset) =
   for i = 0 to pred !nrFormulae do
     if memABS src i then addBSNoChk trg i else ()
   done
-
+*)
 
 (** Selects a principal formula from a set of formulae if possible.
     @param bs A bitset of formulae.
@@ -590,6 +591,7 @@ let rec intern_mkEXList bs bnd acc i =
 
 let mkEXList bs = intern_mkEXList bs !lposEX [] !hposEX
 
+(*
 (** Constructs a list of all EX-formulae of a set of annotated formulae.
     @param abs The annotated bitset of formulae.
     @param bnd The greatest integer representing an EX-formula.
@@ -604,7 +606,7 @@ let rec intern_mkEXListAnn abs bnd acc i =
   else acc
 
 let mkEXListAnn abs = intern_mkEXListAnn abs !lposEX [] !hposEX
-
+*)
 
 (** Prints a "collection" as a set.
     @param ps A string prefixing the set.
@@ -637,6 +639,7 @@ let exportFSet expF bs = foldBS (fun i acc -> (expF i)::acc) bs []
   !res
  *)
 
+(*
 (** Converts an annotated set of formulae into a list of strings
     where each string represents one formula of the set and its annotation.
     @param expF A function which converts the formula in integer
@@ -660,7 +663,7 @@ let exportAnnFSet expF abs =
     else ()
   done;
   !res
-
+*)
 
 (** Initialises the global fields of this module
     with the exception of the tables.
@@ -678,9 +681,11 @@ let initMisc size bsf bst lEX nrEX nrAX =
   bssize := (size - 1) / bsintsize + 1;
   assert (!bssize <= Sys.max_array_length);
   bsindex := pred !bssize;
+  (*
   abssize := (size - 1) / annbsintsize + 1;
   assert (!abssize <= Sys.max_array_length);
   absindex := pred !abssize;
+  *)
   bsfalse := bsf;
   bstrue := bst;
   lposEX := lEX;
diff --git a/src/lib/MiscSolver.mli b/src/lib/MiscSolver.mli
index c29bc540958e8bd37bebc4f49df9ba8f1b3f38c9..32fb3816e4ed684ac8e9e0d4eccd8d49c90f8148 100644
--- a/src/lib/MiscSolver.mli
+++ b/src/lib/MiscSolver.mli
@@ -37,6 +37,9 @@ val unionBSNoChk : bitset -> bitset -> bitset
 val iterBS : (int -> unit) -> bitset -> unit
 val foldBS : (int -> 'a -> 'a) -> bitset -> 'a -> 'a
 
+(*
+    Annotated bitsets aren't used anymore and will be removed soon.
+
 type annbitset
 val absNotIn : int
 val absUnAnn : int
@@ -56,14 +59,17 @@ val remABS : annbitset -> int -> unit
 val addABS : annbitset -> int -> bool
 val addBSa : bitset -> annbitset -> int -> bool
 val blitBSa : annbitset -> bitset -> unit
+
+val mkEXListAnn : annbitset -> int list
+val exportAnnFSet : (int -> string) -> annbitset -> string list
+*)
+
 val getPFinclEX : bitset -> int
 val getPFexclEX : bitset -> int
 
 val mkEXList : bitset -> int list
-val mkEXListAnn : annbitset -> int list
 
 val exportAsSet : string -> ('a -> string list) -> 'a -> string
 val exportFSet : (int -> 'a) -> bitset -> 'a list
-val exportAnnFSet : (int -> string) -> annbitset -> string list
 
 val initMisc : int -> int -> int -> int -> int -> int -> unit