diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index f523b21970..f566fc2f39 100644
--- a/src/analyses/abortUnless.ml
+++ b/src/analyses/abortUnless.ml
@@ -32,10 +32,7 @@ struct
       | [arg] when isIntegralType arg.vtype ->
         (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
          | v when Queries.ID.is_bot v -> false
-         | v ->
-           match Queries.ID.to_bool v with
-           | Some b -> b
-           | None -> false)
+         | v -> BatOption.default false (Queries.ID.to_bool v))
       | _ ->
         (* should not happen, man.local should always be false in this case *)
         false
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 55d79a1131..5c19d65cf4 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -79,10 +79,7 @@ struct
     man.local
 
   let return man exp fundec : D.t =
-    begin match exp with
-      | Some exp -> access_one_top man Read false exp
-      | None -> ()
-    end;
+    Option.iter (access_one_top man Read false) exp;
     man.local
 
   let body man f : D.t =
@@ -99,9 +96,7 @@ struct
       LibraryDesc.Accesses.iter desc.accs (fun {kind; deep = reach} exp ->
           access_one_top ~deref:true man kind reach exp (* access dereferenced using special accesses *)
         ) arglist;
-      (match lv with
-       | Some x -> access_one_top ~deref:true man Write false (AddrOf x)
-       | None -> ());
+      Option.iter (fun x -> access_one_top ~deref:true man Write false (AddrOf x)) lv;
       List.iter (access_one_top man Read false) arglist; (* always read all argument expressions without dereferencing *)
       man.local
 
@@ -115,19 +110,15 @@ struct
     au
 
   let combine_assign man lv fexp f args fc al f_ask =
-    begin match lv with
-      | None      -> ()
-      | Some lval -> access_one_top ~deref:true man Write false (AddrOf lval)
-    end;
+    Option.iter (fun lval -> access_one_top ~deref:true man Write false (AddrOf lval)) lv;
     man.local
 
 
   let threadspawn man  ~multiple lval f args fman =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
-    begin match lval with
-      | None -> ()
-      | Some lval -> access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
-    end;
+    Option.iter (fun lval ->
+        access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
+      ) lval;
     man.local
 
   let query man (type a) (q: a Queries.t): a Queries.result =
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 0f5f0e1434..8dd51487b4 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -291,16 +291,14 @@ struct
     in
     List.fold (fun vs e -> VS.join vs (to_vs e)) (VS.empty ()) args
 
-  let pass_to_callee fundec any_local_reachable var =
-    (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachbale to preserve relationality *)
+  let belongs_to_fundec fundec var =
+    (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachable to preserve relationality *)
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
     let vname = GobApron.Var.show var in
-    let locals = fundec.sformals @ fundec.slocals in
-    match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
-    | None -> true
-    | Some v -> any_local_reachable
+    let equiv v = VM.var_name (Local v) = vname in
+    (not @@ List.exists equiv fundec.sformals) && (not @@ List.exists equiv fundec.slocals)
 
   let make_callee_rel ~thread man f args =
     let fundec = Node.find_fundec man.node in
@@ -328,7 +326,7 @@ struct
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
-        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
+        | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* remove caller locals provided they are unreachable *)
         | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
@@ -358,16 +356,14 @@ struct
     let st = man.local in
     let ask = Analyses.ask_of_man man in
     let new_rel =
-      if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
+      if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then
         let rel' = RD.add_vars st.rel [RV.return] in
-        match e with
-        | Some e ->
+        Option.map_default (fun e ->
           assign_from_globals_wrapper ask man.global {st with rel = rel'} e (fun rel' e' ->
               RD.assign_exp ask rel' RV.return e' (no_overflow ask e)
-            )
-        | None ->
-          rel' (* leaves V.return unconstrained *)
-      )
+              )
+          ) rel' e
+        (* default value rel' leaves V.return unconstrained *)
       else
         RD.copy st.rel
     in
@@ -425,7 +421,7 @@ struct
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
     let new_rel = RD.keep_filter st.rel (fun var ->
         match RV.find_metadata var with
-        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* keep caller locals, provided they were not passed to the function *)
+        | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* keep caller locals, provided they were not passed to the function *)
         | Some (Arg _) -> true (* keep caller args *)
         | Some ((Local _ | Global _)) when not (RD.mem_var new_fun_rel var) -> false (* remove locals and globals, for which no record exists in the new_fun_apr *)
         | Some ((Local v | Global v)) when not (TaintPartialContexts.VS.mem v tainted_vars) -> true (* keep locals and globals, which have not been touched by the call *)
@@ -438,20 +434,17 @@ struct
 
   let combine_assign man r fe f args fc fun_st (f_ask : Queries.ask) =
     let unify_st = man.local in
-    if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
-      let unify_st' = match r with
-        | Some lv ->
+    if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then
+      let unify_st' = Option.map_default (fun lv ->
           let ask = Analyses.ask_of_man man in
           assign_to_global_wrapper ask man.global man.sideg unify_st lv (fun st v ->
               let rel = RD.assign_var st.rel (RV.local v) RV.return in
               assert_type_bounds ask rel v (* TODO: should be done in return instead *)
             )
-        | None ->
-          unify_st
+        ) unify_st r
       in
       RD.remove_vars_with unify_st'.rel [RV.return]; (* mutates! *)
       unify_st'
-    )
     else
       unify_st
 
diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml
index c9045037f7..7592d2ab74 100644
--- a/src/analyses/assert.ml
+++ b/src/analyses/assert.ml
@@ -18,10 +18,7 @@ struct
     let check_assert e st =
       match man.ask (Queries.EvalInt e) with
       | v when Queries.ID.is_bot v -> `Bot
-      | v ->
-        match Queries.ID.to_bool v with
-        | Some b -> `Lifted b
-        | None -> `Top
+      | v -> Option.map_default (fun b -> `Lifted b) `Top (Queries.ID.to_bool v)
     in
     let expr = CilType.Exp.show e in
     let warn warn_fn ?annot msg = if check then
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index c21051b87b..e1145c048d 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -153,10 +153,7 @@ struct
   let char_array : (lval, bytes) Hashtbl.t = Hashtbl.create 500
 
   let init marshal =
-    begin match marshal with
-      | Some marshal -> array_map := marshal
-      | None -> ()
-    end;
+    GobOption.iter ((:=) array_map) marshal;
     return_varstore := Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType;
     longjmp_return := Cilfacade.create_var @@ makeVarinfo false "LONGJMP_RETURN" intType;
     Priv.init ()
@@ -781,7 +778,7 @@ struct
       (* seems like constFold already converts CChr to CInt *)
       | Const (CChr x) -> eval_rv ~man st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
       | Const (CInt (num,ikind,str)) ->
-        (match str with Some x -> if M.tracing then M.tracel "casto" "CInt (%s, %a, %s)" (Z.to_string num) d_ikind ikind x | None -> ());
+        GobOption.iter (fun x -> if M.tracing then M.tracel "casto" "CInt (%s, %a, %s)" (Z.to_string num) d_ikind ikind x) str;
         Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
       | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
       | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) && num = 0.0 -> Float (FD.of_const fkind num) (* constant 0 is ok, CIL creates these for zero-initializers; it is safe across float types *)
@@ -883,10 +880,9 @@ struct
           | _ ->
             None
         in
-        begin match eqs_value with
-          | Some x -> x
-          | None -> evalbinop ~man st LOr ~e1 ~e2 typ (* fallback to general case *)
-        end
+        (* fallback to general case *)
+        let fallback () = evalbinop ~man st LOr ~e1 ~e2 typ in
+        Option.default_delayed fallback eqs_value
       | BinOp (op,e1,e2,typ) ->
         evalbinop ~man st op ~e1 ~e2 typ
       (* Unary operators *)
@@ -1765,9 +1761,7 @@ struct
       end
     in
     let update_one x store =
-      match Addr.to_mval x with
-      | Some x -> update_one_addr x store
-      | None -> store
+      Option.map_default (fun x -> update_one_addr x store) store (Addr.to_mval x)
     in try
       (* We start from the current state and an empty list of global deltas,
        * and we assign to all the the different possible places: *)
@@ -1918,14 +1912,10 @@ struct
       AD.is_top xs || AD.exists not_local xs
     in
     (match rval_val, lval_val with
-     | Address adrs, lval
-       when (not !AnalysisState.global_initialization) && get_bool "kernel" && not_local lval && not (AD.is_top adrs) ->
-       let find_fps e xs = match Addr.to_var_must e with
-         | Some x -> x :: xs
-         | None -> xs
-       in
+     | Address adrs, lval when (not !AnalysisState.global_initialization) && get_bool "kernel" && not_local lval && not (AD.is_top adrs) ->
+       let find_fps e xs = Option.map_default (fun x -> x :: xs) xs (Addr.to_var_must e) in
        let vars = AD.fold find_fps adrs [] in (* filter_map from AD to list *)
-       let funs = Seq.filter (fun x -> isFunctionType x.vtype)@@ List.to_seq vars in
+       let funs = Seq.filter (fun x -> isFunctionType x.vtype) @@ List.to_seq vars in
        Seq.iter (fun x -> man.spawn None x []) funs
      | _ -> ()
     );
@@ -1978,8 +1968,7 @@ struct
     (* For a boolean value: *)
     | Int value ->
       if M.tracing then M.traceu "branch" "Expression %a evaluated to %a" d_exp exp ID.pretty value;
-      begin match ID.to_bool value with
-        | Some v ->
+      Option.map_default_delayed (fun v ->
           (* Eliminate the dead branch and just propagate to the true branch *)
           if v = tv then
             refine ()
@@ -1987,9 +1976,7 @@ struct
             if M.tracing then M.tracel "branch" "A The branch %B is dead!" tv;
             raise Deadcode
           )
-        | None ->
-          refine () (* like fallback below *)
-      end
+        ) refine (ID.to_bool value)
     (* for some reason refine () can refine these, but not raise Deadcode in struct *)
     | Address ad when tv && AD.is_null ad ->
       raise Deadcode
@@ -2027,9 +2014,7 @@ struct
       let locals = List.filter (fun v -> not (WeakUpdates.mem v st.weak)) (fundec.sformals @ fundec.slocals) in
       let nst_part = rem_many_partitioning (Queries.to_value_domain_ask ask) man.local locals in
       let nst: store = rem_many ask nst_part locals in
-      match exp with
-      | None -> nst
-      | Some exp ->
+      Option.map_default (fun exp ->
         let t_override = match Cilfacade.fundec_return_type fundec with
           | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false
           | ret -> ret
@@ -2044,6 +2029,7 @@ struct
           man.sideg (V.thread tid) (G.create_thread rv);
           Priv.thread_return ask (priv_getg man.global) (priv_sideg man.sideg) tid st'
         | _ -> st'
+        ) nst exp
 
   let vdecl man (v:varinfo) =
     if not (Cil.isArrayType v.vtype) then
@@ -2154,7 +2140,7 @@ struct
     let new_cpa = project (Queries.to_value_domain_ask ask) (Some p) new_cpa fundec in
 
     (* Identify locals of this fundec for which an outer copy (from a call down the callstack) is reachable *)
-    let reachable_other_copies = List.filter (fun v -> match Cilfacade.find_scope_fundec v with Some scope -> CilType.Fundec.equal scope fundec | None -> false) reachable in
+    let reachable_other_copies = List.filter (fun v -> GobOption.exists (CilType.Fundec.equal fundec) @@ Cilfacade.find_scope_fundec v) reachable in
     (* Add to the set of weakly updated variables *)
     let new_weak = WeakUpdates.join st.weak (WeakUpdates.of_list reachable_other_copies) in
     {st' with cpa = new_cpa; weak = new_weak}
@@ -2169,21 +2155,14 @@ struct
       try
         (* try to get function declaration *)
         let fd = Cilfacade.find_varinfo_fundec v in
-        let args =
-          match arg with
-          | Some x -> [x]
-          | None -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals
-        in
+        let args = Option.map_default_delayed (List.singleton) (fun () -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals) arg in
         Some (lval, v, args, multiple)
       with Not_found ->
         if LF.use_special f.vname then None (* we handle this function *)
         else if isFunctionType v.vtype then
           (* FromSpec warns about unknown thread creation, so we don't do it here any more *)
           let (_, v_args, _, _) = Cil.splitFunctionTypeVI v in
-          let args = match arg with
-            | Some x -> [x]
-            | None -> List.map (fun x -> MyCFG.unknown_exp) (Cil.argsToList v_args)
-          in
+          let args = Option.map_default_delayed (List.singleton) (fun () -> List.map (fun x -> MyCFG.unknown_exp) (Cil.argsToList v_args)) arg in
           Some (lval, v, args, multiple)
         else (
           M.debug ~category:Analyzer "Not creating a thread from %s because its type is %a" v.vname d_type v.vtype;
@@ -2334,11 +2313,11 @@ struct
          `Top)
 
   let special man (lv:lval option) (f: varinfo) (args: exp list) =
