diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml
index 07b1ee02..3339175d 100644
--- a/src/backend/Dimacs.ml
+++ b/src/backend/Dimacs.ml
@@ -34,7 +34,7 @@ module Make(St : Solver_types_intf.S) = struct
 
   (* Dimacs & iCNF export *)
   let export_vec name fmt vec =
-    Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.Clause.pp_dimacs) vec
+    Format.fprintf fmt "c %s@,%a@," name (Vec.pp ~sep:"" St.Clause.pp_dimacs) vec
 
   let export_assumption fmt vec =
     Format.fprintf fmt "c Local assumptions@,a %a@," St.Clause.pp_dimacs vec
@@ -66,7 +66,7 @@ module Make(St : Solver_types_intf.S) = struct
       end
 
   let filter_vec learnt =
-    let lemmas = Vec.make (Vec.size learnt) St.Clause.dummy in
+    let lemmas = Vec.create() in
     Vec.iter (fun c ->
         match map_filter_learnt c with
         | None -> ()
diff --git a/src/core/Expr_intf.ml b/src/core/Expr_intf.ml
index 172ab472..4536d36c 100644
--- a/src/core/Expr_intf.ml
+++ b/src/core/Expr_intf.ml
@@ -55,9 +55,6 @@ module type S = sig
     val print : Format.formatter -> t -> unit
     (** Printing function used among other thing for debugging.  *)
 
-    val dummy : t
-    (** Constant formula. A valid formula should never be physically equal to [dummy] *)
-
     val neg : t -> t
     (** Formula negation *)
 
diff --git a/src/core/Formula_intf.ml b/src/core/Formula_intf.ml
index fe45e908..edf8b3ff 100644
--- a/src/core/Formula_intf.ml
+++ b/src/core/Formula_intf.ml
@@ -35,9 +35,6 @@ module type S = sig
   val print : Format.formatter -> t -> unit
   (** Printing function used among other thing for debugging.  *)
 
-  val dummy : t
-  (** Formula constant. A valid formula should never be physically equal to [dummy] *)
-
   val neg : t -> t
   (** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should
       always hold. *)
diff --git a/src/core/Heap.ml b/src/core/Heap.ml
index 1e309ab1..175a4007 100644
--- a/src/core/Heap.ml
+++ b/src/core/Heap.ml
@@ -8,12 +8,12 @@ module Make(Elt : RANKED) = struct
 
   type t = {
     heap : elt Vec.t;
-  }
+  } [@@unboxed]
 
   let _absent_index = -1
 
   let create () =
-    { heap = Vec.make_empty Elt.dummy; }
+    { heap = Vec.create(); }
 
   let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
   let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
@@ -109,9 +109,6 @@ module Make(Elt : RANKED) = struct
       percolate_up s elt;
     )
 
-  let[@inline] grow_to_at_least s sz =
-    Vec.grow_to_at_least s.heap sz
-
   (*
   let update cmp s n =
     assert (heap_property cmp s);
@@ -130,10 +127,9 @@ module Make(Elt : RANKED) = struct
     if Vec.size heap=0 then raise Not_found;
     let x = Vec.get heap 0 in
     Elt.set_idx x _absent_index;
-    let new_hd = Vec.last heap in (* heap.last() *)
+    let new_hd = Vec.pop heap in (* new head *)
     Vec.set heap 0 new_hd;
     Elt.set_idx new_hd 0;
-    Vec.pop heap; (* remove last *)
     (* enforce heap property again *)
     if Vec.size heap > 1 then (
       percolate_down s new_hd;
diff --git a/src/core/Heap_intf.ml b/src/core/Heap_intf.ml
index a5d11100..bee623e6 100644
--- a/src/core/Heap_intf.ml
+++ b/src/core/Heap_intf.ml
@@ -3,7 +3,6 @@ module type RANKED = sig
   type t
   val idx: t -> int (** Index in heap. return -1 if never set *)
   val set_idx : t -> int -> unit (** Update index in heap *)
-  val dummy : t
   val cmp : t -> t -> bool
 end
 
@@ -36,10 +35,6 @@ module type S = sig
   val insert : t -> elt -> unit
   (** Insert a new element into the heap *)
 
-  val grow_to_at_least: t -> int -> unit
-  (** Hint: augment the internal capacity of the heap until it reaches at
-      least the given integer *)
-
   (*val update : (int -> int -> bool) -> t -> int -> unit*)
 
   val remove_min : t -> elt
diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index a613820a..2fcf5645 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -17,7 +17,6 @@ module Make
   module H = Heap.Make(struct
     type t = St.Elt.t
     let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *)
-    let dummy = Elt.of_var St.Var.dummy
     let idx = Elt.idx
     let set_idx = Elt.set_idx
   end)
@@ -122,14 +121,14 @@ module Make
   }
 
   (* Starting environment. *)
