diff --git a/util/iheap.ml b/util/iheap.ml
index 9829ff4c..f09df933 100644
--- a/util/iheap.ml
+++ b/util/iheap.ml
@@ -11,13 +11,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t = {heap : int Vec.t; indices : int Vec.t }
+module V = Sparse_vec
 
-let dummy = 0
+type t = {heap : int Vec.t; indices : int V.t }
+
+let _absent_index = -1
 
 let init sz =
-  { heap    =  Vec.init sz (fun i -> i) dummy;
-    indices =  Vec.init sz (fun i -> i) dummy}
+  { heap    =  Vec.init sz (fun i -> i) 0;
+    indices =  V.init sz (fun i -> i) _absent_index}
 
 let left i   = (i lsl 1) + 1 (* i*2 + 1 *)
 let right i  = (i + 1) lsl 1 (* (i+1)*2 *)
@@ -38,12 +40,12 @@ let percolate_up cmp {heap=heap;indices=indices} i =
   let i = ref i in
   while !i <> 0 && cmp x (Vec.get heap !pi) do
     Vec.set heap !i (Vec.get heap !pi);
-    Vec.set indices (Vec.get heap !i) !i;
+    V.set indices (Vec.get heap !i) !i;
     i  := !pi;
     pi := parent !i
   done;
   Vec.set heap !i x;
-  Vec.set indices x !i
+  V.set indices x !i
 
 let percolate_down cmp {heap=heap;indices=indices} i =
   let x = Vec.get heap i in
@@ -59,22 +61,22 @@ let percolate_down cmp {heap=heap;indices=indices} i =
        in
        if not (cmp (Vec.get heap child) x) then raise Exit;
        Vec.set heap !i (Vec.get heap child);
-       Vec.set indices (Vec.get heap !i) !i;
+       V.set indices (Vec.get heap !i) !i;
        i  := child;
        li := left !i;
        ri := right !i
      done;
    with Exit -> ());
   Vec.set heap !i x;
-  Vec.set indices x !i
+  V.set indices x !i
 
-let in_heap s n = n < Vec.size s.indices && Vec.get s.indices n >= 0
+let in_heap s n = n < V.length s.indices && V.get s.indices n >= 0
 
 let decrease cmp s n =
-  assert (in_heap s n); percolate_up cmp s (Vec.get s.indices n)
+  assert (in_heap s n); percolate_up cmp s (V.get s.indices n)
 
 let increase cmp s n =
-  assert (in_heap s n); percolate_down cmp s (Vec.get s.indices n)
+  assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
 
 let filter s filt cmp =
   let j = ref 0 in
@@ -82,10 +84,10 @@ let filter s filt cmp =
   for i = 0 to lim - 1 do
     if filt (Vec.get s.heap i) then begin
       Vec.set s.heap !j (Vec.get s.heap i);
-      Vec.set s.indices (Vec.get s.heap i) !j;
+      V.set s.indices (Vec.get s.heap i) !j;
       incr j;
     end
-    else Vec.set s.indices (Vec.get s.heap i) (-1);
+    else V.set s.indices (Vec.get s.heap i) _absent_index;
   done;
   Vec.shrink s.heap (lim - !j);
   for i = (lim / 2) - 1 downto 0 do
@@ -98,19 +100,19 @@ let is_empty s = Vec.is_empty s.heap
 
 let clear {heap; indices} =
   Vec.clear heap;
-  Vec.clear indices;
+  V.clear indices;
   ()
 
 let insert cmp s n =
   if not (in_heap s n) then
     begin
-      Vec.set_unsafe s.indices n (Vec.size s.heap);
+      V.set s.indices n (Vec.size s.heap);
       Vec.push s.heap n;
-      percolate_up cmp s (Vec.get s.indices n)
+      percolate_up cmp s (V.get s.indices n)
     end
 
 let grow_to_by_double s sz =
-  Vec.grow_to_by_double s.indices sz;
+  V.resize s.indices sz;
   Vec.grow_to_by_double s.heap sz
 
 (*
@@ -131,8 +133,8 @@ let remove_min cmp ({heap=heap; indices=indices} as s) =
   if Vec.size heap=0 then raise Not_found;
   let x = Vec.get heap 0 in
   Vec.set heap 0 (Vec.last heap); (*heap.last()*)
-  Vec.set indices (Vec.get heap 0) 0;
-  Vec.set indices x (-1);
+  V.set indices (Vec.get heap 0) 0;
+  V.set indices x (-1);
   Vec.pop s.heap;
   if Vec.size s.heap > 1 then percolate_down cmp s 0;
   x
diff --git a/util/iheap.mli b/util/iheap.mli
index 0c5ace86..c2825e41 100644
--- a/util/iheap.mli
+++ b/util/iheap.mli
@@ -41,7 +41,7 @@ val insert : (int -> int -> bool) -> t -> int -> unit
 (** Insert a new integer into the heap, according to the given comparison *)
 
 val grow_to_by_double: t -> int -> unit
-(** Augment the internal capacity of the heap until it reaches at
+(** Hint: augment the internal capacity of the heap until it reaches at
     least the given integer *)
 
 (*val update : (int -> int -> bool) -> t -> int -> unit*)
diff --git a/util/sparse_vec.ml b/util/sparse_vec.ml
new file mode 100644
index 00000000..35f20fca
--- /dev/null
+++ b/util/sparse_vec.ml
@@ -0,0 +1,71 @@
+
+(*
+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 =
+  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_double_size t =
+  if Array.length t.data = Sys.max_array_length then _size_too_big();
+  let size = min Sys.max_array_length (2* Array.length t.data) in
+  grow_to t size
+
+let rec 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/util/sparse_vec.mli b/util/sparse_vec.mli
new file mode 100644
index 00000000..f547b792
--- /dev/null
+++ b/util/sparse_vec.mli
@@ -0,0 +1,45 @@
+
+(*
+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 *)
diff --git a/util/vec.mli b/util/vec.mli
index daab5626..95846e2d 100644
--- a/util/vec.mli
+++ b/util/vec.mli
@@ -70,6 +70,7 @@ val set : 'a t -> int -> 'a -> unit
     @raise Invalid_argument if the index is not valid *)
 
 val set_unsafe : 'a t -> int -> 'a -> unit
+(* undocumented. TODO remove asap *)
 
 val copy : 'a t -> 'a t
 (** Fresh copy *)