diff --git a/common/vec.ml b/common/vec.ml
index 0300bdb3..791f62ea 100644
--- a/common/vec.ml
+++ b/common/vec.ml
@@ -15,9 +15,13 @@ type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
 
 let make capa d = {data = Array.make capa d; sz = 0; dummy = d}
 
+let make_empty d = {data = [||]; sz=0; dummy=d }
+
 let init capa f d = {data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
 
-let from_array data sz d = {data = data; sz = sz; dummy = d}
+let from_array data sz d =
+  assert (sz <= Array.length data);
+  {data = data; sz = sz; dummy = d}
 
 let from_list l sz d =
   let l = ref l in
@@ -28,7 +32,9 @@ let clear s = s.sz <- 0
 
 let shrink t i = assert (i >= 0 && i<=t.sz); t.sz <- t.sz - i
 
-let pop t = assert (t.sz >=1); t.sz <- t.sz - 1
+let pop t =
+  if t.sz = 0 then invalid_arg "vec.pop";
+  t.sz <- t.sz - 1
 
 let size t = t.sz
 
@@ -56,39 +62,25 @@ let push t e =
   t.data.(t.sz) <- e;
   t.sz <- t.sz + 1
 
-let push_none t =
-  if is_full t then grow_to_double_size t;
-  t.data.(t.sz) <- t.dummy;
-  t.sz <- t.sz + 1
-
 let last t =
-  let e = t.data.(t.sz - 1) in
-  assert (not (e == t.dummy));
-  e
+  if t.sz = 0 then invalid_arg "vec.last";
+  t.data.(t.sz - 1)
 
 let get t i =
-  assert (i < t.sz);
-  let e = t.data.(i) in
-  if e == t.dummy then raise Not_found
-  else e
+  if i < 0 || i >= t.sz then invalid_arg "vec.get";
+  Array.unsafe_get t.data i
 
 let set t i v =
-  t.data.(i) <- v;
-  t.sz <- max t.sz (i + 1)
-
-let set_size t sz = t.sz <- sz
+  if i < 0 || i > t.sz then invalid_arg "vec.set";
+  t.sz <- max t.sz (i+1);  (* can set first empty slot *)
+  Array.unsafe_set t.data i v
 
 let copy t =
-  let data = t.data in
-  let len = Array.length data in
-  let data = Array.init len (fun i -> data.(i)) in
-  { data=data; sz=t.sz; dummy = t.dummy }
+  let data = Array.copy t.data in
+  {t with data; }
 
 let move_to t t' =
-  let data = t.data in
-  let len = Array.length data in
-  let data = Array.init len (fun i -> data.(i)) in
-  t'.data <- data;
+  t'.data <- Array.copy t.data;
   t'.sz <- t.sz
 
 
@@ -118,6 +110,15 @@ let iter f t =
     f (get t i)
   done
 
+let fold f acc t =
+  let rec _fold f acc t i =
+    if i=t.sz
+    then acc
+    else
+      let acc' = f acc (Array.unsafe_get t.data i) in
+      _fold f acc' t (i+1)
+  in _fold f acc t 0
+
 (*
 template<class V, class T>
 static inline void remove(V& ts, const T& t)
diff --git a/common/vec.mli b/common/vec.mli
index 8c056b20..d5db6ffb 100644
--- a/common/vec.mli
+++ b/common/vec.mli
@@ -11,29 +11,82 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
+type 'a t
+(** Abstract type of vectors of 'a *)
+
 val make : int -> 'a -> 'a t
+(** [make cap dummy] creates a new vector filled with [dummy]. The vector
+    is initially empty but its underlying array has capacity [cap].
+    [dummy] will stay alive as long as the vector *)
+
+val make_empty : 'a -> 'a t
+(** Vector with an empty capacity. The only argument is the dummy. *)
+
 val init : int -> (int -> 'a) -> 'a -> 'a t
+(** Same as {!Array.init}, but also with a dummy element *)
+
 val from_array : 'a array -> int -> 'a -> 'a t
+(** [from_array arr size dummy] takes ownership of [data] (no copy)
+    to create a vector. [size] is the length of the slice of [data] that is
+    used ([size <= Array.length data] must hold) *)
+
 val from_list : 'a list -> int -> 'a -> 'a t
+
 val clear : 'a t -> unit
+(** Set size to 0, doesn't free elements *)
+
 val shrink : 'a t -> int -> unit
+
 val pop : 'a t -> unit
+(** Pop last element
+    @raise Invalid_argument if the vector is empty *)
+
 val size : 'a t -> int
+
 val is_empty : 'a t -> bool
+
 val grow_to : 'a t -> int -> unit
+
 val grow_to_double_size : 'a t -> unit
+
 val grow_to_by_double : 'a t -> int -> unit
+
 val is_full : 'a t -> bool
+(** Is the capacity of the vector equal to the number of its elements? *)
+
 val push : 'a t -> 'a -> unit
-val push_none : 'a t -> unit
+
 val last : 'a t -> 'a
+(** Last element, or
+    @raise Invalid_argument if the vector is empty *)
+
 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
-val set_size : 'a t -> int -> 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 *)
+
 val copy : 'a t -> 'a t
+(** Fresh copy *)
+
 val move_to : 'a t -> 'a t -> unit
+(** [move_to a b] copies the content of [a] to [b], discarding [b]'s old content *)
+
 val remove : 'a t -> 'a -> unit
+(** Uses [(==)] for comparison *)
+
 val fast_remove : 'a t -> 'a -> unit
+(** Remove element without preserving order (swap with last element) *)
+
 val sort : 'a t -> ('a -> 'a -> int) -> unit
+(** Sort in place the array *)
+
 val iter : ('a -> unit) -> 'a t -> unit
+(** Iterate on elements *)
+
+val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+(** Fold over elements *)
+
diff --git a/sat/solver.ml b/sat/solver.ml
index 1f0092f7..a90a5f87 100644
--- a/sat/solver.ml
+++ b/sat/solver.ml
@@ -160,7 +160,7 @@ module Make (F : Formula_intf.S)
   let var_bump_activity v =
     v.weight <- v.weight +. env.var_inc;
     if v.weight > 1e100 then begin
-      for i = 0 to env.vars.Vec.sz - 1 do
+      for i = 0 to (Vec.size env.vars) - 1 do
         (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100
       done;
       env.var_inc <- env.var_inc *. 1e-100;
@@ -172,7 +172,7 @@ module Make (F : Formula_intf.S)
   let clause_bump_activity c =
     c.activity <- c.activity +. env.clause_inc;
     if c.activity > 1e20 then begin
-      for i = 0 to env.learnts.Vec.sz - 1 do
+      for i = 0 to (Vec.size env.learnts) - 1 do
         (Vec.get env.learnts i).activity <-
           (Vec.get env.learnts i).activity *. 1e-20;
       done;
diff --git a/sat/solver_types.ml b/sat/solver_types.ml
index 22da672d..529028c2 100644
--- a/sat/solver_types.ml
+++ b/sat/solver_types.ml
@@ -63,18 +63,24 @@ module Make (F : Formula_intf.S) = struct
   and dummy_atom =
     { var = dummy_var;
       lit = dummy_lit;
-      watched = {Vec.dummy=dummy_clause; data=[||]; sz=0};
+      watched = Obj.magic 0;
+        (* should be [Vec.make_empty dummy_clause]
+          but we have to break the cycle *)
       neg = dummy_atom;
       is_true = false;
       aid = -102 }
-  and dummy_clause =
+
+  let dummy_clause =
     { name = "";
-      atoms = {Vec.dummy=dummy_atom; data=[||]; sz=0};
+      atoms = Vec.make_empty dummy_atom;
       activity = -1.;
       removed = false;
       learnt = false;
       cpremise = [] }
 
+  let () =
+    dummy_atom.watched <- Vec.make_empty dummy_clause
+
   module MA = Map.Make(F)
   type varmap = var MA.t