diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index dcc1856aff5bb0cf56a3d25744fec5ba666f0846..f3d16e4fd6c4302c95e8d268e4308569219398bc 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -791,7 +791,7 @@ let rec verifyMuGuarded unguarded formula =
      raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
 
 let verifyFormula formula =
-  verifyMuAltFree formula;
+  ignore (verifyMuAltFree formula);
   verifyMuMonotone [] formula;
   verifyMuGuarded [] formula
 
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 85d08bcabeaf8f13ceba5442f5eaa76fa0ac5440..eb2e67b08d3620b5f55475c4d77bdae18cc60acd 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -575,7 +575,10 @@ let coreGetChildren core = core.childrenC
 let coreAddChild core child = core.childrenC <- child::core.childrenC
 let coreGetConstraints core = core.constraintsC
 let coreSetConstraints core csets = core.constraintsC <- csets
-let coreGetSolver core = core.solver
+let coreGetSolver core =
+  match core.solver with
+  | Some solver -> solver
+  | None -> raise (Failure "Sat solver not allocated")
 let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
 let coreGetFht core = core.fht
 let coreGetIdx (core:core) = core.idx
@@ -785,8 +788,6 @@ let stateToString (state:state): string =
         (csetToString state.sortS cset):: lst
     in
     let constraints = cssFold helper state.constraintsS [] in
-    let core2idx core = core.idx in
-    let fst (a,b) = a in
     let conclusionList =
         List.map (fun (_,lst) ->
                   List.map (fun (core:core) -> string_of_int core.idx) lst
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index b93b94ea1a0798dbcabcf1447a2549b1145c1841..4c605adc757e25c36a43785ce1f5e7aea3b61691 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -253,7 +253,11 @@ val coreGetChildren : core -> state list
 val coreAddChild : core -> state -> unit
 val coreGetConstraints : core -> csetSet
 val coreSetConstraints : core -> csetSet -> unit
-val coreGetSolver : core -> Minisat.solver option
+
+(** Return minisat solver of a core, if allocated
+   @raise Failure if no solver is allocated for this core
+ *)
+val coreGetSolver : core -> Minisat.solver
 val coreDeallocateSolver : core -> unit
 val coreGetFht : core -> fht
 val coreGetIdx : core -> int
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index efb1734a8702628fdb1be1267005b5adcbb0d522..489826987449cacae35b619be958162881318165 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -341,7 +341,7 @@ let rec propagateUnsat = function
                   if comesFromCnstr then coreGetBs core
                   else
                     let bs = coreGetBs core in
-                    let Some solver = coreGetSolver core in
+                    let solver = coreGetSolver core in
                     let fht = coreGetFht core in
                     let lht = lhtInit () in
                     let addLits f acc =
@@ -817,7 +817,7 @@ let getNextState core =
   in
   let fht = coreGetFht core in
   let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
-  let Some solver = coreGetSolver core in
+  let solver = coreGetSolver core in
   let isSat = M.invoke_solver solver litset in
   (* Clearly, if the current core is unsatisfiable, no further child state can
      be created *)
diff --git a/src/lib/FunctorParsing.ml b/src/lib/FunctorParsing.ml
index 23c4ce1c741d5f27e6e8ffc372e3b5d8143d91d3..6671a898ff8fc716af177d9be8632dc9c02d5cb1 100644
--- a/src/lib/FunctorParsing.ml
+++ b/src/lib/FunctorParsing.ml
@@ -24,10 +24,10 @@ let explode (s:string) : char list =
   exp (String.length s - 1) [];;
 
 let implode (l:char list) : string =
-  let res = String.create (List.length l) in
+  let res = Bytes.create (List.length l) in
   let rec imp i = function
   | [] -> res
-  | c :: l -> res.[i] <- c; imp (i + 1) l in
+  | c :: l -> Bytes.set res i c; imp (i + 1) l in
   imp 0 l;;
 
 let string_of_char : char -> string = String.make 1
diff --git a/src/lib/HashConsing.ml b/src/lib/HashConsing.ml
index 6b75c0b9ee40f79c227f74b8b2096b6dce97dd83..f19d88d84fef5ca502c181a533dade055a4b185d 100644
--- a/src/lib/HashConsing.ml
+++ b/src/lib/HashConsing.ml
@@ -211,7 +211,7 @@ module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
           let idxN = hkeyN mod ds in
           let bucketN = data.(idxN) in
           try begin
-            find ndeN bucketN;
+            ignore (find ndeN bucketN);
             hc.size <- succ osize;
           end
           with Not_found ->
diff --git a/src/lib/genAndComp.ml b/src/lib/genAndComp.ml
index 7d5275ddce13f7ec6a0ae9b5eb60d223f0022d16..b75b17e25557ff406f1332e352a34c2702aac284 100644
--- a/src/lib/genAndComp.ml
+++ b/src/lib/genAndComp.ml
@@ -832,7 +832,7 @@ let outputBenchmarks ?(filenameL = "out.tex") ?(filenameG = "plot") ?(filenameD
         let t =
           if ns = 1 then ts else if nu = 1 then tu else if nd = 1 then td else (assert false)
         in
-        if t < ft & (fs+fu+fd) = 0 then succ n else n
+        if t < ft && (fs+fu+fd) = 0 then succ n else n
       in
       List.map2 map2T acc sl
     in
diff --git a/src/lib/minisat.ml b/src/lib/minisat.ml
index d98d9896751192a4c6d753c7d10d8931fd3cbcb0..4dd15a496ef810b88706a5ca075d86f226fab2f5 100644
--- a/src/lib/minisat.ml
+++ b/src/lib/minisat.ml
@@ -3,6 +3,9 @@ type lit = int
 type solver
 type litstatus = LTRUE | LFALSE | LUNDEF
 
+(* "noalloc" is deprecated in OCaml 4.03 and should be replaced by [@@noalloc]
+   once 4.03 becomes the minimum required version
+*)
 external var_to_lit : var -> bool -> lit = "mkLit_stub" "noalloc"
 external lit_to_var : lit -> var = "var_stub" "noalloc"
 external sign : lit -> bool = "sign_stub" "noalloc"