-    let invalidate_ret_lv st = match lv with
-      | Some lv ->
+    let invalidate_ret_lv st =
+      Option.map_default (fun lv ->
         if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s" d_plainlval lv f.vname;
         invalidate ~must:true ~deep:false ~man st [Cil.mkAddrOrStartOf lv]
-      | None -> st
+        ) st lv
     in
     let addr_type_of_exp exp =
       let lval = mkMem ~addr:(Cil.stripCasts exp) ~off:NoOffset in
@@ -2435,48 +2414,47 @@ struct
         end
         (* else compute value in array domain *)
       else
-        let lv_a, lv_typ = match lv with
-          | Some lv_val -> eval_lv ~man st lv_val, Cilfacade.typeOfLval lv_val
-          | None -> s1_a, s1_typ in
-        begin match (get ~man st s1_a None), get ~man st s2_a None with
-          | Array array_s1, Array array_s2 -> set ~man ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2)
-          | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType ->
-            let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
-            let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
-            set ~man ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2)
-          | Bot, Array array_s2 ->
-            (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
-            let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
-            let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
-            let s_id =
-              try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
-              with Failure _ -> ID.top_of ptrdiff_ik in
-            let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
-            set ~man st lv_a lv_typ (op_array empty_array array_s2)
-          | Bot , _ when CilType.Typ.equal s2_typ charPtrType ->
-            (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
-            let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
-            let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
-            let s_id =
-              try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
-              with Failure _ -> ID.top_of ptrdiff_ik in
-            let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
-            let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
-            let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
-            set ~man st lv_a lv_typ (op_array empty_array array_s2)
-          | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType ->
-            (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *)
-            if op_addr = None then
-              (* triggers warning, function only evaluated for side-effects *)
-              let _ = AD.string_writing_defined s1_a in
-              set ~man st s1_a s1_typ (VD.top_value (unrollType s1_typ))
-            else
-              let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in
-              let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in
-              set ~man st lv_a lv_typ (op_array array_s1 array_s2)
-          | _ ->
-            set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ))
-        end
+        let lv_a, lv_typ =
+          Option.map_default (fun lv -> eval_lv ~man st lv, Cilfacade.typeOfLval lv) (s1_a, s1_typ) lv
+        in
+        match (get ~man st s1_a None), get ~man st s2_a None with
+        | Array array_s1, Array array_s2 -> set ~man ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2)
+        | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType ->
+          let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
+          let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
+          set ~man ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2)
+        | Bot, Array array_s2 ->
+          (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
+          let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
+          let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
+          let s_id =
+            try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
+            with Failure _ -> ID.top_of ptrdiff_ik in
+          let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
+          set ~man st lv_a lv_typ (op_array empty_array array_s2)
+        | Bot , _ when CilType.Typ.equal s2_typ charPtrType ->
+          (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
+          let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
+          let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
+          let s_id =
+            try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
+            with Failure _ -> ID.top_of ptrdiff_ik in
+          let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
+          let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
+          let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
+          set ~man st lv_a lv_typ (op_array empty_array array_s2)
+        | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType ->
+          (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *)
+          if op_addr = None then
+            (* triggers warning, function only evaluated for side-effects *)
+            let _ = AD.string_writing_defined s1_a in
+            set ~man st s1_a s1_typ (VD.top_value (unrollType s1_typ))
+          else
+            let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in
+            let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in
+            set ~man st lv_a lv_typ (op_array array_s1 array_s2)
+        | _ ->
+          set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ))
     in
     let st = match desc.special args, f.vname with
     | Memset { dest; ch; count; }, _ ->
@@ -2502,10 +2480,9 @@ struct
     | Strcpy { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_copy ar1 ar2 (eval_n n)))
     | Strcat { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_concat ar1 ar2 (eval_n n)))
     | Strlen s, _ ->
-      begin match lv with
-        | Some lv_val ->
-          let dest_a = eval_lv ~man st lv_val in
-          let dest_typ = Cilfacade.typeOfLval lv_val in
+      Option.map_default (fun lv ->
+          let dest_a = eval_lv ~man st lv in
+          let dest_typ = Cilfacade.typeOfLval lv in
           let v = eval_rv ~man st s in
           let a = address_from_value v in
           let value:value =
@@ -2515,37 +2492,32 @@ struct
               Int (AD.to_string_length a)
               (* else compute strlen in array domain *)
             else
-              begin match get ~man st a None with
-                | Array array_s -> Int (CArrays.to_string_length array_s)
-                | _ -> VD.top_value (unrollType dest_typ)
-              end in
+              match get ~man st a None with
+              | Array array_s -> Int (CArrays.to_string_length array_s)
+              | _ -> VD.top_value (unrollType dest_typ)
+          in
           set ~man st dest_a dest_typ value
-        | None -> st
-      end
+        ) st lv
     | Strstr { haystack; needle }, _ ->