-  let create_ ~st ~size_trail ~size_lvl () : t = {
+  let create_ ~st () : t = {
     st;
     unsat_conflict = None;
     next_decision = None;
 
-    clauses_hyps = Vec.make 0 Clause.dummy;
-    clauses_learnt = Vec.make 0 Clause.dummy;
-    clauses_temp = Vec.make 0 Clause.dummy;
+    clauses_hyps = Vec.create();
+    clauses_learnt = Vec.create();
+    clauses_temp = Vec.create();
 
     clauses_root = Stack.create ();
     clauses_to_add = Stack.create ();
@@ -137,10 +136,10 @@ module Make
     th_head = 0;
     elt_head = 0;
 
-    trail = Vec.make size_trail (Trail_elt.of_atom Atom.dummy);
-    elt_levels = Vec.make size_lvl (-1);
-    th_levels = Vec.make size_lvl Plugin.dummy;
-    user_levels = Vec.make 0 (-1);
+    trail = Vec.create ();
+    elt_levels = Vec.create();
+    th_levels = Vec.create();
+    user_levels = Vec.create();
 
     order = H.create();
 
@@ -153,13 +152,9 @@ module Make
     dirty=false;
   }
 
-  let create ?(size=`Big) ?st () : t =
-    let st = match st with Some s -> s | None -> St.create ~size () in
-    let size_trail, size_lvl = match size with
-      | `Tiny -> 0, 0
-      | `Small -> 32, 16
-      | `Big -> 600, 50
-    in create_ ~st ~size_trail ~size_lvl ()
+  let create ?(size=`Big) () : t =
+    let st = St.create ~size () in
+    create_ ~st ()
 
   (* Misc functions *)
   let to_float = float_of_int
@@ -504,8 +499,8 @@ module Make
           Log.debugf error
             (fun k ->
                k "@[<v 2>Failed at reason simplification:@,%a@,%a@]"
-                 (Vec.print ~sep:"" Atom.debug)
-                 (Vec.from_list l Atom.dummy)
+                 (Vec.pp ~sep:"" Atom.debug)
+                 (Vec.of_list l)
                  Clause.debug cl);
           assert false
       end
@@ -537,7 +532,6 @@ module Make
       let l = List.map (Lit.make st.st) terms in
       let lvl = List.fold_left (fun acc {l_level; _} ->
           assert (l_level > 0); max acc l_level) 0 l in
-      H.grow_to_at_least st.order (St.nb_elt st.st);
       enqueue_bool st a ~level:lvl Semantic
     )
 
@@ -864,8 +858,6 @@ module Make
 
   let flush_clauses st =
     if not (Stack.is_empty st.clauses_to_add) then (
-      let nbv = St.nb_elt st.st in
-      H.grow_to_at_least st.order nbv;
       while not (Stack.is_empty st.clauses_to_add) do
         let c = Stack.pop st.clauses_to_add in
         add_clause st c
@@ -986,7 +978,6 @@ module Make
         else if p.neg.is_true then (
           Stack.push c st.clauses_to_add
         ) else (
-          H.grow_to_at_least st.order (St.nb_elt st.st);
           insert_subterms_order st p.var;
           let level = List.fold_left (fun acc a -> max acc a.var.v_level) 0 l in
           enqueue_bool st p ~level (Bcp c)
@@ -1033,7 +1024,6 @@ module Make
         if not @@ List.for_all (fun a -> a.neg.is_true) l then (
           raise (Invalid_argument "msat:core/internal: invalid conflict");
         );
-        H.grow_to_at_least st.order (St.nb_elt st.st);
         List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l;
         (* Create the clause and return it. *)
         let c = St.Clause.make l (Lemma p) in
@@ -1215,14 +1205,14 @@ module Make
       cancel_until st (base_level st);
       Log.debugf debug
         (fun k -> k "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]"
-            st.elt_head st.th_head (Vec.print ~sep:"" Trail_elt.debug) st.trail);
+            st.elt_head st.th_head (Vec.pp ~sep:"" Trail_elt.debug) st.trail);
       begin match propagate st with
         | Some confl ->
           report_unsat st confl
         | None ->
           Log.debugf debug
             (fun k -> k "@[<v>Current trail:@,@[<hov>%a@]@]"
-                (Vec.print ~sep:"" Trail_elt.debug) st.trail);
+                (Vec.pp ~sep:"" Trail_elt.debug) st.trail);
           Log.debug info "Creating new user level";
           new_decision_level st;
           Vec.push st.user_levels (Vec.size st.clauses_temp);
@@ -1237,8 +1227,7 @@ module Make
       Log.debug info "Popping user level";
       assert (base_level st > 0);
       st.unsat_conflict <- None;
-      let n = Vec.last st.user_levels in
-      Vec.pop st.user_levels; (* before the [cancel_until]! *)
+      let n = Vec.pop st.user_levels in (* before the [cancel_until]! *)
       (* Add the root clauses to the clauses to add *)
       Stack.iter (fun c -> Stack.push c st.clauses_to_add) st.clauses_root;
       Stack.clear st.clauses_root;
@@ -1263,9 +1252,6 @@ module Make
           (* conflict between assumptions: UNSAT *)
           report_unsat st c;
         ) else (
-          (* Grow the heap, because when the lit is backtracked,
-             it will be added to the heap. *)
-          H.grow_to_at_least st.order (St.nb_elt st.st);
           (* make a decision, propagate *)
           let level = decision_level st in
           enqueue_bool st a ~level (Bcp c);
diff --git a/src/core/Solver.ml b/src/core/Solver.ml
index 883636f0..bc55b0af 100644
--- a/src/core/Solver.ml
+++ b/src/core/Solver.ml
@@ -31,7 +31,7 @@ module Make
   type t = S.t
   type solver = t
 
-  let[@inline] create ?size () = S.create ?size ()
+  let create = S.create
 
   (* Result type *)
   type res =
@@ -44,10 +44,10 @@ module Make
           "@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,\
            @[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,@]@."
           status
-          (Vec.print ~sep:"" St.Trail_elt.debug) (S.trail st)
-          (Vec.print ~sep:"" St.Clause.debug) (S.temp st)
-          (Vec.print ~sep:"" St.Clause.debug) (S.hyps st)
-          (Vec.print ~sep:"" St.Clause.debug) (S.history st)
+          (Vec.pp ~sep:"" St.Trail_elt.debug) (S.trail st)
+          (Vec.pp ~sep:"" St.Clause.debug) (S.temp st)
+          (Vec.pp ~sep:"" St.Clause.debug) (S.hyps st)
+          (Vec.pp ~sep:"" St.Clause.debug) (S.history st)
       )
 
   let mk_sat (st:S.t) : (_,_) sat_state =
diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml
index add513cf..9f3a4f2d 100644
--- a/src/core/Solver_types.ml
+++ b/src/core/Solver_types.ml
@@ -24,8 +24,6 @@ module McMake (E : Expr_intf.S) = struct
   type formula = E.Formula.t
   type proof = E.proof
 
-  let pp_form = E.Formula.dummy
-
   type seen =
     | Nope
     | Both
@@ -91,37 +89,6 @@ module McMake (E : Expr_intf.S) = struct
     | Lit of lit
     | Atom of atom
 
-  let rec dummy_var =
-    { vid = -101;
-      pa = dummy_atom;
-      na = dummy_atom;
-      v_fields = Var_fields.empty;
-      v_level = -1;
-      v_weight = -1.;
-      v_idx= -1;
-      v_assignable = None;
-      reason = None;
-    }
-  and dummy_atom =
-    { var = dummy_var;
-      lit = E.Formula.dummy;
-      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 }
-  let dummy_clause =
-    { name = -1;
-      tag = None;
-      atoms = [| |];
-      activity = -1.;
-      attached = false;
-      visited = false;
-      cpremise = History [] }
-
-  let () = dummy_atom.watched <- Vec.make_empty dummy_clause
-
   (* Constructors *)
   module MF = Hashtbl.Make(E.Formula)
   module MT = Hashtbl.Make(E.Term)
@@ -136,21 +103,21 @@ module McMake (E : Expr_intf.S) = struct
 
   type state = t
 
-  let create_ size_map size_vars () : t = {
+  let create_ size_map () : t = {
     f_map = MF.create size_map;
     t_map = MT.create size_map;
-    vars = Vec.make size_vars (E_var dummy_var);
+    vars = Vec.create();
     cpt_mk_var = 0;
     cpt_mk_clause = 0;
   }
 
   let create ?(size=`Big) () : t =
-    let size_map, size_vars = match size with
-      | `Tiny -> 8, 0
-      | `Small -> 16, 10
-      | `Big -> 4096, 128
+    let size_map = match size with
+      | `Tiny -> 8
+      | `Small -> 16
+      | `Big -> 4096
     in
-    create_ size_map size_vars ()
+    create_ size_map ()
 
   let nb_elt st = Vec.size st.vars
   let get_elt st i = Vec.get st.vars i
@@ -200,7 +167,6 @@ module McMake (E : Expr_intf.S) = struct
 
   module Var = struct
     type t = var
-    let dummy = dummy_var
     let[@inline] level v = v.v_level
     let[@inline] pos v = v.pa
     let[@inline] neg v = v.na
@@ -228,14 +194,14 @@ module McMake (E : Expr_intf.S) = struct
         and pa =
           { var = var;
             lit = lit;
-            watched = Vec.make 10 dummy_clause;
+            watched = Vec.create();
             neg = na;
             is_true = false;
             aid = cpt_double (* aid = vid*2 *) }
         and na =
           { var = var;
             lit = E.Formula.neg lit;
-            watched = Vec.make 10 dummy_clause;
+            watched = Vec.create();
             neg = pa;
             is_true = false;
             aid = cpt_double + 1 (* aid = vid*2+1 *) } in
@@ -255,7 +221,6 @@ module McMake (E : Expr_intf.S) = struct
 
   module Atom = struct
     type t = atom
-    let dummy = dummy_atom
     let[@inline] level a = a.var.v_level
     let[@inline] var a = a.var
     let[@inline] neg a = a.neg
@@ -370,7 +335,6 @@ module McMake (E : Expr_intf.S) = struct
 
   module Clause = struct
     type t = clause
-    let dummy = dummy_clause
 
     let make =
       let n = ref 0 in
diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml
index 4a1816be..61d1727a 100644
--- a/src/core/Solver_types_intf.ml
+++ b/src/core/Solver_types_intf.ml
@@ -156,7 +156,6 @@ module type S = sig
 
   module Var : sig
     type t = var
-    val dummy : t
 
     val pos : t -> atom
     val neg : t -> atom
@@ -180,7 +179,6 @@ module type S = sig
 
   module Atom : sig
     type t = atom
-    val dummy : t
     val level : t -> int
     val reason : t -> reason option
     val lit : t -> formula
@@ -227,7 +225,6 @@ module type S = sig
 
   module Clause : sig
     type t = clause
-    val dummy : t
 
     val name : t -> string
     val equal : t -> t -> bool
diff --git a/src/core/Theory_intf.ml b/src/core/Theory_intf.ml
index 7a6621d8..1cb7e672 100644
--- a/src/core/Theory_intf.ml
+++ b/src/core/Theory_intf.ml
@@ -49,9 +49,6 @@ module type S = sig
   type level
   (** The type for levels to allow backtracking. *)
 
-  val dummy : level
-  (** A dummy level. *)
-
   val current_level : unit -> level
   (** Return the current level of the theory (either the empty/beginning state, or the
       last level returned by the [assume] function). *)
@@ -76,7 +73,6 @@ module Dummy(F: Formula_intf.S)
   type formula = F.t
   type proof = unit
   type level = unit
-  let dummy = ()
   let current_level () = ()
   let assume _ = Sat
   let if_sat _ = Sat
diff --git a/src/core/Vec.ml b/src/core/Vec.ml
index c8c68f84..6223dfd9 100644
--- a/src/core/Vec.ml
+++ b/src/core/Vec.ml
@@ -1,49 +1,12 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 
 type 'a t = {
-  mutable dummy: 'a;
   mutable data : 'a array;
   mutable sz : int;
 }
 
-let _size_too_big()=
-  failwith "Vec: capacity exceeds maximum array size"
+let make n x = {data=Array.make n x; sz=0}
 
-let make capa d =
-  if capa > Sys.max_array_length then _size_too_big();
-  {data = Array.make capa d; sz = 0; dummy = d}
-
-let[@inline] make_empty d = {data = [||]; sz=0; dummy=d }
-
-let init capa f d =
-  if capa > Sys.max_array_length then _size_too_big();
-  {data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
-
-let from_array data sz d =
-  assert (sz <= Array.length data);
-  {data = data; sz = sz; dummy = d}
-
-let from_list l d =
-  let a = Array.of_list l in
-  from_array a (Array.length a) d
-
-let to_list s =
-  let l = ref [] in
-  for i = 0 to s.sz - 1 do
-    l := s.data.(i) :: !l
-  done;
-  List.rev !l
+let[@inline] create () = {data = [||]; sz = 0}
 
 let[@inline] clear s = s.sz <- 0
 
@@ -54,159 +17,96 @@ let[@inline] shrink t i =
 
 let[@inline] pop t =
   if t.sz = 0 then invalid_arg "vec.pop";
-  t.sz <- t.sz - 1
+  let x = Array.unsafe_get t.data (t.sz - 1) in
+  t.sz <- t.sz - 1;
+  x
 
 let[@inline] size t = t.sz
 
 let[@inline] is_empty t = t.sz = 0
 
-let grow_to_exact t new_capa =
-  assert (new_capa > Array.length t.data);
-  let new_data = Array.make new_capa t.dummy in
-  assert (t.sz <= new_capa);
-  Array.blit t.data 0 new_data 0 t.sz;
-  t.data <- new_data
-
-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 + 1) in
-  grow_to_exact t size
-
-let grow_to_at_least t new_capa =
-  assert (new_capa >= 0);
-  if new_capa > Sys.max_array_length then _size_too_big ();
-  let data = t.data in
-  let capa = ref (max (Array.length data) 1) in
-  while !capa < new_capa do
-    capa := min (2 * !capa + 1) Sys.max_array_length;
-  done;
-  if !capa > Array.length data then (
-    grow_to_exact t !capa
-  )
-
 let[@inline] is_full t = Array.length t.data = t.sz
 
-let[@inline] push t e =
-  if is_full t then grow_to_double_size t;
-  t.data.(t.sz) <- e;
+let[@inline] copy t : _ t =
+  let data = Array.copy t.data in
+  {t with data}
+
+(* grow the array *)
+let[@inline never] grow_to_double_size t x : unit =
+  if Array.length t.data = Sys.max_array_length then (
+    failwith "vec: cannot resize";
+  );
+  let size =
+    min Sys.max_array_length (max 4 (2 * Array.length t.data))
+  in
+  let arr' = Array.make size x in
+  Array.blit t.data 0 arr' 0 (Array.length t.data);
+  t.data <- arr';
+  assert (Array.length t.data > t.sz);
+  ()
+
+let[@inline] push t x : unit =
+  if is_full t then grow_to_double_size t x;
+  Array.unsafe_set t.data t.sz x;
   t.sz <- t.sz + 1
 
-let[@inline] last t =
-  if t.sz = 0 then invalid_arg "vec.last";
-  t.data.(t.sz - 1)
-
-let[@inline] pop_last t =
-  if t.sz = 0 then invalid_arg "vec.pop_last";
-  let x = t.data.(t.sz - 1) in
-  t.sz <- t.sz - 1;
-  x
-
 let[@inline] get t i =
   if i < 0 || i >= t.sz then invalid_arg "vec.get";
   Array.unsafe_get t.data i
 
 let[@inline] set t i v =
   if i < 0 || i > t.sz then invalid_arg "vec.set";
-  if i = t.sz then
+  if i = t.sz then (
     push t v
-  else
+  ) else (
     Array.unsafe_set t.data i v
-
-let[@inline] copy t =
-  let data = Array.copy t.data in
-  {t with data; }
-
-let[@inline] move_to t t' =
-  t'.data <- Array.copy t.data;
-  t'.sz <- t.sz
-
-let remove t e =
-  let j = ref 0 in
-  while (!j < t.sz && not (t.data.(!j) == e)) do incr j done;
-  assert (!j < t.sz);
-  for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done;
-  pop t
+  )
 
 let[@inline] fast_remove t i =
-  assert (i < t.sz);
-  t.data.(i) <- t.data.(t.sz - 1);
+  assert (i>= 0 && i < t.sz);
+  Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1);
   t.sz <- t.sz - 1
 
 let filter_in_place f vec =
   let i = ref 0 in
   while !i < size vec do
