Fix for iteration on variables

sat/solver.ml

@@ -698,12 +698,10 @@ module Make (F : Formula_intf.S)
     let nbv = St.nb_vars () in
     let nbc = env.nb_init_clauses + List.length cnf in
     Iheap.grow_to_by_double env.order nbv;
-    List.iter
+    (*
-      (List.iter
+    List.iter (List.iter (fun a -> insert_var_order a.var)) cnf;
-         (fun a ->
+    *)
-            insert_var_order a.var
+    St.iter_vars insert_var_order;
-         )
-      ) cnf;
     Vec.grow_to_by_double env.model nbv;
     Vec.grow_to_by_double env.clauses nbc;
     Vec.grow_to_by_double env.learnts nbc;

sat/solver_types.ml

@@ -93,6 +93,7 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct
 
   let nb_vars () = Vec.size vars
   let get_var i = Vec.get vars i
+  let iter_vars f = Vec.iter f vars
 
   let cpt_mk_var = ref 0
   let make_var =

sat/solver_types_intf.ml

@@ -72,6 +72,7 @@ module type S = sig
 
   val nb_vars : unit -> int
   val get_var : int -> var
+  val iter_vars : (var -> unit) -> unit
   (** Read access to the vector of variables created *)
 
   val fresh_name : unit -> string

util/vec.ml

@@ -125,7 +125,7 @@ let sort t f =
 
 let iter f t =
   for i = 0 to size t - 1 do
-    f (get t i)
+    f t.data.(i)
   done
 
 let fold f acc t =