-      begin match lv with
-        | Some lv_val ->
+      Option.map_default (fun lv_val ->
           (* check if needle is a substring of haystack in string literals domain if haystack and needle are string literals,
-             else check in null bytes domain if both haystack and needle are / can be transformed to an array domain representation;
-             if needle is substring, assign the substring of haystack starting at the first occurrence of needle to dest,
-             if it surely isn't, assign a null_ptr *)
+              else check in null bytes domain if both haystack and needle are / can be transformed to an array domain representation;
+              if needle is substring, assign the substring of haystack starting at the first occurrence of needle to dest,
+              if it surely isn't, assign a null_ptr *)
           string_manipulation haystack needle lv true (Some (fun h_a n_a -> Address (AD.substring_extraction h_a n_a)))
             (fun h_ar n_ar -> match CArrays.substring_extraction h_ar n_ar with
                | CArrays.IsNotSubstr -> Address (AD.null_ptr)
                | CArrays.IsSubstrAtIndex0 -> Address (eval_lv ~man st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
                | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~man st
                                                               (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Lazy.force Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
-        | None -> st
-      end
+        ) st lv
     | Strcmp { s1; s2; n }, _ ->
-      begin match lv with
-        | Some _ ->
+      Option.map_default (fun _ ->
           (* when s1 and s2 are string literals, compare both completely or their first n characters in the string literals domain;
              else compare them in the null bytes array domain if they are / can be transformed to an array domain representation *)
           string_manipulation s1 s2 lv false (Some (fun s1_a s2_a -> Int (AD.string_comparison s1_a s2_a (eval_n n))))
             (fun s1_ar s2_ar -> Int (CArrays.string_comparison s1_ar s2_ar (eval_n n)))
-        | None -> st
-      end
+        ) st lv
     | Abort, _ -> raise Deadcode
     | ThreadExit { ret_val = exp }, _ ->
       begin match ThreadId.get_current (Analyses.ask_of_man man) with
@@ -2573,22 +2545,17 @@ struct
         let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in
         let dest_typ = get_type dst_lval in
         let dest_a = eval_lv ~man st dst_lval in
+        let fallback () = set ~man st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) in
         match eval_rv ~man st mtyp with
         | Int x ->
-          begin
-            match ID.to_int x with
-            | Some z ->
+          Option.map_default_delayed (fun z ->
               if M.tracing then M.tracel "attr" "setting";
               set ~man st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z))
-            | None -> set ~man st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ()))
-          end
-        | _ -> set ~man st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ()))
+            ) fallback (ID.to_int x)
+        | _ -> fallback ()
       end
     | Identity e, _ ->
-      begin match lv with
-        | Some x -> assign man x e
-        | None -> man.local
-      end
+      Option.map_default (fun lv -> assign man lv e) man.local lv
     (**Floating point classification and trigonometric functions defined in c99*)
     | Math { fun_args; }, _ ->
       let apply_unary fk float_fun x =
@@ -2656,10 +2623,7 @@ struct
           | Abs (ik, x) -> Int (ID.cast_to ik (apply_abs ik x))
         end
       in
-      begin match lv with
-        | Some lv_val -> set ~man st (eval_lv ~man st lv_val) (Cilfacade.typeOfLval lv_val) result
-        | None -> st
-      end
+      Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) result) st lv
     (* handling thread creations *)
     | ThreadCreate _, _ ->
       invalidate_ret_lv man.local (* actual results joined via threadspawn *)
