diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 8486afb17..03db10a15 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -20,6 +20,11 @@ let equal : t -> t -> bool = Poly.equal
 let compare : t -> t -> int = Poly.compare
 let man = lazy (Box.manager_alloc ())
 let join l r = Abstract1.join (Lazy.force man) l r
+
+let joinN = function
+  | [] -> Abstract1.bottom (Lazy.force man) (Environment.make [||] [||])
+  | x :: xs -> List.fold ~f:join xs x
+
 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 d21b00480..9a10d6857 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -447,9 +447,14 @@ module Make (Config : Config) (D : Domain) (Queue : Queue) = struct
       [%Trace.info
         " %i: %a [%a]@ | %a" depth Edge.pp edge Stack.pp edge.stk Queue.pp
           queue] ;
-      let state, depths =
-        List.fold elts (state, depths) ~f:(fun elt (state, depths) ->
-            (D.join elt.state state, Depths.join elt.depths depths) )
+      let states, depths =
+        List.fold elts
+          ([state], depths)
+          ~f:(fun elt (states, depths) ->
+            (elt.state :: states, Depths.join elt.depths depths) )
+      in
+      let state =
+        D.joinN (List.sort_uniq ~cmp:(Ord.opp D.compare) states)
       in
       (edge, state, depths, queue)
 
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index b0ba8724b..705df0044 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -12,6 +12,7 @@ module type Domain = sig
   val pp : t pp
   val init : Llair.GlobalDefn.t iarray -> t
   val join : t -> t -> t
+  val joinN : t list -> 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 05a8791db..f4e4f9c08 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -39,6 +39,10 @@ module Make (State_domain : State_domain_sig) = struct
     ( State_domain.join entry_a entry_b
     , State_domain.join current_a current_b )
 
+  let joinN rs =
+    let entrys, currents = List.split rs in
+    (State_domain.joinN entrys, State_domain.joinN currents)
+
   let exec_assume (entry, current) cnd =
     let+ next = State_domain.exec_assume current cnd in
     (entry, next)
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index b1564fd50..1509b3905 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -40,6 +40,13 @@ let join p q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
+let joinN qs =
+  [%Trace.call fun {pf} -> pf "@ %a" Sh.pp_djn qs]
+  ;
+  (match qs with [q] -> q | _ -> Sh.orN qs |> simplify)
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
+
 let dnf = Sh.dnf
 
 let exec_assume q b =
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index 8c55da22f..a92acc418 100644
--- a/sledge/src/domain_unit.ml
+++ b/sledge/src/domain_unit.ml
@@ -12,6 +12,7 @@ type t = unit [@@deriving compare, equal, sexp]
 let pp fs () = Format.pp_print_string fs "()"
 let init _ = ()
 let join () () = ()
+let joinN _ = ()
 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 fcecfb7b6..3765bbca4 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -18,6 +18,7 @@ let init globals =
   empty
 
 let join l r = Llair.Global.Set.union l r
+let joinN = function [] -> empty | x :: xs -> List.fold ~f:join xs x
 let recursion_beyond_bound = `skip
 let post _ _ state = state
 let retn _ _ from_call post = Llair.Global.Set.union from_call post
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index c22d10a91..93d3af34c 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -59,6 +59,10 @@ val or_ : t -> t -> t
 (** Disjoin formulas, extending to a common vocabulary, and avoiding
     capturing existentials. *)
 
+val orN : t list -> t
+(** Disjoin formulas, extending to a common vocabulary, and avoiding
+    capturing existentials. *)
+
 val pure : Formula.t -> t
 (** Atomic pure boolean constraint formula. *)