diff --git a/sat/solver.ml b/sat/solver.ml
index a8a8b473..26729ebf 100644
--- a/sat/solver.ml
+++ b/sat/solver.ml
@@ -463,15 +463,16 @@ module Make (F : Formula_intf.S)
   (* returns true if the clause is used as a reason for a propagation,
       and therefore can be needed in case of conflict. In this case
       the clause can't be forgotten *)
-  let locked c =
+  let locked c = false (*
     Vec.exists
       (fun v -> match v.reason with
          | Some c' -> c ==c'
          | _ -> false
       ) env.vars
+      *)
 
   (* remove some learnt clauses *)
-  let reduce_db () =
+  let reduce_db () = () (*
     let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in
     Vec.sort env.learnts f_sort_db;
     let lim2 = Vec.size env.learnts in
@@ -492,6 +493,7 @@ module Make (F : Formula_intf.S)
         begin Vec.set env.learnts !j c; incr j end
     done;
     Vec.shrink env.learnts (lim2 - !j)
+    *)
 
   (* remove from [vec] the clauses that are satisfied in the current trail *)
   let remove_satisfied vec =
@@ -879,14 +881,13 @@ module Make (F : Formula_intf.S)
       None -> () | Some dep -> report_t_unsat dep
 
   let init_solver cnf ~cnumber =
-    let nbv, _ = made_vars_info () in
+    let nbv = made_vars_info env.vars in
     let nbc = env.nb_init_clauses + List.length cnf in
     Vec.grow_to_by_double env.vars nbv;
     Iheap.grow_to_by_double env.order nbv;
     List.iter
       (List.iter
          (fun a ->
-            Vec.set env.vars a.var.vid a.var;
             insert_var_order a.var
          )
       ) cnf;
@@ -899,7 +900,7 @@ module Make (F : Formula_intf.S)
 
 
   let assume cnf ~cnumber =
-    let cnf = List.map (List.map St.add_atom) cnf in
+    let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
     init_solver cnf ~cnumber
 
   let eval lit =
diff --git a/sat/solver_types.ml b/sat/solver_types.ml
index f33f5e2f..ba810c41 100644
--- a/sat/solver_types.ml
+++ b/sat/solver_types.ml
@@ -122,7 +122,10 @@ module Make (F : Formula_intf.S) = struct
         incr cpt_mk_var;
         var, negated
 
-  let made_vars_info () = !cpt_mk_var, MA.fold (fun lit var acc -> var::acc)!ma []
+  let made_vars_info vars =
+      Vec.grow_to_by_double vars !cpt_mk_var;
+      MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma;
+      !cpt_mk_var
 
   let add_atom lit =
     let var, negated = make_var lit in
diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml
index a6d28128..6f2b2fc3 100644
--- a/sat/solver_types_intf.ml
+++ b/sat/solver_types_intf.ml
@@ -72,7 +72,7 @@ module type S = sig
   val to_float : int -> float
 
   val to_int : float -> int
-  val made_vars_info : unit -> int * var list
+  val made_vars_info : var Vec.t -> int
   val clear : unit -> unit
 
   val pp_atom : Buffer.t -> atom -> unit
diff --git a/util/iheap.ml b/util/iheap.ml
index 228e78eb..9829ff4c 100644
--- a/util/iheap.ml
+++ b/util/iheap.ml
@@ -104,7 +104,7 @@ let clear {heap; indices} =
 let insert cmp s n =
   if not (in_heap s n) then
     begin
-      Vec.set s.indices n (Vec.size s.heap);
+      Vec.set_unsafe s.indices n (Vec.size s.heap);
       Vec.push s.heap n;
       percolate_up cmp s (Vec.get s.indices n)
     end
diff --git a/util/sat_solve.ml b/util/sat_solve.ml
index 426a7e5b..27ee05d9 100644
--- a/util/sat_solve.ml
+++ b/util/sat_solve.ml
@@ -64,7 +64,7 @@ let check () =
 
 (* Entry file parsing *)
 let get_cnf () =
-  List.map (List.map S.make) (Parser.parse !file)
+  List.rev_map (List.rev_map S.make) (Parser.parse !file)
 
 let print_cnf cnf =
   Format.printf "CNF :@\n";
diff --git a/util/vec.ml b/util/vec.ml
index 5738d626..7930216e 100644
--- a/util/vec.ml
+++ b/util/vec.ml
@@ -13,11 +13,18 @@
 
 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 _size_too_big()=
+    failwith "Vec: capacity exceeds maximum array size"
+
+let make capa d =
+    if capa > Sys.max_array_length then _size_too_big();
+    {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 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);
@@ -45,12 +52,18 @@ let grow_to t new_capa =
   let capa = Array.length data in
   t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy)
 
-let grow_to_double_size t = grow_to t (2* Array.length t.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) 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 := 2 * !capa done;
+  while !capa < new_capa do
+      capa := min (2 * !capa) Sys.max_array_length;
+  done;
   grow_to t !capa
 
 
@@ -75,6 +88,11 @@ let set t i v =
   t.sz <- max t.sz (i+1);  (* can set first empty slot *)
   Array.unsafe_set t.data i v
 
+let set_unsafe t i v =
+  if i < 0 || i >= Array.length t.data then invalid_arg "vec.set_unsafe";
+  t.sz <- max t.sz (i+1);
+  Array.unsafe_set t.data i v
+
 let copy t =
   let data = Array.copy t.data in
   {t with data; }
diff --git a/util/vec.mli b/util/vec.mli
index bc990b7f..daab5626 100644
--- a/util/vec.mli
+++ b/util/vec.mli
@@ -69,6 +69,8 @@ val set : 'a t -> int -> 'a -> unit
     free slot if [not (is_full vec)], or
     @raise Invalid_argument if the index is not valid *)
 
+val set_unsafe : 'a t -> int -> 'a -> unit
+
 val copy : 'a t -> 'a t
 (** Fresh copy *)