diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 60fed440c..d3618f0fe 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -73,39 +73,30 @@ let exec_intrinsic ~skip_throw r i es q =
     (List.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
-let term_eq_class_has_only_vars_in fvs ctx term =
-  [%Trace.call fun {pf} ->
-    pf "@[<v> fvs: @[%a@] @,ctx: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
-      Context.pp ctx Term.pp term]
-  ;
-  let term_has_only_vars_in fvs term =
-    Var.Set.subset (Term.fv term) ~of_:fvs
-  in
-  let term_eq_class = Context.class_of ctx term in
-  List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
-  |>
-  [%Trace.retn fun {pf} -> pf "%b"]
+let value_determined_by ctx us a =
+  List.exists (Context.class_of ctx a) ~f:(fun b ->
+      Term.Set.subset (Term.Set.of_iter (Term.atoms b)) ~of_:us )
 
-let garbage_collect (q : t) ~wrt =
+let garbage_collect (q : Sh.t) ~wrt =
   [%Trace.call fun {pf} -> pf "%a" pp q]
   ;
   (* only support DNF for now *)
   assert (List.is_empty q.djns) ;
   let rec all_reachable_vars previous current (q : t) =
-    if Var.Set.equal previous current then current
+    if Term.Set.equal previous current then current
     else
       let new_set =
         List.fold q.heap current ~f:(fun seg current ->
-            if term_eq_class_has_only_vars_in current q.ctx seg.loc then
+            if value_determined_by q.ctx current seg.loc then
               List.fold (Context.class_of q.ctx seg.seq) current
-                ~f:(fun e c -> Var.Set.union c (Term.fv e))
+                ~f:(fun e c ->
+                  Term.Set.union c (Term.Set.of_iter (Term.atoms e)) )
             else current )
       in
       all_reachable_vars current new_set q
   in
-  let r_vars = all_reachable_vars Var.Set.empty wrt q in
-  Sh.filter_heap q ~f:(fun seg ->
-      term_eq_class_has_only_vars_in r_vars q.ctx seg.loc )
+  let r_vars = all_reachable_vars Term.Set.empty wrt q in
+  Sh.filter_heap q ~f:(fun seg -> value_determined_by q.ctx r_vars seg.loc)
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
@@ -120,10 +111,14 @@ let localize_entry globals actuals formals freturn locals shadow pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
   let formals_set = Var.Set.of_list formals in
   let freturn_locals = X.regs (Llair.Reg.Set.add_option freturn locals) in
-  let function_summary_pre =
-    garbage_collect entry
-      ~wrt:(Var.Set.union formals_set (X.globals globals))
+  let wrt =
+    Term.Set.of_iter
+      (Iter.append
+         (Iter.map ~f:(Term.var << X.global)
+            (Llair.Global.Set.to_iter globals))
+         (Iter.map ~f:Term.var (List.to_iter formals)))
   in
+  let function_summary_pre = garbage_collect entry ~wrt in
   [%Trace.info "function summary pre %a" pp function_summary_pre] ;
   let foot = Sh.exists formals_set function_summary_pre in
   let xs, foot = Sh.bind_exists ~wrt:pre.Sh.us foot in
@@ -332,19 +327,19 @@ let%test_module _ =
     let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main}
 
     let%expect_test _ =
-      pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ;
+      pp (garbage_collect seg_main ~wrt:(Term.Set.of_list [])) ;
       [%expect {| emp |}]
 
     let%expect_test _ =
       pp
         (garbage_collect (Sh.star seg_a seg_main)
-           ~wrt:(Var.Set.of_list [a_])) ;
+           ~wrt:(Term.Set.of_list [a])) ;
       [%expect {| %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%end_5⟩ |}]
 
     let%expect_test _ =
       pp
         (garbage_collect (Sh.star seg_a seg_main)
-           ~wrt:(Var.Set.of_list [main_])) ;
+           ~wrt:(Term.Set.of_list [main])) ;
       [%expect
         {|
           %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩
@@ -354,7 +349,7 @@ let%test_module _ =
       pp
         (garbage_collect
            (Sh.star seg_cycle seg_main)
-           ~wrt:(Var.Set.of_list [a_])) ;
+           ~wrt:(Term.Set.of_list [a])) ;
       [%expect
         {|
           %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩
diff --git a/sledge/src/fol/exp.ml b/sledge/src/fol/exp.ml
index 81f857f11..df24f3434 100644
--- a/sledge/src/fol/exp.ml
+++ b/sledge/src/fol/exp.ml
@@ -196,6 +196,7 @@ module Term = struct
   end
 
   include T
+  module Set = Set.Make (T)
   module Map = Map.Make (T)
 
   let ppx = ppx
@@ -269,6 +270,7 @@ module Term = struct
     match e with `Fml f -> iter_f f | #cnd as c -> iter_c c
 
   let vars = iter ~f:Trm.vars
+  let atoms = iter ~f:(fun e -> Iter.map ~f:(fun a -> `Trm a) (Trm.atoms e))
 
   (** Transform *)
 
diff --git a/sledge/src/fol/exp.mli b/sledge/src/fol/exp.mli
index a394a949f..4bfba9e70 100644
--- a/sledge/src/fol/exp.mli
+++ b/sledge/src/fol/exp.mli
@@ -13,6 +13,7 @@ module rec Term : sig
   val ppx : Var.strength -> t pp
   val pp : t pp
 
+  module Set : Set.S with type elt := t
   module Map : Map.S with type key := t
 
   (** Construct *)
@@ -78,6 +79,7 @@ module rec Term : sig
   (** Traverse *)
 
   val vars : t -> Var.t iter
+  val atoms : t -> t iter
 
   (** Transform *)
 
diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index 29f17f921..d00459e33 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -437,6 +437,13 @@ let trms = function
       Iter.(cons x (cons y (cons z empty)))
   | Concat xs | Apply (_, xs) -> Iter.of_array xs
 
+let is_atomic = function
+  | Var _ | Z _ | Q _ | Concat [||] | Apply (_, [||]) -> true
+  | Arith _ | Splat _ | Sized _ | Extract _ | Concat _ | Apply _ -> false
+
+let rec atoms e =
+  if is_atomic e then Iter.return e else Iter.flat_map ~f:atoms (trms e)
+
 (** Query *)
 
 let fv e = Var.Set.of_iter (vars e)
diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli
index 14a0dbe9b..d2d05d002 100644
--- a/sledge/src/fol/trm.mli
+++ b/sledge/src/fol/trm.mli
@@ -89,8 +89,9 @@ val map : t -> f:(t -> t) -> t
 
 val seq_size_exn : t -> t
 val seq_size : t -> t option
-val fv : t -> Var.Set.t
+val is_atomic : t -> bool
 val height : t -> int
+val fv : t -> Var.Set.t
 
 (** Traverse *)
 
@@ -99,3 +100,6 @@ val trms : t -> t iter
 
 val vars : t -> Var.t iter
 (** The variables that occur in a term. *)
+
+val atoms : t -> t iter
+(** The atomic reflexive-transitive subterms of a term. *)