diff --git a/sat/res.ml b/sat/res.ml
index b2230aa2..159cd731 100644
--- a/sat/res.ml
+++ b/sat/res.ml
@@ -166,7 +166,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
       let new_c, new_cl = (ref temp_c, ref temp_cl) in
       while not (equal_cl cl !new_cl) do
         let unit_to_use = diff_learnt [] cl !new_cl in
-        let unit_r = List.map St.(fun a -> clause_unit a) unit_to_use in
+        let unit_r = List.map (fun a -> clause_unit a) unit_to_use in
         let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
         new_c := temp_c;
         new_cl := temp_cl;
diff --git a/sat/solver_types.ml b/sat/solver_types.ml
index f74d36f5..2eba53b9 100644
--- a/sat/solver_types.ml
+++ b/sat/solver_types.ml
@@ -188,11 +188,6 @@ module Make (F : Formula_intf.S) = struct
     else if a.neg.is_true then sprintf "[F%s]" (level a)
     else ""
 
-  let value_ms_like a =
-    if a.is_true then sprintf ":1%s" (level a)
-    else if a.neg.is_true then sprintf ":0%s" (level a)
-    else ":X"
-
   let pp_premise b v =
     List.iter (fun {name=name} -> bprintf b "%s," name) v
 
@@ -201,9 +196,6 @@ module Make (F : Formula_intf.S) = struct
       (sign a) (a.var.vid+1) (value a) (Log.on_fmt F.print a.lit)
       pp_premise a.var.vpremise
 
-  let pp_atoms_list b l = List.iter (bprintf b "%a ; " pp_atom) l
-  let pp_atoms_array b arr = Array.iter (bprintf b "%a ; " pp_atom) arr
-
   let pp_atoms_vec b vec =
     for i = 0 to Vec.size vec - 1 do
       bprintf b "%a ; " pp_atom (Vec.get vec i)
diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml
index 377eefb4..56f1196e 100644
--- a/util/smtlib/smtlib.ml
+++ b/util/smtlib/smtlib.ml
@@ -65,8 +65,8 @@ let rec translate_term = function
             (* CORE theory translation - '=', 'distinct','ite' not yet implemented *)
             | "not", [e] -> T.make_not e
             | "not", _ -> raise (Bad_arity "not")
-            | "and" as s, l -> T.make_and l
-            | "or" as s, l -> T.make_or l
+            | "and", l -> T.make_and l
+            | "or", l -> T.make_or l
             | "xor" as s, l -> left_assoc s T.make_xor l
             | "=>" as s, l -> right_assoc s T.make_imply l
             | _ -> raise Unknown_command
diff --git a/util/smtlib/smtlib_syntax.ml b/util/smtlib/smtlib_syntax.ml
index c3cac59a..6f33e693 100644
--- a/util/smtlib/smtlib_syntax.ml
+++ b/util/smtlib/smtlib_syntax.ml
@@ -34,7 +34,7 @@ and commanddefinesort_command_symbol11 = pd * ( symbol) list
 and attributevalsexpr_attributevalue_sexpr5 = pd * ( sexpr) list;;
 
 (* pd stands for pos (position) and extradata *)
-let rec dummy () = () 
+let dummy () = () 
 and pd_an_option = function 
   | AnOptionAttribute(d,_) -> d
 
@@ -226,4 +226,4 @@ and pd_attributevalsexpr_attributevalue_sexpr5 = function
 
   | (d,( _ )::f1239o2) -> d
 ;;
-let pd e = pd_commands e;;
\ No newline at end of file
+let pd e = pd_commands e;;
diff --git a/util/sparse_vec.ml b/util/sparse_vec.ml
index d6054011..748eddc6 100644
--- a/util/sparse_vec.ml
+++ b/util/sparse_vec.ml
@@ -27,12 +27,7 @@ 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.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 =
+let 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
diff --git a/util/vec.ml b/util/vec.ml
index 29aa6e1d..7c1333cd 100644
--- a/util/vec.ml
+++ b/util/vec.ml
@@ -57,7 +57,7 @@ let grow_to_double_size t =
   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 =
+let 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