@@ -2746,8 +2710,7 @@ struct
     | Realloc { ptr = p; size }, _ ->
       (* Realloc shouldn't be passed non-dynamically allocated memory *)
       check_invalid_mem_dealloc man f p;
-      begin match lv with
-        | Some lv ->
+      Option.map_default (fun lv ->
           let p_rv = eval_rv ~man st p in
           let p_addr =
             match p_rv with
@@ -2773,9 +2736,7 @@ struct
             (heap_addr, TVoid [], heap_val);
             (lv_addr, Cilfacade.typeOfLval lv, Address heap_addr');
           ] (* TODO: free (i.e. invalidate) old blob if successful? *)
-        | None ->
-          st
-      end
+        ) st lv
     | Free ptr, _ ->
       (* Free shouldn't be passed non-dynamically allocated memory *)
       check_invalid_mem_dealloc man f ptr;
@@ -2790,11 +2751,9 @@ struct
           r
         | _ -> failwith "problem?!"
       in
-      begin match lv with
-        | Some lv ->
+      Option.map_default (fun lv ->
           set ~man st' (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero))
-        | None -> st'
-      end
+        ) st' lv
     | Longjmp {env; value}, _ ->
       let ensure_not_zero (rv:value) = match rv with
         | Int i ->
@@ -2816,12 +2775,10 @@ struct
       let t = Cilfacade.typeOf value in
       set ~man ~t_override:t man.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
     | Rand, _ ->
-      begin match lv with
-        | Some x ->
+      Option.map_default (fun x ->
           let result:value = (Int (ID.starting IInt Z.zero)) in
           set ~man st (eval_lv ~man st x) (Cilfacade.typeOfLval x) result
-        | None -> st
-      end
+        ) st lv
     | _, _ ->
       let st =
         special_unknown_invalidate man f args
@@ -2851,19 +2808,17 @@ struct
             (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
             | Some voidVal when Addr.type_of addr = voidType -> {st with cpa = CPA.add v voidVal st.cpa}
             | _ ->
-              begin
-                let address = AD.singleton addr in
-                let new_val = get ~man fun_st address None in
-                if M.tracing then M.trace "taintPC" "update val: %a" VD.pretty new_val;
-                let st' = set_savetop ~man st address lval_type new_val in
-                match Dep.find_opt v fun_st.deps with
-                | None -> st'
-                (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
-                | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
-                                                                  match val_opt with
-                                                                  | None -> accCPA
-                                                                  | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
-              end
+              let address = AD.singleton addr in
+              let new_val = get ~man fun_st address None in
+              if M.tracing then M.trace "taintPC" "update val: %a" VD.pretty new_val;
+              let st' = set_savetop ~man st address lval_type new_val in
+              Option.map_default (fun deps ->
+                  {st' with cpa = (Dep.VarSet.fold
+                                     (fun v accCPA ->
+                                        let val_opt = CPA.find_opt v fun_st.cpa in
+                                        Option.map_default (fun new_val -> CPA.add v new_val accCPA) accCPA val_opt
+                                     ) deps st'.cpa)}
+                ) st' (Dep.find_opt v fun_st.deps)
           end
         | _ -> st
       ) tainted_lvs local_st
@@ -2939,9 +2894,7 @@ struct
       in
       let return_val = project_val (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (attributes_varinfo (return_varinfo ()) callerFundec) (Some p) return_val (is_privglob (return_varinfo ())) in
 
-      match lval with
-      | None      -> st
-      | Some lval -> set_savetop ~man st (eval_lv ~man st lval) (Cilfacade.typeOfLval lval) return_val
+      Option.map_default (fun lval -> set_savetop ~man st (eval_lv ~man st lval) (Cilfacade.typeOfLval lval) return_val) st lval
     in
     combine_one man.local after
 
@@ -2955,16 +2908,13 @@ struct
       [st]
 
   let threadspawn man ~multiple (lval: lval option) (f: varinfo) (args: exp list) fman: D.t =
-    begin match lval with
-      | Some lval ->
-        begin match ThreadId.get_current (Analyses.ask_of_man fman) with
-          | `Lifted tid ->
-            (* Cannot set here, because man isn't in multithreaded mode and set wouldn't side-effect if lval is global. *)
-            man.emit (Events.AssignSpawnedThread (lval, tid))
-          | _ -> ()
-        end
-      | None -> ()
-    end;
+    GobOption.iter (fun lval ->
+        match ThreadId.get_current (Analyses.ask_of_man fman) with
+        | `Lifted tid ->
+          (* Cannot set here, because man isn't in multithreaded mode and set wouldn't side-effect if lval is global. *)
+          man.emit (Events.AssignSpawnedThread (lval, tid))
+        | _ -> ()
+      ) lval;
     (* D.join man.local @@ *)
     Priv.threadspawn (Analyses.ask_of_man man) (priv_getg man.global) (priv_sideg man.sideg) man.local
 
@@ -3130,12 +3080,10 @@ struct
     | Events.Unassume {exp; tokens} ->
       Timing.wrap "base unassume" (unassume man exp) tokens
     | Events.Longjmped {lval} ->
-      begin match lval with
-        | Some lval ->
+      Option.map_default (fun lval ->
           let st' = assign man lval (Lval (Cil.var !longjmp_return)) in
           {st' with cpa = CPA.remove !longjmp_return st'.cpa}
-        | None -> man.local
-      end
+        ) man.local lval
     | _ ->
       man.local
 end
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 484d7bac62..975283c090 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -305,9 +305,7 @@ struct
          * If the upper bound of a is divisible by b, we can also meet with the result of a/b*b - c to get the precise [3,3].
          * If b is negative we have to look at the lower bound. *)
         let is_divisible bound =
-          match bound a with
-          | Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero
-          | None -> false
+          GobOption.exists (fun ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero) (bound a)
         in
         let max_pos = match ID.maximal b with None -> true | Some x -> Z.compare x Z.zero >= 0 in
         let min_neg = match ID.minimal b with None -> true | Some x -> Z.compare x Z.zero < 0 in
@@ -735,6 +733,7 @@ struct
                 | _ -> Int c
               in
               (* handle special calls *)
+              let default () = update_lval c x c' ID.pretty in
               begin match x, t with
                 | (Var v, offs), TInt (ik, _) ->
                   let tmpSpecial = man.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in
@@ -744,24 +743,21 @@ struct
                       let c' = ID.cast_to ik c in (* different ik! *)
                       inv_exp (Int (ID.join c' (ID.neg c'))) xInt st
                     | tmpSpecial ->
-                      begin match ID.to_bool c with
-                        | Some tv ->
-                          begin match tmpSpecial with
-                            | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
-                            | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
-                            (* should be correct according to C99 standard*)
-                            (* The following do to_bool and of_bool to convert Not{0} into 1 for downstream float inversions *)
-                            | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
-                            | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
-                            | _ -> update_lval c x c' ID.pretty
-                          end
-                        | None -> update_lval c x c' ID.pretty
-                      end
+                      BatOption.map_default_delayed (fun tv ->
+                          match tmpSpecial with
+                          | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
+                          | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
+                          (* should be correct according to C99 standard*)
+                          (* The following do to_bool and of_bool to convert Not{0} into 1 for downstream float inversions *)
+                          | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
+                          | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
+                          | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
+                          | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
+                          | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
+                          | _ -> default ()
+                        ) default (ID.to_bool c)
                   end
-                | _, _ -> update_lval c x c' ID.pretty
+                | _, _ -> default ()
               end
             | Float c ->
               let c' = match t with
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index d31243ae70..1a5244d18c 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -643,11 +643,7 @@ module Codegen = struct
         let end_label = res_id ^ "_end" in
         let goto = goto_str % label in
         let goto_start_node =
-          match List.find is_start_node nodes with
-          | Some node ->
-            goto node
-          | None ->
-            ""
+          Option.map_default goto "" (List.find is_start_node nodes)
         in
         let called_funs = ref [] in
         let str_edge (a, action, b) =
diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml
index 02cbe3d231..fa9adbb650 100644
--- a/src/analyses/loopTermination.ml
+++ b/src/analyses/loopTermination.ml
@@ -75,9 +75,7 @@ struct
     | Queries.MustTermLoop loop_statement ->
       let multithreaded = man.ask Queries.IsEverMultiThreaded in
       (not multithreaded)
-      && (match G.find_opt (`Lifted loop_statement) (man.global ()) with
-            Some b -> b
-          | None -> false)
+      && (BatOption.default false (G.find_opt (`Lifted loop_statement) (man.global ())))
     | Queries.MustTermAllLoops ->
       let multithreaded = man.ask Queries.IsEverMultiThreaded in
       if multithreaded then (
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 07f798583e..530aaa4360 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -166,14 +166,13 @@ struct
   let return man (exp:exp option) (f:fundec) : D.t =
     let remove_var x v = List.fold_right D.remove (to_addrs v) x in
     let nst = List.fold_left remove_var man.local (f.slocals @ f.sformals) in
-    match exp with
-    | Some ret ->
+    BatOption.map_default (fun ret ->
       warn_deref_exp (Analyses.ask_of_man man) man.local ret;
-      begin match get_concrete_exp ret man.global man.local with
-        | Some ev when might_be_null (Analyses.ask_of_man man) ev man.global man.local ->
-          D.add (return_addr ()) nst
-        | _ -> nst  end
-    | None -> nst
+      match get_concrete_exp ret man.global man.local with
+      | Some ev when might_be_null (Analyses.ask_of_man man) ev man.global man.local ->
+        D.add (return_addr ()) nst
+      | _ -> nst
+      ) nst exp
 
   (* Function calls *)
 
diff --git a/src/autoTune.ml b/src/autoTune.ml
index ed5b8a59a0..5449998db1 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -97,15 +97,10 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi
 let findMallocWrappers () =
   let isMalloc f =
     Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
-    if LibraryFunctions.is_special f then (
+    if LibraryFunctions.is_special f then
       let desc = LibraryFunctions.find f in
-      match functionArgs f with
-      | None -> false
-      | Some args ->
-        match desc.special args with
-        | Malloc _ -> true
-        | _ -> false
-    )
+      let args = functionArgs f in
+      GobOption.exists (fun args -> match desc.special args with Malloc _ -> true | _ -> false) args
     else
       false
   in
diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml
index da684cc4f4..f84cd58acb 100644
--- a/src/cdomain/value/cdomains/addressDomain.ml
+++ b/src/cdomain/value/cdomains/addressDomain.ml
@@ -270,9 +270,7 @@ struct
     let needle' = List.map Addr.to_c_string (elements needle) in
 
     (* helper functions *)
-    let extract_lval_string = function
-      | Some s -> of_string s
-      | None -> null_ptr in
+    let extract_lval_string = BatOption.map_default of_string null_ptr in
     let compute_substring s1 s2 =
       try
         let i = Str.search_forward (Str.regexp_string s2) s1 0 in
diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml
index 4192489c3a..46d602d774 100644
--- a/src/cdomain/value/cdomains/arrayDomain.ml
+++ b/src/cdomain/value/cdomains/arrayDomain.ml
@@ -202,9 +202,6 @@ struct
     (show_list xl) ^ Val.show xr ^ ")"
   let pretty () x = text "Array: " ++ text (show x)
   let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
-  let extract x default = match x with
-    | Some c -> c
-    | None -> default
   let get ?(checkBounds=true)  (ask: VDQ.t) (xl, xr) (_,i) =
     let search_unrolled_values min_i max_i =
       let rec subjoin l i = match l with
@@ -218,8 +215,8 @@ struct
           end in
       subjoin xl Z.zero in
     let f = Z.of_int (factor ()) in
-    let min_i = extract (Idx.minimal i) Z.zero in
-    let max_i = extract (Idx.maximal i) f in
+    let min_i = BatOption.default Z.zero (Idx.minimal i) in
+    let max_i = BatOption.default f (Idx.maximal i) in
     if Z.geq min_i f then xr
     else if Z.lt max_i f then search_unrolled_values min_i max_i
     else Val.join xr (search_unrolled_values min_i (Z.of_int ((factor ())-1)))
@@ -239,8 +236,8 @@ struct
       if Z.equal min_i max_i then full_update xl Z.zero
       else weak_update xl Z.zero in
     let f = Z.of_int (factor ()) in
-    let min_i = extract(Idx.minimal i) Z.zero in
-    let max_i = extract(Idx.maximal i) f in
+    let min_i = BatOption.default Z.zero (Idx.minimal i) in
+    let max_i = BatOption.default f (Idx.maximal i) in
     if Z.geq min_i f then (xl, (Val.join xr v))
     else if Z.lt max_i f then ((update_unrolled_values min_i max_i), xr)
     else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
@@ -501,32 +498,26 @@ struct
         x
       else
         (* check if one part covers the entire array, so we can drop partitioning *)
-        begin
-          let e_must_bigger_max_index =
-            match length with
-            | Some l ->
-              begin
-                match Idx.to_int l with
-                | Some i ->
-                  let b = VDQ.may_be_less ask.eval_int e (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) i) in
-                  not b (* !(e <_{may} length) => e >=_{must} length *)
-                | None -> false
-              end
-            | _ -> false
-          in
-          let e_must_less_zero =
+        let e_must_bigger_max_index = GobOption.exists (fun i ->
+            let b = VDQ.may_be_less ask.eval_int e (Cil.kintegerCilint (Cilfacade.ptrdiff_ikind ()) i) in
+            not b (* !(e <_{may} length) => e >=_{must} length *)
+          ) (Option.bind length Idx.to_int)
+        in
+
+        if e_must_bigger_max_index then
+          (* Entire array is covered by left part, dropping partitioning. *)
+          Joint xl
+        else
+          let e_must_less_zero  =
             VDQ.eval_int_binop (module BoolDomain.MustBool) Lt ask.eval_int e Cil.zero (* TODO: untested *)
           in
-          if e_must_bigger_max_index then
-            (* Entire array is covered by left part, dropping partitioning. *)
-            Joint xl
-          else if e_must_less_zero then
+          if e_must_less_zero then
             (* Entire array is covered by right value, dropping partitioning. *)
             Joint xr
           else
             (* If we can not drop partitioning, move *)
             move (movement_for_exp e) (e, (xl,xm, xr))
-        end
+
     | _ -> x (* If the array is not partitioned, nothing to do *)
 
   let move_if_affected ?replace_with_const = move_if_affected_with_length ?replace_with_const None
@@ -534,7 +525,7 @@ struct
   let set_with_length length (ask:VDQ.t) x (i,_) a =
     if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
     match i with
-    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
+    | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.all) ->
       (* TODO: Doesn't seem to work for unassume. *)
       Joint a
     | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.any) ->
