diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index d01b0844d..caef8639b 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -223,7 +223,7 @@ let exec_intrinsic ~skip_throw:_ pre aret i _ =
       ; "__cxa_allocate_exception"
       ; "_ZN5folly13usingJEMallocEv" ]
       ~f:(String.equal name)
-  then Option.map ~f:(Option.some << exec_kill pre) aret
+  then Option.map ~f:(Option.return << exec_kill pre) aret
   else None
 
 type from_call = {areturn: Llair.Reg.t option; caller_q: t}
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index c674d3956..89c53bd8e 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -43,7 +43,7 @@ exception Invalid_llvm of string
 let invalid_llvm : string -> 'a =
  fun msg ->
   let first_line =
-    Option.value_map ~default:msg
+    Option.map_or ~default:msg
       ~f:(fun i -> String.take i msg)
       (String.index msg '\n')
   in
@@ -554,7 +554,7 @@ and xlate_opcode stk :
    |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast ->
       convert opcode
   | ICmp -> (
-    match Option.value_exn (Llvm.icmp_predicate llv) with
+    match Option.get_exn (Llvm.icmp_predicate llv) with
     | Eq -> binary Exp.eq
     | Ne -> binary Exp.dq
     | Sgt -> binary Exp.gt
@@ -1187,7 +1187,7 @@ let xlate_instr :
       in
       emit_term ~prefix:(pop loc @ pre) (Term.return ~exp ~loc)
   | Br -> (
-    match Option.value_exn (Llvm.get_branch instr) with
+    match Option.get_exn (Llvm.get_branch instr) with
     | `Unconditional blk ->
         let prefix, dst, blocks = xlate_jump x instr blk loc [] in
         emit_term ~prefix (Term.goto ~dst ~loc) ~blocks
@@ -1567,7 +1567,7 @@ let translate ~models ~fuzzer ~internalize : string list -> Llair.program =
   let link_model_file name =
     Llvm_linker.link_in link_ctx
       (Llvm_irreader.parse_ir llcontext
-         (Llvm.MemoryBuffer.of_string (Option.value_exn (Model.read name))))
+         (Llvm.MemoryBuffer.of_string (Option.get_exn (Model.read name))))
   in
   if models then link_model_file "/cxxabi.bc" ;
   if fuzzer then link_model_file "/lib_fuzzer_main.bc" ;
diff --git a/sledge/cli/sledge_buck.ml b/sledge/cli/sledge_buck.ml
index e4808b2e3..cdfc60295 100644
--- a/sledge/cli/sledge_buck.ml
+++ b/sledge/cli/sledge_buck.ml
@@ -150,7 +150,7 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules =
   let open Process in
   eval ~context
     ( ( if fuzzer then
-        echo ~n:() (Option.value_exn (Model.read "/lib_fuzzer_main.bc"))
+        echo ~n:() (Option.get_exn (Model.read "/lib_fuzzer_main.bc"))
       else return () )
     |- run (Lazy.force llvm_bin ^ "llvm-link") ("-o=-" :: modules)
     |- run
diff --git a/sledge/cli/version.ml b/sledge/cli/version.ml
index 3782af8ad..242c9d679 100644
--- a/sledge/cli/version.ml
+++ b/sledge/cli/version.ml
@@ -17,7 +17,7 @@ let debug =
 module Build_info = Build_info.V1
 
 let version_to_string v =
-  Option.value_map ~f:Build_info.Version.to_string v ~default:"dev"
+  Option.map_or ~f:Build_info.Version.to_string v ~default:"dev"
 
 let version =
   Format.sprintf "%s%s"
diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml
index 88c647667..ffaba1610 100644
--- a/sledge/nonstdlib/NS.ml
+++ b/sledge/nonstdlib/NS.ml
@@ -20,7 +20,7 @@ module Map = Map
 module Monad = Monad
 module Multiset = Multiset
 module Option = Option
-include Option.Import
+include Option.Infix
 module Q = Q_ext
 module Set = Set
 module Sign = Sign
diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli
index e91369c53..1591ce195 100644
--- a/sledge/nonstdlib/NS.mli
+++ b/sledge/nonstdlib/NS.mli
@@ -130,7 +130,7 @@ include module type of Iter.Import
 type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
 
 module Option = Option
-include module type of Option.Import
+include module type of Option.Infix
 
 module Either : sig
   type ('a, 'b) t = Left of 'a | Right of 'b
diff --git a/sledge/nonstdlib/hashTable.ml b/sledge/nonstdlib/hashTable.ml
index 1a1d68202..2f838b702 100644
--- a/sledge/nonstdlib/hashTable.ml
+++ b/sledge/nonstdlib/hashTable.ml
@@ -34,7 +34,7 @@ module Make (Key : HashedType) = struct
       | Some v ->
           found := Some v ;
           Some v ) ;
-    Option.value_exn !found
+    Option.get_exn !found
 
   let iteri tbl ~f = iter (fun key data -> f ~key ~data) tbl
 
diff --git a/sledge/nonstdlib/list.ml b/sledge/nonstdlib/list.ml
index 7f7fcdad1..d6a147c21 100644
--- a/sledge/nonstdlib/list.ml
+++ b/sledge/nonstdlib/list.ml
@@ -13,12 +13,12 @@ exception Not_found_s = Base.Sexp.Not_found_s
 let rec pp ?pre ?suf sep pp_elt fs = function
   | [] -> ()
   | x :: xs ->
-      Option.iter pre ~f:(Format.fprintf fs) ;
+      Option.iter ~f:(Format.fprintf fs) pre ;
       pp_elt fs x ;
       ( match xs with
       | [] -> ()
       | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
-      Option.iter suf ~f:(Format.fprintf fs)
+      Option.iter ~f:(Format.fprintf fs) suf
 
 let findi x xs =
   let rec findi_ i xs =
diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 990754569..c85ba7963 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -105,7 +105,7 @@ end) : S with type key = Key.t = struct
   let length = M.cardinal
   let choose_key = root_key
   let choose = root_binding
-  let choose_exn m = CCOpt.get_exn (choose m)
+  let choose_exn m = Option.get_exn (choose m)
   let min_binding = M.min_binding_opt
   let mem m k = M.mem k m
   let find_exn m k = M.find k m
@@ -141,10 +141,10 @@ end) : S with type key = Key.t = struct
     in
     Option.map ~f:(fun v -> (v, m)) !found
 
-  let pop m = choose m |> CCOpt.map (fun (k, v) -> (k, v, remove m k))
+  let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k))
 
   let pop_min_binding m =
-    min_binding m |> CCOpt.map (fun (k, v) -> (k, v, remove m k))
+    min_binding m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k))
 
   let change m key ~f = M.update key f m
   let update m k ~f = M.update k (fun v -> Some (f v)) m
diff --git a/sledge/nonstdlib/option.ml b/sledge/nonstdlib/option.ml
index 1fa93acc5..a319c519d 100644
--- a/sledge/nonstdlib/option.ml
+++ b/sledge/nonstdlib/option.ml
@@ -6,23 +6,18 @@
  *)
 
 open! NS0
-include Base.Option
+include Containers.Option
+
+type 'a t = 'a option [@@deriving compare, equal, hash, sexp]
 
 let pp fmt pp_elt fs = function
   | Some x -> Format.fprintf fs fmt pp_elt x
   | None -> ()
 
-let or_else ~f = function None -> f () | o -> o
-let cons xo xs = match xo with Some x -> x :: xs | None -> xs
-
-module Monad_syntax = struct
-  let ( let+ ) x f = map ~f x
-  let ( and+ ) x y = both x y
-  let ( let* ) x f = bind ~f x
-  let ( and* ) x y = both x y
-end
-
-module Import = struct
-  include Monad_infix
-  include Monad_syntax
-end
+let map xo ~f = map f xo
+let map_or xo ~default ~f = map_or ~default f xo
+let bind xo ~f = bind xo f
+let iter xo ~f = iter f xo
+let exists xo ~f = exists f xo
+let for_all xo ~f = for_all f xo
+let fold xo ~init ~f = fold f init xo
diff --git a/sledge/nonstdlib/option.mli b/sledge/nonstdlib/option.mli
index caf9d8c8c..92cb6838c 100644
--- a/sledge/nonstdlib/option.mli
+++ b/sledge/nonstdlib/option.mli
@@ -6,17 +6,15 @@
  *)
 
 open! NS0
-include module type of Base.Option
+include module type of Containers.Option
 
-val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp
-(** Pretty-print an option. *)
-
-val or_else : f:(unit -> 'a option) -> 'a option -> 'a option
-(** [or_else ~f] is [f ()] on [None] and otherwise identity *)
+type 'a t = 'a option [@@deriving compare, equal, hash, sexp]
 
-val cons : 'a t -> 'a list -> 'a list
-
-module Import : sig
-  include Monad_syntax with type 'a t := 'a option
-  include module type of Monad_infix
-end
+val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp
+val map : 'a t -> f:('a -> 'b) -> 'b t
+val map_or : 'a t -> default:'b -> f:('a -> 'b) -> 'b
+val bind : 'a t -> f:('a -> 'b t) -> 'b t
+val iter : 'a t -> f:('a -> unit) -> unit
+val exists : 'a t -> f:('a -> bool) -> bool
+val for_all : 'a t -> f:('a -> bool) -> bool
+val fold : 'a t -> init:'s -> f:('s -> 'a -> 's) -> 's
diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml
index 9261637b8..7c9d94550 100644
--- a/sledge/nonstdlib/set.ml
+++ b/sledge/nonstdlib/set.ml
@@ -6,7 +6,6 @@
  *)
 
 open! NS0
-module Option = CCOpt
 include Set_intf
 
 module Make (Elt : sig
@@ -29,10 +28,10 @@ end) : S with type elt = Elt.t = struct
 
   let empty = S.empty
   let of_ = S.singleton
-  let of_option xo = Option.map_or S.singleton xo ~default:empty
+  let of_option xo = Option.map_or ~f:S.singleton xo ~default:empty
   let of_list = S.of_list
   let add s x = S.add x s
-  let add_option xo s = Option.fold add s xo
+  let add_option xo s = Option.fold ~f:add ~init:s xo
   let add_list xs s = S.add_list s xs
   let diff = S.diff
   let inter = S.inter
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 9c2f8db99..234438462 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -126,7 +126,7 @@ let localize_entry globals actuals formals freturn locals shadow pre entry =
   let foot = Sh.exists formals_set function_summary_pre in
   let xs, foot = Sh.bind_exists ~wrt:pre.Sh.us foot in
   let frame =
-    try Option.value_exn (Solver.infer_frame pre xs foot)
+    try Option.get_exn (Solver.infer_frame pre xs foot)
     with _ ->
       fail "Solver couldn't infer frame of a garbage-collected pre" ()
   in
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index a5e47b368..d96ae5e70 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -630,7 +630,7 @@ let strlen_spec reg ptr =
  * Symbolic Execution
  *)
 
-open Option.Import
+open Option.Infix
 
 let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
   let gain_us = Var.Set.diff q1.us q0.us in
diff --git a/sledge/src/llair/loc.ml b/sledge/src/llair/loc.ml
index 3245b4a39..35647bec1 100644
--- a/sledge/src/llair/loc.ml
+++ b/sledge/src/llair/loc.ml
@@ -22,7 +22,7 @@ let pp fs ({dir; file; line; col} as loc) =
   if not (equal loc none) then Format.pp_print_string fs "; " ;
   if not (String.is_empty dir) then (
     let dir =
-      Option.value_map ~f:Fpath.to_string
+      Option.map_or ~f:Fpath.to_string
         (Fpath.relativize ~root:(Fpath.v !root) (Fpath.v dir))
         ~default:dir
     in
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index f12eb5edf..73226ac3b 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -320,7 +320,7 @@ and solve_ ?f d e s =
 let solve ?f ~us ~xs d e =
   [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp d Term.pp e]
   ;
-  (solve_ ?f d e (us, xs, Subst.empty) >>| fun (_, xs, s) -> (xs, s))
+  (solve_ ?f d e (us, xs, Subst.empty) >|= fun (_, xs, s) -> (xs, s))
   |>
   [%Trace.retn fun {pf} ->
     function
@@ -443,8 +443,8 @@ let invariant r =
 
 let true_ =
   let rep = Subst.empty in
-  let rep = Option.value_exn (Subst.extend Term.true_ rep) in
-  let rep = Option.value_exn (Subst.extend Term.false_ rep) in
+  let rep = Option.get_exn (Subst.extend Term.true_ rep) in
+  let rep = Option.get_exn (Subst.extend Term.false_ rep) in
   {xs= Var.Set.empty; sat= true; rep} |> check invariant
 
 let false_ = {true_ with sat= false}