diff --git a/src/util/array_util.ml b/src/util/array_util.ml
deleted file mode 100644
index 2c3894ee..00000000
--- a/src/util/array_util.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** {1 Utils for Arrays} *)
-
-let exists p a =
-  let n = Array.length a in
-  let rec loop i =
-    if i = n then false
-    else if p (Array.unsafe_get a i) then true
-    else loop (succ i) in
-  loop 0
-
-let for_all p a =
-  let n = Array.length a in
-  let rec loop i =
-    if i = n then true
-    else if p (Array.unsafe_get a i) then loop (succ i)
-    else false in
-  loop 0
diff --git a/src/util/hashcons.ml b/src/util/hashcons.ml
deleted file mode 100644
index 2f2fa7e7..00000000
--- a/src/util/hashcons.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-
-module type ARG = sig
-  type t
-  val equal : t -> t -> bool
-  val hash : t -> int
-  val set_id : t -> int -> unit
-end
-
-module Make(A : ARG): sig
-  val hashcons : A.t -> A.t
-  val iter : (A.t -> unit) -> unit
-end = struct
-  module W = Weak.Make(A)
-
-  let tbl_ = W.create 1024
-  let n_ = ref 0
-
-  (* hashcons terms *)
-  let hashcons t =
-    let t' = W.merge tbl_ t in
-    if t == t' then (
-      incr n_;
-      A.set_id t' !n_;
-    );
-    t'
-
-  let iter yield = W.iter yield tbl_
-end
diff --git a/src/util/sparse_vec.ml b/src/util/sparse_vec.ml
deleted file mode 100644
index 8ca1bb0c..00000000
--- a/src/util/sparse_vec.ml
+++ /dev/null
@@ -1,67 +0,0 @@
-
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** {1 Sparse vector, filled with default value} *)
-
-let _size_too_big()=
-  failwith "Sparse_vec: capacity exceeds maximum array size"
-
-type 'a t = { default : 'a; mutable data : 'a array; mutable sz : int }
-
-let make sz default =
-  if sz > Sys.max_array_length then _size_too_big();
-  { default; sz; data=Array.make sz default; }
-
-let init sz f default =
-  if sz > Sys.max_array_length then _size_too_big();
-  {data = Array.init sz (fun i -> f i); sz ; default}
-
-let length {sz} = sz
-
-let grow_to t new_capa =
-  assert (new_capa >= Array.length t.data);
-  let data = t.data in
-  let capa = Array.length data in
-  t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.default)
-
-let grow_to_by_double t new_capa =
-  if new_capa > Sys.max_array_length then _size_too_big ();
-  let data = t.data in
-  let capa = ref (Array.length data + 1) in
-  while !capa < new_capa do
-    capa := min (2 * !capa) Sys.max_array_length;
-  done;
-  grow_to t !capa
-
-let resize v len =
-  assert (len >= 0);
-  if len <= v.sz
-  then v.sz <- len
-  else (
-    grow_to_by_double v len;
-    v.sz <- len
-  )
-
-let incr v = resize v (v.sz + 1)
-
-let decr v =
-  if v.sz = 0 then invalid_arg "Sparse_vec.decr";
-  resize v (v.sz - 1)
-
-let is_empty {sz} = sz=0
-
-let clear v = v.sz <- 0
-
-let get t i =
-  if i < 0 || i >= t.sz then invalid_arg "Sparse_vec.get";
-  Array.unsafe_get t.data i
-
-let set t i v =
-  if i < 0 || i >= t.sz then invalid_arg "Sparse_vec.set";
-  t.sz <- max t.sz i;
-  Array.unsafe_set t.data i v
-
diff --git a/src/util/sparse_vec.mli b/src/util/sparse_vec.mli
deleted file mode 100644
index f547b792..00000000
--- a/src/util/sparse_vec.mli
+++ /dev/null
@@ -1,45 +0,0 @@
-
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** {1 Sparse vector, filled with default value} *)
-
-type 'a t
-(** Abstract type of sparse vectors of 'a *)
-
-val make : int -> 'a -> 'a t
-(** [make cap default] creates a new vector filled with [default]. The vector's
-    initial length is [cap] *)
-
-val init : int -> (int -> 'a) -> 'a -> 'a t
-(** Same as {!Array.init}, but also with a default element *)
-
-val length : 'a t -> int
-(** Range of valid indices *)
-
-val resize : 'a t -> int -> unit
-(** Set the length of the array to [i] *)
-
-val incr : 'a t -> unit
-(** Increment length size by one *)
-
-val decr : 'a t -> unit
-(** Decrement length by one *)
-
-val is_empty : 'a t -> bool
-(** Check whether length=0 *)
-
-val clear : 'a t -> unit
-(** Set length to 0 *)
-
-val get : 'a t -> int -> 'a
-(** get the element at the given index, or
-    @raise Invalid_argument if the index is not valid *)
-
-val set : 'a t -> int -> 'a -> unit
-(** set the element at the given index, either already set or the first
-    free slot if [not (is_full vec)], or
-    @raise Invalid_argument if the index is not valid *)