@@ -550,16 +541,9 @@ struct
         let n = ask.eval_int e in
         VDQ.ID.to_int n
       in
-      let equals_zero e = BatOption.map_default (Z.equal Z.zero) false (exp_value e) in
+      let equals_zero e = GobOption.exists (Z.equal Z.zero) (exp_value e) in
       let equals_maxIndex e =
-        match length with
-        | Some l ->
-          begin
-            match Idx.to_int l with
-            | Some i -> BatOption.map_default (Z.equal (Z.pred i)) false (exp_value e)
-            | None -> false
-          end
-        | _ -> false
+        GobOption.exists2 (fun l -> Z.equal (Z.pred l)) (Option.bind length Idx.to_int) (exp_value e)
       in
       let lubIfNotBot x = if Val.is_bot x then x else Val.join a x in
       match x with
@@ -666,19 +650,14 @@ struct
 
   let length _ = None
 
+  let must_i_one_smaller l i =
+    GobOption.exists2 (fun l i -> Z.equal i (Z.pred l)) (Option.bind l Idx.to_int) i
+
+  let must_be_zero = GobOption.exists (Z.equal Z.zero)
+
   let smart_op (op: Val.t -> Val.t -> Val.t) length x1 x2 x1_eval_int x2_eval_int =
     normalize @@
