diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 43356788a..aa7b7a9d2 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -9,7 +9,7 @@
 
     The analysis' semantics of control flow. *)
 
-type exec_opts = {bound: int; skip_throw: bool}
+type exec_opts = {bound: int; skip_throw: bool; function_summaries: bool}
 
 module Stack : sig
   type t
@@ -254,19 +254,27 @@ let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) =
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
-    (return : Llair.jump) throw =
+    (return : Llair.jump) throw globals =
   [%Trace.call fun {pf} ->
     pf "%a from %a" Var.pp dst.parent.name.var Var.pp
       return.dst.parent.name.var]
   ;
-  let locals = dst.parent.locals in
-  let state, from_call = Domain.call args dst.params locals state in
-  ( match
-      Stack.push_call ~bound:opts.bound dst ~retreating ~return from_call
-        ?throw stk
-    with
-  | Some stk -> Work.add stk ~prev:block ~retreating state dst
-  | None -> Work.skip )
+  let dnf_states =
+    if opts.function_summaries then Domain.dnf state else [state]
+  in
+  List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
+      let locals = dst.parent.locals in
+      let state, from_call =
+        Domain.call ~summaries:opts.function_summaries args dst.params
+          locals globals state
+      in
+      Work.seq acc
+        ( match
+            Stack.push_call ~bound:opts.bound dst ~retreating ~return
+              from_call ?throw stk
+          with
+        | Some stk -> Work.add stk ~prev:block ~retreating state dst
+        | None -> Work.skip ) )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
@@ -395,7 +403,7 @@ let exec_term :
             | None ->
                 exec_call ~opts stk state block
                   {dst= callee.entry; args; retreating}
-                  return throw )
+                  return throw pgm.globals )
             |> Work.seq x ) )
   | Return {exp} -> exec_return stk state block exp
   | Throw {exc} ->
@@ -423,8 +431,8 @@ let exec_block :
       Report.invalid_access_inst state inst ;
       Work.skip
 
-let harness : Llair.t -> (int -> Work.t) option =
- fun pgm ->
+let harness : opts:exec_opts -> Llair.t -> (int -> Work.t) option =
+ fun ~opts pgm ->
   let entry_points = Config.find_list "entry-points" in
   List.find_map entry_points ~f:(fun name ->
       Llair.Func.find pgm.functions (Var.program name) )
@@ -432,7 +440,9 @@ let harness : Llair.t -> (int -> Work.t) option =
   | Some {locals; entry= {params= []} as block} ->
       Some
         (Work.init
-           (fst (Domain.call [] [] locals (Domain.init pgm.globals)))
+           (fst
+              (Domain.call ~summaries:opts.function_summaries [] [] locals
+                 pgm.globals (Domain.init pgm.globals)))
            block)
   | _ -> None
 
@@ -440,7 +450,7 @@ let exec_pgm : exec_opts -> Llair.t -> unit =
  fun opts pgm ->
   [%Trace.call fun {pf} -> pf "@]@,@["]
   ;
-  ( match harness pgm with
+  ( match harness ~opts pgm with
   | Some work -> Work.run ~f:(exec_block ~opts pgm) (work opts.bound)
   | None -> fail "no applicable harness" () )
   |>
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index 6edfc0b6f..95f3febf3 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -9,6 +9,7 @@
 
 type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
-  ; skip_throw: bool  (** Treat throw as unreachable *) }
+  ; skip_throw: bool  (** Treat throw as unreachable *)
+  ; function_summaries: bool  (** Use function summarisation *) }
 
 val exec_pgm : exec_opts -> Llair.t -> unit
diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml
index a85d1df78..c76149707 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/src/sledge.ml
@@ -66,8 +66,12 @@ let analyze =
   and skip_throw =
     flag "skip-throw" no_arg
       ~doc:"do not explore past throwing an exception"
+  and function_summaries =
+    flag "function-summaries" no_arg
+      ~doc:"Use function summaries (in development)"
   in
-  fun program () -> Control.exec_pgm {bound; skip_throw} (program ())
+  fun program () ->
+    Control.exec_pgm {bound; skip_throw; function_summaries} (program ())
 
 let analyze_cmd =
   let summary = "analyze LLAIR code" in
diff --git a/sledge/src/sledge_buck.ml b/sledge/src/sledge_buck.ml
index c19c08850..3ec2cff86 100644
--- a/sledge/src/sledge_buck.ml
+++ b/sledge/src/sledge_buck.ml
@@ -231,8 +231,8 @@ let main ~(command : unit Command.basic_command) ~analyze =
      //fully/qualified/build:target. The mechanism used to integrate with \
      buck uses the arguments passed to the linker, so the target must \
      specify a binary that will be linked, not for instance a library \