-    if f (get vec !i) then incr i else fast_remove vec !i
+    if f (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i
   done
 
-let sort t f =
-  let sub_arr = Array.sub t.data 0 t.sz in
+let sort t f : unit =
+  let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in
   Array.fast_sort f sub_arr;
   t.data <- sub_arr
 
-let iter f t =
+let[@inline] iter f t =
   for i = 0 to size t - 1 do
     f (Array.unsafe_get t.data i)
   done
 
-let append a b =
-  grow_to_at_least a (size a + size b);
-  iter (push a) b
+let[@inline] iteri f t =
+  for i = 0 to size t - 1 do
+    f i (Array.unsafe_get t.data 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
+let[@inline] to_seq a k = iter k a
 
-exception ExitVec
+let exists p t = Sequence.exists p @@ to_seq t
+let for_all p t = Sequence.for_all p @@ to_seq t
+let fold f acc a = Sequence.fold f acc @@ to_seq a
+let to_list a = Sequence.to_list @@ to_seq a
 
-let exists p t =
-  try
-    for i = 0 to t.sz - 1 do
-      if p (Array.unsafe_get t.data i) then raise ExitVec
-    done;
-    false
-  with ExitVec -> true
+let of_list l : _ t =
+  match l with
+  | [] -> create()
+  | x :: tl ->
+    let v = make (List.length tl+1) x in
+    List.iter (push v) l;
+    v
 
-let for_all p t =
-  try
-    for i = 0 to t.sz - 1 do
-      if not (p (Array.unsafe_get t.data i)) then raise ExitVec
-    done;
-    true
-  with ExitVec -> false
-
-let print ?(sep=", ") pp out v =
+let pp ?(sep=", ") pp out v =
   let first = ref true in
   iter
     (fun x ->
        if !first then first := false else Format.fprintf out "%s@," sep;
        pp out x)
     v
-
-(*
-template<class V, class T>
-static inline void remove(V& ts, const T& t)
-{
-    int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
-    assert(j < ts.size());
-    ts[j] = ts.last();
-    ts.pop();
-}
-#endif
-
-template<class V, class T>
-static inline bool find(V& ts, const T& t)
-{
-    int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
-    return j < ts.size();
-}
-
-#endif
-*)
diff --git a/src/core/Vec.mli b/src/core/Vec.mli
index 914d4eba..b35e0f04 100644
--- a/src/core/Vec.mli
+++ b/src/core/Vec.mli
@@ -1,15 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 
 type 'a t
 (** Abstract type of vectors of 'a *)
@@ -19,22 +7,15 @@ val make : int -> 'a -> 'a t
     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 -> 'a -> 'a t
+val create : unit -> 'a t
 
 val to_list : 'a t -> 'a list
 (** Returns the list of elements of the vector *)
 
+val of_list : 'a list -> 'a t
+
+val to_seq : 'a t -> 'a Sequence.t
+
 val clear : 'a t -> unit
 (** Set size to 0, doesn't free elements *)
 
@@ -42,37 +23,19 @@ val shrink : 'a t -> int -> unit
 (** [shrink vec sz] resets size of [vec] to [sz].
     Assumes [sz >=0 && sz <= size vec] *)
 
-val pop : 'a t -> unit
-(** Pop last element
+val pop : 'a t -> 'a
+(** Pop last element and return it.
     @raise Invalid_argument if the vector is empty *)
 
 val size : 'a t -> int
 
 val is_empty : 'a t -> bool
 
-val grow_to_exact : 'a t -> int -> unit
-
-val grow_to_double_size : 'a t -> unit
-
-val grow_to_at_least : 'a t -> int -> unit
-(** [grow_to_at_least vec n] ensures that [capacity vec >= n] in
-    the most efficient way *)
-
 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 append : 'a t -> 'a t -> unit
-(** [append v1 v2] pushes all elements of [v2] into [v1] *)
-
-val last : 'a t -> 'a
-(** Last element, or
-    @raise Invalid_argument if the vector is empty *)
-
-val pop_last : 'a t -> 'a
-(** Combine {!last} and {!pop}: remove last element and return it
-    @raise Invalid_argument if empty *)
+(** Push element into the vector *)
 
 val get : 'a t -> int -> 'a
 (** get the element at the given index, or
@@ -86,12 +49,6 @@ val set : 'a t -> int -> 'a -> unit
 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 -> int -> unit
 (** Remove element at index [i] without preserving order
     (swap with last element) *)
@@ -106,6 +63,9 @@ val sort : 'a t -> ('a -> 'a -> int) -> unit
 val iter : ('a -> unit) -> 'a t -> unit
 (** Iterate on elements *)
 
+val iteri : (int -> 'a -> unit) -> 'a t -> unit
+(** Iterate on elements with their index *)
+
 val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
 (** Fold over elements *)
 
@@ -115,7 +75,7 @@ val exists : ('a -> bool) -> 'a t -> bool
 val for_all : ('a -> bool) -> 'a t -> bool
 (** Do all elements satisfy the predicate? *)
 
-val print :
+val pp :
   ?sep:string ->
   (Format.formatter -> 'a -> unit) ->
   Format.formatter -> 'a t -> unit
diff --git a/src/core/dune b/src/core/dune
index c72f5475..e5c561a3 100644
--- a/src/core/dune
+++ b/src/core/dune
@@ -2,6 +2,7 @@
 (library
   (name msat)
   (public_name msat)
+  (libraries sequence)
   (synopsis "core data structures and algorithms for msat")
   (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
   (ocamlopt_flags :standard -O3 -bin-annot
diff --git a/src/sat/Expr_sat.ml b/src/sat/Expr_sat.ml
index efb92778..86fc6242 100644
--- a/src/sat/Expr_sat.ml
+++ b/src/sat/Expr_sat.ml
@@ -26,9 +26,6 @@ let _make i =
   end else
     raise Bad_atom
 
-(** A dummy atom *)
-let dummy = 0
-
 (** *)
 let neg a = - a