-    let must_be_length_minus_one v = match length with
-      | Some l ->
-        begin
-          match Idx.to_int l with
-          | Some i ->
-            v = Some (Z.pred i)
-          | None -> false
-        end
-      | None -> false
-    in
-    let must_be_zero v = v = Some Z.zero in
+    let must_be_length_minus_one = must_i_one_smaller length in
     let op_over_all = op (join_of_all_parts x1) (join_of_all_parts x2) in
     match x1, x2 with
     | Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) when Basetype.CilExp.equal e1 e2 ->
@@ -742,17 +721,7 @@ struct
 
   let smart_leq_with_length length x1_eval_int x2_eval_int x1 x2 =
     let leq' = Val.smart_leq x1_eval_int x2_eval_int in
-    let must_be_zero v = (v = Some Z.zero) in
-    let must_be_length_minus_one v =  match length with
-      | Some l ->
-        begin
-          match Idx.to_int l with
-          | Some i ->
-            v = Some (Z.pred i)
-          | None -> false
-        end
-      | None -> false
-    in
+    let must_be_length_minus_one = must_i_one_smaller length in
     match x1, x2 with
     | Joint x1, Joint x2 ->
       leq' x1 x2
@@ -833,10 +802,10 @@ end
 (* This is the main array out of bounds check *)
 let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
   if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