-     archive. Sledge passes the --config sledge.build=True flag to buck, which can \
-     be used to configure buck targets for sledge."
+     archive. Sledge passes the --config sledge.build=True flag to buck, \
+     which can be used to configure buck targets for sledge."
   in
   Command.group ~summary ~readme ~preserve_subcommand_order:()
     [("analyze", analyze_cmd); ("bitcode", bitcode_cmd); ("link", link_cmd)]
diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml
index 20b1b10f2..1a53105e9 100644
--- a/sledge/src/symbheap/domain.ml
+++ b/sledge/src/symbheap/domain.ml
@@ -45,18 +45,27 @@ type from_call =
 [@@deriving sexp_of]
 
 let jump actuals formals ?temps (entry, current) =
-  let current, _ =
-    State_domain.call actuals formals Var.Set.empty ?temps current
-  in
+  let current, _ = State_domain.jump actuals formals ?temps current in
   (entry, current)
 
-let call actuals formals locals (_, current) =
-  [%Trace.call fun {pf} -> pf ""]
+let call ~summaries actuals formals locals globals_vec (_, current) =
+  let globals =
+    Var.Set.of_vector
+      (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
+  in
+  ([%Trace.call fun {pf} ->
+     pf
+       "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
+        globals: {@[%a@]}@ current: %a@]"
+       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
+       (List.rev formals) Var.Set.pp locals Var.Set.pp globals
+       State_domain.pp current]
   ;
-  let current, state_from_call =
-    State_domain.call actuals formals locals current
+  let caller_current, state_from_call =
+    State_domain.call ~summaries actuals formals locals globals current
   in
-  ((current, current), {state_from_call; caller_entry= current})
+  ( (caller_current, caller_current)
+  , {state_from_call; caller_entry= current} ))
   |>
   [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 
@@ -74,5 +83,8 @@ let retn formals {caller_entry; state_from_call} (_, current) =
   |>
   [%Trace.retn fun {pf} -> pf "@,%a" pp]
 
+let dnf (entry, current) =
+  List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current)
+
 let resolve_callee f e (_, current) =
   State_domain.resolve_callee f e current
diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli
index bc4cf0e99..e7c48a83a 100644
--- a/sledge/src/symbheap/domain.mli
+++ b/sledge/src/symbheap/domain.mli
@@ -22,9 +22,19 @@ val exec_intrinsic :
 type from_call [@@deriving sexp_of]
 
 val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t
-val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
+
+val call :
+     summaries:bool
+  -> Exp.t list
+  -> Var.t list
+  -> Var.Set.t
+  -> Global.t vector
+  -> t
+  -> t * from_call
+
 val post : Var.Set.t -> from_call -> t -> t
 val retn : Var.t list -> from_call -> t -> t
+val dnf : t -> t list
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 2ea07fbb9..6a00729fe 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -22,6 +22,11 @@ type t =
             'rep(resentative)' of [a] *) }
 [@@deriving compare, equal, sexp]
 
+let classes r =
+  Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
+      if Exp.equal key data then cls
+      else Map.add_multi cls ~key:data ~data:key )
+
 (** Pretty-printing *)
 
 let pp fs {sat; rep} =
@@ -37,16 +42,12 @@ let pp fs {sat; rep} =
     (Map.to_alist rep)
 
 let pp_classes fs r =
-  let cls =
-    Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
-        if Exp.equal key data then cls
-        else Map.add_multi cls ~key:data ~data:key )
-  in
   List.pp "@ @<2>∧ "
     (fun fs (key, data) ->
       Format.fprintf fs "@[%a@ = %a@]" Exp.pp key (List.pp "@ = " Exp.pp)
         (List.sort ~compare:Exp.compare data) )
-    fs (Map.to_alist cls)
+    fs
+    (Map.to_alist (classes r))
 
 let pp_diff fs (r, s) =
   let pp_sdiff_map pp_elt_diff equal nam fs x y =
@@ -220,6 +221,10 @@ let entails r s =
 
 let normalize = canon
 
+let class_of r e =
+  let e' = normalize r e in
+  e' :: Map.find_multi (classes r) e'
+
 let difference r a b =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
   ;
diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli
index 11e4d2072..cf80ea97b 100644
--- a/sledge/src/symbheap/equality.mli
+++ b/sledge/src/symbheap/equality.mli
@@ -45,11 +45,14 @@ val entails_eq : t -> Exp.t -> Exp.t -> bool
 val entails : t -> t -> bool
 (** Test if one relation entails another. *)
 
