diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 5bb89b956..8486afb17 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -19,7 +19,7 @@ type t = Box.t Abstract1.t
 let equal : t -> t -> bool = Poly.equal
 let compare : t -> t -> int = Poly.compare
 let man = lazy (Box.manager_alloc ())
-let join l r = Some (Abstract1.join (Lazy.force man) l r)
+let join l r = Abstract1.join (Lazy.force man) l r
 let is_false x = Abstract1.is_bottom (Lazy.force man) x
 
 let bindings (itv : t) =
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index b50c3777f..9f8461f9e 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -267,12 +267,10 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
       let state, depths, queue =
         List.fold elts (state, depths, queue)
           ~f:(fun elt (state, depths, queue) ->
-            match Dom.join elt.state state with
-            | Some state ->
-                let depths = Depths.join elt.depths depths in
-                let queue = PrioQueue.remove elt queue in
-                (state, depths, queue)
-            | None -> (state, depths, queue) )
+            let state = Dom.join elt.state state in
+            let depths = Depths.join elt.depths depths in
+            let queue = PrioQueue.remove elt queue in
+            (state, depths, queue) )
       in
       (edge, state, depths, queue)
 
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index 28eb833bc..d373aab82 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -11,7 +11,7 @@ module type Dom = sig
 
   val pp : t pp
   val init : Llair.GlobalDefn.t iarray -> t
-  val join : t -> t -> t option
+  val join : t -> t -> t
   val dnf : t -> t list
   val exec_assume : t -> Llair.Exp.t -> t option
   val exec_kill : Llair.Reg.t -> t -> t
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index aab6d660a..65dbddd89 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -34,10 +34,8 @@ module Make (State_domain : State_domain_sig) = struct
   let init globals = embed (State_domain.init globals)
 
   let join (entry_a, current_a) (entry_b, current_b) =
-    if State_domain.equal entry_a entry_b then
-      let+ next = State_domain.join current_a current_b in
-      (entry_a, next)
-    else None
+    assert (State_domain.equal entry_a entry_b) ;
+    (entry_a, State_domain.join current_a current_b)
 
   let exec_assume (entry, current) cnd =
     let+ next = State_domain.exec_assume current cnd in
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index ac970b1e0..d6f2f9139 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -36,9 +36,9 @@ let init globals =
 let join p q =
   [%Trace.call fun {pf} -> pf "@ %a@ %a" pp p pp q]
   ;
-  Some (Sh.or_ p q) |> Option.map ~f:simplify
+  Sh.or_ p q |> simplify
   |>
-  [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" pp)]
+  [%Trace.retn fun {pf} -> pf "%a" pp]
 
 let dnf = Sh.dnf
 
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index 48fbece28..8c55da22f 100644
--- a/sledge/src/domain_unit.ml
+++ b/sledge/src/domain_unit.ml
@@ -11,7 +11,7 @@ type t = unit [@@deriving compare, equal, sexp]
 
 let pp fs () = Format.pp_print_string fs "()"
 let init _ = ()
-let join () () = Some ()
+let join () () = ()
 let exec_assume () _ = Some ()
 let exec_kill _ () = ()
 let exec_move _ () = ()
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 72fcc9ac1..016624e19 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -17,7 +17,7 @@ let init globals =
     " globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ;
   empty
 
-let join l r = Some (Llair.Global.Set.union l r)
+let join l r = Llair.Global.Set.union l r
 let recursion_beyond_bound = `skip
 let post _ _ state = state
 let retn _ _ from_call post = Llair.Global.Set.union from_call post