-    let idx_before_end = Idx.to_bool (Idx.lt v l) (* check whether index is before the end of the array *)
-    and idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) in (* check whether the index is non-negative *)
+    let idx_before_end = Idx.to_bool (Idx.lt v l) in (* check whether index is before the end of the array *)
+    let idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) in (* check whether the index is non-negative *)
     (* For an explanation of the warning types check the Pull Request #255 *)
-    match(idx_after_start, idx_before_end) with
+    match idx_after_start, idx_before_end with
     | Some true, Some true -> (* Certainly in bounds on both sides.*)
       ()
     | Some true, Some false -> (* The following matching differentiates the must and may cases*)
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index f41d48ab61..06e23f108d 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -59,10 +59,8 @@ let exclude_vars_regexp = ResettableLazy.from_fun (fun () ->
 (* let var_is_tmp {vdescrpure} = not vdescrpure (* doesn't exclude tmp___0 *) *)
 (* TODO: instead check if vdescr is nonempty? (doesn't cover all cases, e.g. ternary temporary) *)
 let varname_is_tmp vname = Str.string_match (ResettableLazy.force exclude_vars_regexp) vname 0
-let var_is_tmp vi =
-  match Cilfacade.find_original_name vi with
-  | None -> true
-  | Some vname -> varname_is_tmp vname
+let var_is_tmp vi = BatOption.map_default varname_is_tmp true (Cilfacade.find_original_name vi)
+
 class exp_contains_tmp_visitor (acc: bool ref) = object
   inherit nopCilVisitor as super
   method! vvrbl (vi: varinfo) =
diff --git a/src/cdomain/value/domains/valueDomainQueries.ml b/src/cdomain/value/domains/valueDomainQueries.ml
index bafec3f8bd..6ccdefd0a6 100644
--- a/src/cdomain/value/domains/valueDomainQueries.ml
+++ b/src/cdomain/value/domains/valueDomainQueries.ml
@@ -61,9 +61,7 @@ let eval_int_binop (module Bool: Lattice.S with type t = bool) binop (eval_int:
   if ID.is_bot i || ID.is_bot_ikind i then
     Bool.top () (* base returns bot for non-int results, consider unknown *)
   else
-    match ID.to_bool i with
-    | Some b -> b
-    | None -> Bool.top ()
+    BatOption.default (Bool.top ()) (ID.to_bool i)
 
 (** Backwards-compatibility for former [MustBeEqual] query. *)
 let must_be_equal = eval_int_binop (module MustBool) Eq
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 60a9a4dc84..8e2c8de0db 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -432,9 +432,8 @@ let createCFG (file: file) =
                   List.iter (fun (fromNode, toNode) ->
                       addEdge_fromLoc fromNode (Test (one, false)) toNode;
                       added_connect := true;
-                      match NH.find_option node_scc toNode with
-                      | Some toNode_scc -> iter_scc toNode_scc (* continue to target scc as normally, to ensure they are also connected *)
-                      | None -> () (* pseudo return, wasn't in scc, but is fine *)
+                      Option.iter iter_scc (NH.find_option node_scc toNode) (* continue to target scc as normally, to ensure they are also connected *)
+                      (* otherwise pseudo return, wasn't in scc, but is fine *)
                     ) targets
                 )
               )
@@ -556,12 +555,10 @@ struct
     Format.fprintf out ("\t%a [%s];\n") p_node n styles;
     match n with
     | Statement s when get_bool "dbg.cfg.loop-unrolling" ->
-      begin match LoopUnrolling0.find_copyof s with
-        | Some s' ->
+      Option.iter (fun s' ->
           let n' = Statement s' in
           Format.fprintf out "\t%a -> %a [style=dotted];\n" p_node n p_node n'
-        | None -> ()
-      end
+        ) (LoopUnrolling0.find_copyof s)
     | _ -> ()
 end
 
diff --git a/src/common/util/richVarinfo.ml b/src/common/util/richVarinfo.ml
index 6a27339eed..fe52b04ae5 100644
--- a/src/common/util/richVarinfo.ml
+++ b/src/common/util/richVarinfo.ml
@@ -57,11 +57,7 @@ struct
 
   let marshal () = !xh
 
-  let unmarshal = function
-    | Some xh_loaded ->
-      xh := xh_loaded
-    | None -> ()
-
+  let unmarshal = Option.iter ((:=) xh)
   let bindings () = List.of_seq (XH.to_seq !xh)
 end
 
diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml
index 60859f1ccb..043dbc9253 100644
--- a/src/constraint/constrSys.ml
+++ b/src/constraint/constrSys.ml
@@ -282,9 +282,7 @@ struct
     include S
 
     let system x =
-      match S.system x with
-      | None -> None
-      | Some f ->
+      Option.map (fun f ->
         let f' get set =
           let old_current_var = !current_var in
           current_var := Some x;
@@ -294,6 +292,7 @@ struct
               f get set
             )
         in
-        Some f'
+        f'
+        ) (S.system x)
   end
 end
diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
index 837bd65589..d7c77812f1 100644
--- a/src/incremental/compareCIL.ml
+++ b/src/incremental/compareCIL.ml
@@ -101,9 +101,7 @@ let addToFinalMatchesMapping oV nV final_matches =
 let empty_rename_assms m = VarinfoMap.for_all (fun vo vn -> vo.vname = vn.vname) m
 
 let already_matched oV nV final_matches =
-  match VarinfoMap.find_opt oV (fst final_matches) with
-  | None -> false
-  | Some v -> v.vid = oV.vid
+  GobOption.exists (fun v -> v.vid = nV.vid) (VarinfoMap.find_opt oV (fst final_matches))
 
 (* looks up the result of the already executed comparison and returns true if it is unchanged, false if it is changed.
    Throws an exception if not found. *)
diff --git a/src/incremental/makefileUtil.ml b/src/incremental/makefileUtil.ml
index 33cd8f64c9..4c3b6051c7 100644
--- a/src/incremental/makefileUtil.ml
+++ b/src/incremental/makefileUtil.ml
@@ -9,12 +9,11 @@ let comb_suffix = "_comb.c"
 
 let exec_command ?path (command: string) =
   let current_dir = Sys.getcwd () in
-  (match path with
-   | Some path ->
+  GobOption.iter (fun path ->
      let path_str = Fpath.to_string path in
      if Sys.file_exists path_str && Sys.is_directory path_str then Sys.chdir path_str
      else failwith ("Directory " ^ path_str ^ " does not exist!")
-   | None -> ());
+    ) path;
   Logs.debug "%s" ("executing command `" ^ command ^ "` in " ^ Sys.getcwd ());
   let (std_out, std_in) = open_process command in
   let output = Buffer.create buff_size in
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 70b7f04f4f..e688012dd9 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -214,12 +214,7 @@ let parse_arguments () =
   let anon_arg = set_string "files[+]" in
   let arg_speclist = Arg_complete.arg_speclist (Lazy.force option_spec_list) in
   Arg.parse arg_speclist anon_arg "Look up options using 'goblint --help'.";
-  begin match !writeconffile with
-    | Some writeconffile ->
-      GobConfig.write_file writeconffile;
-      raise Stdlib.Exit
-    | None -> ()
-  end;
+  GobOption.iter (fun writeconffile -> GobConfig.write_file writeconffile; raise Stdlib.Exit) !writeconffile;
   handle_options ();
   if not (get_bool "server.enabled") && get_string_list "files" = [] then (
     Logs.error "No files for Goblint?";
diff --git a/src/util/std/gobOption.ml b/src/util/std/gobOption.ml
index 55597a8e50..5fb4775b54 100644
--- a/src/util/std/gobOption.ml
+++ b/src/util/std/gobOption.ml
@@ -6,11 +6,18 @@ let for_all p = function
   | Some x -> p x
   | None -> true
 
+let iter = Stdlib.Option.iter
+
 let map2 binop opt1 opt2 =
   match opt1, opt2 with
   | Some x1, Some x2 -> Some (binop x1 x2)
   | _ -> None
 
+let exists2 p opt1 opt2 =
+  match opt1, opt2 with
+  | Some x1, Some x2 -> p x1 x2
+  | _ -> false
+
 (** Open this to use applicative functor/monad syntax for {!option}. *)
 module Syntax =
 struct