+val class_of : t -> Exp.t -> Exp.t list
+(** Equivalence class of [e]: all the expressions in [f] in the relation
+    such that [e = f] is implied by the relation. *)
+
 val normalize : t -> Exp.t -> Exp.t
 (** Normalize an exp [e] to [e'] such that [e = e'] is implied by the
     relation, where [e'] and its sub-exps are expressed in terms of the
-    relation's canonical representatives of each equivalence-modulo-offset
-    class. *)
+    relation's canonical representatives of each equivalence class. *)
 
 val difference : t -> Exp.t -> Exp.t -> Z.t option
 (** The difference as an offset. [difference r a b = Some k] if [r] implies
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index cfa406116..e63fb626f 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -211,6 +211,18 @@ let%test_module _ =
 
       %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
+    let%expect_test _ =
+      printf (List.pp " , " Exp.pp) (Equality.class_of r7 t) ;
+      printf (List.pp " , " Exp.pp) (Equality.class_of r7 x) ;
+      printf (List.pp " , " Exp.pp) (Equality.class_of r7 z) ;
+      [%expect
+        {|
+        %t_1
+
+        %v_3 , %x_5
+
+        %w_4 , %z_7 , %y_6 |}]
+
     let r7' = and_eq x z r7
 
     let%expect_test _ =
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 7b1931bbb..3fae3dd4f 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -404,6 +404,9 @@ let with_pure pure q = {q with pure} |> check invariant
 let rem_seg seg q =
   {q with heap= List.remove_exn q.heap seg} |> check invariant
 
+let filter_heap ~f q =
+  {q with heap= List.filter q.heap ~f} |> check invariant
+
 (** Query *)
 
 let is_emp = function
diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli
index da8b6ef9c..4a64cdcae 100644
--- a/sledge/src/symbheap/sh.mli
+++ b/sledge/src/symbheap/sh.mli
@@ -76,6 +76,9 @@ val rem_seg : seg -> t -> t
     (physically equal to) one of the elements of [q.heap]. Raises if [s] is
     not an element of [q.heap]. *)
 
+val filter_heap : f:(seg -> bool) -> t -> t
+(** [filter_heap q f] Remove all segments in [q] for which [f] returns false *)
+
 (** Quantification and Vocabulary *)
 
 val exists : Var.Set.t -> t -> t
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index b609f8415..24c386048 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -26,6 +26,41 @@ let exec_assume = Exec.assume
 let exec_return = Exec.return
 let exec_inst = Exec.inst
 let exec_intrinsic = Exec.intrinsic
+let dnf = Sh.dnf
+
+let exp_eq_class_has_only_vars_in fvs cong exp =
+  [%Trace.call fun {pf} ->
+    pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,exp: @[%a@]@]" Var.Set.pp fvs
+      Equality.pp cong Exp.pp exp]
+  ;
+  let exp_has_only_vars_in fvs exp = Set.is_subset (Exp.fv exp) ~of_:fvs in
+  let exp_eq_class = Equality.class_of cong exp in
+  List.exists ~f:(exp_has_only_vars_in fvs) exp_eq_class
+  |>
+  [%Trace.retn fun {pf} -> pf "%b"]
+
+let garbage_collect (q : 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 previous == current then current
+    else
+      let new_set =
+        List.fold ~init:current q.heap ~f:(fun current seg ->
+            if exp_eq_class_has_only_vars_in current q.cong seg.loc then
+              List.fold (Equality.class_of q.cong seg.arr) ~init:current
+                ~f:(fun c e -> Set.union c (Exp.fv 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 ->
+      exp_eq_class_has_only_vars_in r_vars q.cong seg.loc )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
 
 type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 
@@ -33,12 +68,36 @@ type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify the temps and
     fresh vars. *)
-let call actuals formals locals ?temps q =
+let jump actuals formals ?temps q =
+  [%Trace.call fun {pf} ->
+    pf "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ q: %a@]"
+      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
+      (List.rev formals) Sh.pp q]
+  ;
+  let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) in
+  let and_eq q formal actual =
+    let actual' = Exp.rename actual freshen_locals in
+    Sh.and_ (Exp.eq (Exp.var formal) actual') q
+  in
+  let and_eqs formals actuals q =
+    List.fold2_exn ~f:and_eq formals actuals ~init:q
+  in
+  ( Option.fold ~f:(Fn.flip Sh.exists) temps
+      ~init:(and_eqs formals actuals q')
+  , freshen_locals )
+  |>
+  [%Trace.retn fun {pf} (q', s) ->
+    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s Sh.pp q']
+
+(** Express formula in terms of formals instead of actuals, and enter scope
+    of locals: rename formals to fresh vars in formula and actuals, add
+    equations between each formal and actual, and quantify fresh vars. *)
+let call ~summaries actuals formals locals globals q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-      (List.rev formals) Var.Set.pp locals Sh.pp q]
+      (List.rev formals) Var.Set.pp locals pp q]
   ;
   let wrt = Set.add_list formals locals in
   let q', freshen_locals = Sh.freshen q ~wrt in
@@ -49,13 +108,39 @@ let call actuals formals locals ?temps q =
   let and_eqs formals actuals q =
     List.fold2_exn ~f:and_eq formals actuals ~init:q
   in
-  ( Sh.extend_us locals
-      (Option.fold ~f:(Fn.flip Sh.exists) temps
-         ~init:(and_eqs formals actuals q'))
-  , freshen_locals )
+  let q'', state_from_call =
+    (Sh.extend_us locals (and_eqs formals actuals q'), freshen_locals)
+  in
+  if summaries then (
+    let formals_set = Var.Set.of_list formals in
+    let non_function_specific_vars =
+      Set.diff (Sh.fv q'') (Set.union formals_set globals)
+    in
+    let function_summary_pre = Sh.exists non_function_specific_vars q'' in
+    let function_summary_pre =
+      garbage_collect function_summary_pre ~wrt:function_summary_pre.us
+    in
+    [%Trace.info "function summary pre %a" pp function_summary_pre] ;
+    let and_eq q formal actual =
+      Sh.and_ (Exp.eq (Exp.var formal) actual) q
+    in
+    (* Replace formals with actuals in the function summary *)
+    let foot =
+      Sh.exists formals_set
+        (List.fold2_exn ~f:and_eq formals actuals ~init:function_summary_pre)
+    in
+    (* Replace formals with actuals in the callsite precondition *)
+    let pre =
+      Sh.exists formals_set
+        (List.fold2_exn ~f:and_eq formals actuals ~init:q'')
+    in
+    let xs, foot = Sh.bind_exists ~wrt:pre.us foot in
+    let frame = Solver.infer_frame pre xs foot in
+    [%Trace.info "Maybe frame %a" (Option.pp "%a" pp) frame] ) ;
+  (q'', state_from_call)
   |>
   [%Trace.retn fun {pf} (q', s) ->
-    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s Sh.pp q']
+    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s pp q']
 
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals q =
@@ -86,3 +171,51 @@ let resolve_callee lookup ptr _ =
   match Var.of_exp ptr with
   | Some callee_name -> lookup callee_name
   | None -> []
+
+let%test_module _ =
+  ( module struct
+    let pp = Format.printf "@.%a@." Sh.pp
+    let wrt = Var.Set.empty
+    let main_, wrt = Var.fresh "main" ~wrt
+    let a_, wrt = Var.fresh "a" ~wrt
+    let n_, wrt = Var.fresh "n" ~wrt
+    let b_, wrt = Var.fresh "b" ~wrt
+    let end_, _ = Var.fresh "end" ~wrt
+    let a = Exp.var a_
+    let main = Exp.var main_
+    let b = Exp.var b_
+    let n = Exp.var n_
+    let endV = Exp.var end_
+    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; arr= a}
+    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= endV}
+    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= main}
+
+    let%expect_test _ =
+      pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ;
+      [%expect {| emp |}]
+
+    let%expect_test _ =
+      pp
+        (garbage_collect (Sh.star seg_a seg_main)
+           ~wrt:(Var.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_])) ;
+      [%expect
+        {|
+          %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩
+        * %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%end_5⟩ |}]
+
+    let%expect_test _ =
+      pp
+        (garbage_collect
+           (Sh.star seg_cycle seg_main)
+           ~wrt:(Var.Set.of_list [a_])) ;
+      [%expect
+        {|
+          %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩
+        * %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%main_1⟩ |}]
+  end )
diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli
index 194e8b4a3..b283530e7 100644
--- a/sledge/src/symbheap/state_domain.mli
+++ b/sledge/src/symbheap/state_domain.mli
@@ -21,16 +21,21 @@ val exec_intrinsic :
 
 type from_call [@@deriving compare, equal, sexp]
 
+val jump :
+  Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t * from_call
+
 val call :
-     Exp.t list
+     summaries:bool
+  -> Exp.t list
   -> Var.t list
   -> Var.Set.t
-  -> ?temps:Var.Set.t
+  -> Var.Set.t
   -> t
   -> t * from_call
 
 val post : Var.Set.t -> t -> t
 val retn : Var.t list -> from_call -> t -> t
+val dnf : t -> t list
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list