diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index af1e06546..d61b1c2e7 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -170,9 +170,9 @@ module Make (Dom : Domain_sig.Dom) = struct
       include Comparator.Make (T)
 
       let pp fs {dst; src} =
-        Format.fprintf fs "#%i %s <--%a" dst.sort_index dst.lbl
+        Format.fprintf fs "#%i %%%s <--%a" dst.sort_index dst.lbl
           (Option.pp "%a" (fun fs (src : Llair.Block.t) ->
-               Format.fprintf fs " #%i %s" src.sort_index src.lbl ))
+               Format.fprintf fs " #%i %%%s" src.sort_index src.lbl ))
           src
     end
 
@@ -383,7 +383,8 @@ module Make (Dom : Domain_sig.Dom) = struct
   let exec_term :
       exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x =
    fun opts pgm stk state block ->
-    [%Trace.info "exec %a" Llair.Term.pp block.term] ;
+    [%Trace.info
+      "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
     match block.term with
     | Switch {key; tbl; els} ->
         Vector.fold tbl
@@ -446,12 +447,14 @@ module Make (Dom : Domain_sig.Dom) = struct
   let exec_inst : Dom.t -> Llair.inst -> (Dom.t, Dom.t * Llair.inst) result
       =
    fun state inst ->
+    [%Trace.info
+      "@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ;
     Dom.exec_inst state inst |> Result.of_option ~error:(state, inst)
 
   let exec_block :
       exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x =
    fun opts pgm stk state block ->
-    [%Trace.info "exec %a" Llair.Block.pp block] ;
+    [%Trace.info "exec block %%%s" block.lbl] ;
     match Vector.fold_result ~f:exec_inst ~init:state block.cmnd with
     | Ok state -> exec_term opts pgm stk state block
     | Error (state, inst) ->
@@ -476,13 +479,9 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let exec_pgm : exec_opts -> Llair.t -> unit =
    fun opts pgm ->
-    [%Trace.call fun {pf} -> pf "@]@,@["]
-    ;
-    ( match harness opts pgm with
+    match harness opts pgm with
     | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound)
-    | None -> fail "no applicable harness" () )
-    |>
-    [%Trace.retn fun {pf} _ -> pf ""]
+    | None -> fail "no applicable harness" ()
 
   let compute_summaries opts pgm : Dom.summary list Reg.Map.t =
     assert opts.function_summaries ;
diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml
index a73aa0177..957a72080 100644
--- a/sledge/src/domain/relation.ml
+++ b/sledge/src/domain/relation.ml
@@ -24,9 +24,11 @@ module Make (State_domain : State_domain_sig) = struct
 
   let embed b = (b, b)
 
+  let pp_entry fs entry =
+    [%Trace.fprintf fs "entry: %a@ current: " State_domain.pp entry]
+
   let pp fs (entry, curr) =
-    Format.fprintf fs "@[<v>entry: %a@ current: %a@]" State_domain.pp entry
-      State_domain.pp curr
+    Format.fprintf fs "@[%a%a@]" pp_entry entry State_domain.pp curr
 
   let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr
   let init globals = embed (State_domain.init globals)
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index e42cf6930..b8c643cb1 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -198,8 +198,8 @@ let pp_term fs term =
 let pp_cmnd = Vector.pp "@ " pp_inst
 
 let pp_block fs {lbl; cmnd; term; parent= _; sort_index} =
-  Format.fprintf fs "@[<v 2>%s: #%i@ @[<v>%a%t%a@]@]" lbl sort_index pp_cmnd
-    cmnd
+  Format.fprintf fs "@[<v 2>%%%s: #%i@ @[<v>%a%t%a@]@]" lbl sort_index
+    pp_cmnd cmnd
     (fun fs -> if Vector.is_empty cmnd then () else Format.fprintf fs "@ ")
     pp_term term
 
diff --git a/sledge/src/llair/loc.ml b/sledge/src/llair/loc.ml
index 4dc0367e2..4237d4425 100644
--- a/sledge/src/llair/loc.ml
+++ b/sledge/src/llair/loc.ml
@@ -28,3 +28,5 @@ let pp fs {dir; file; line; col} =
   if col > 0 then (
     Format.pp_print_int fs col ;
     Format.pp_print_char fs ':' )
+
+let pp fs l = Format.pp_print_as fs 0 (Format.asprintf "%a" pp l)
diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 02f9374a1..03ccf4185 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -140,24 +140,21 @@ let fix (f : (t -> 'a as 'f) -> 'f) (bot : 'f) (e : t) : 'a =
 let fix_flip (f : ('z -> t -> 'a as 'f) -> 'f) (bot : 'f) (z : 'z) (e : t) =
   fix (fun f' e z -> f (fun z e -> f' e z) z e) (fun e z -> bot z e) e z
 
-let rec pp ?is_x fs term =
-  let get_var_style var =
-    match is_x with
-    | None -> `None
-    | Some is_x -> if not (is_x var) then `Bold else `Cyan
-  in
+let rec ppx strength fs term =
   let pp_ pp fs term =
     let pf fmt =
       Format.pp_open_box fs 2 ;
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match term with
-    | Var {name; id= -1} as var ->
-        Trace.pp_styled (get_var_style var) "%@%s" fs name
-    | Var {name; id= 0} as var ->
-        Trace.pp_styled (get_var_style var) "%%%s" fs name
-    | Var {name; id} as var ->
-        Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id
+    | Var {name; id= -1} -> Trace.pp_styled `Bold "%@%s" fs name
+    | Var {name; id= 0} -> Trace.pp_styled `Bold "%%%s" fs name
+    | Var {name; id} -> (
+      match strength term with
+      | None -> pf "%%%s_%d" name id
+      | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" fs name id
+      | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" fs name id
+      | Some `Anonymous -> Trace.pp_styled `Cyan "_" fs )
     | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
     | Float {data} -> pf "%s" data
     | Nondet {msg} -> pf "nondet \"%s\"" msg
@@ -202,7 +199,7 @@ let rec pp ?is_x fs term =
     | Ap2 (Splat, byt, siz) -> pf "%a^%a" pp byt pp siz
     | Ap2 (Memory, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
     | ApN (Concat, args) -> pf "%a" (Vector.pp "@,^" pp) args
-    | ApN (Record, elts) -> pf "{%a}" pp_record elts
+    | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts
     | RecN (Record, elts) -> pf "{|%a|}" (Vector.pp ",@ " pp) elts
     | Ap1 (Select idx, rcd) -> pf "%a[%i]" pp rcd idx
     | Ap2 (Update idx, rcd, elt) ->
@@ -211,7 +208,7 @@ let rec pp ?is_x fs term =
   fix_flip pp_ (fun _ _ -> ()) fs term
   [@@warning "-9"]
 
-and pp_record fs elts =
+and pp_record strength fs elts =
   [%Trace.fprintf
     fs "%a"
       (fun fs elts ->
@@ -223,12 +220,13 @@ and pp_record fs elts =
         with
         | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
         | exception _ ->
-            Format.fprintf fs "@[<h>%a@]" (Vector.pp ",@ " pp) elts )
+            Format.fprintf fs "@[<h>%a@]"
+              (Vector.pp ",@ " (ppx strength))
+              elts )
       elts]
 
-let pp_t = pp ?is_x:None
-let pp_full = pp
-let pp = pp_t
+let pp = ppx (fun _ -> None)
+let pp_t = pp
 
 (** Invariant *)
 
@@ -304,6 +302,8 @@ module Var = struct
 
   let pp = pp
 
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
+
   module Map = Map
 
   module Set = struct
@@ -313,8 +313,13 @@ module Var = struct
 
     type t = Set.M(T).t [@@deriving compare, equal, sexp]
 
-    let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs
-    let pp = pp_full ?is_x:None
+    let pp vs = Set.pp pp_t vs
+    let ppx strength vs = Set.pp (ppx strength) vs
+
+    let pp_xs fs xs =
+      if not (is_empty xs) then
+        Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
+
     let empty = Set.empty (module T)
     let of_ = Set.add empty
     let of_option = Option.fold ~f:Set.add ~init:empty
diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli
index 3c7318e44..711b5df06 100644
--- a/sledge/src/llair/term.mli
+++ b/sledge/src/llair/term.mli
@@ -82,11 +82,6 @@ and t = private
   | Integer of {data: Z.t}  (** Integer constant *)
 [@@deriving compare, equal, hash, sexp]
 
-val comparator : (t, comparator_witness) Comparator.t
-val pp_full : ?is_x:(t -> bool) -> t pp
-val pp : t pp
-val invariant : t -> unit
-
 (** Term.Var is re-exported as Var *)
 module Var : sig
   type term := t
@@ -94,14 +89,17 @@ module Var : sig
 
   include Comparator.S with type t := t
 
+  type strength = t -> [`Universal | `Existential | `Anonymous] option
+
   module Set : sig
     type var := t
 
     type t = (var, comparator_witness) Set.t
     [@@deriving compare, equal, sexp]
 
-    val pp_full : ?is_x:(term -> bool) -> t pp
+    val ppx : strength -> t pp
     val pp : t pp
+    val pp_xs : t pp
     val empty : t
     val of_ : var -> t
     val of_option : var option -> t
@@ -154,6 +152,11 @@ module Map : sig
   val empty : 'a t
 end
 
+val comparator : (t, comparator_witness) Comparator.t
+val ppx : Var.strength -> t pp
+val pp : t pp
+val invariant : t -> unit
+
 (** Construct *)
 
 (* variables *)
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 550841549..18acd75b9 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -50,15 +50,6 @@ let pp fs {sat; rep} =
     (pp_alist Term.pp pp_term_v)
     (Map.to_alist rep)
 
-let pp_classes ?is_x fs r =
-  List.pp "@ @<2>∧ "
-    (fun fs (key, data) ->
-      Format.fprintf fs "@[%a@ = %a@]" (Term.pp_full ?is_x) key
-        (List.pp "@ = " (Term.pp_full ?is_x))
-        (List.sort ~compare:Term.compare data) )
-    fs
-    (Map.to_alist (classes r))
-
 let pp_diff fs (r, s) =
   let pp_sdiff_map pp_elt_diff equal nam fs x y =
     let sd = Sequence.to_list (Map.symmetric_diff ~data_equal:equal x y) in
@@ -313,3 +304,29 @@ let fold_vars r ~init ~f =
   fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
 let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty
+
+let pp_classes x fs r =
+  List.pp "@ @<2>∧ "
+    (fun fs (key, data) ->
+      Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) key
+        (List.pp "@ = " (Term.ppx x))
+        (List.sort ~compare:Term.compare data) )
+    fs
+    (Map.to_alist (classes r))
+
+let pp_classes_diff x fs (r, s) =
+  let clss = classes s in
+  let clss =
+    Map.filter_mapi clss ~f:(fun ~key:rep ~data:cls ->
+        match
+          List.filter cls ~f:(fun exp -> not (entails_eq r rep exp))
+        with
+        | [] -> None
+        | cls -> Some cls )
+  in
+  List.pp "@ @<2>∧ "
+    (fun fs (rep, cls) ->
+      Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep
+        (List.pp "@ = " (Term.ppx x))
+        (List.sort ~compare:Term.compare cls) )
+    fs (Map.to_alist clss)
diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli
index 67e8eb551..3d78ebda8 100644
--- a/sledge/src/symbheap/equality.mli
+++ b/sledge/src/symbheap/equality.mli
@@ -11,7 +11,8 @@
 type t [@@deriving compare, equal, sexp]
 
 val pp : t pp
-val pp_classes : ?is_x:(Term.t -> bool) -> t pp
+val pp_classes : Var.strength -> t pp
+val pp_classes_diff : Var.strength -> (t * t) pp
 
 include Invariant.S with type t := t
 
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index d0e5563ff..4cf4471c3 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -14,7 +14,10 @@ let%test_module _ =
     (* let () = Trace.init ~margin:160 ~config:all () *)
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
-    let pp_classes = printf pp_classes
+
+    let pp_classes =
+      Format.printf "@\n@[<hv>  %a@]@." (pp_classes (fun _ -> None))
+
     let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
     let ( ! ) i = Term.integer (Z.of_int i)
     let ( + ) = Term.add
@@ -84,7 +87,7 @@ let%test_module _ =
       pp r1 ;
       [%expect
         {|
-          %x_5 = %y_6
+            %x_5 = %y_6
 
           {sat= true; rep= [[%y_6 ↦ %x_5]]} |}]
 
@@ -97,7 +100,7 @@ let%test_module _ =
       pp r2 ;
       [%expect
         {|
-          %x_5 = %y_6 = %z_7 = ((u8) %x_5)
+            %x_5 = %y_6 = %z_7 = ((u8) %x_5)
 
           {sat= true;
            rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((u8) %x_5) ↦ %x_5]]} |}]
@@ -140,8 +143,8 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %t_1)
-      = (%y_6 rem %t_1)
+        %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %t_1)
+        = (%y_6 rem %t_1)
 
       {sat= true;
        rep= [[%u_2 ↦ %t_1];
@@ -163,8 +166,7 @@ let%test_module _ =
       pp r4 ;
       [%expect
         {|
-      (%z_7 + -4) = %y_6 ∧ (%z_7 + 3) = %w_4
-      ∧ (%z_7 + 8) = %x_5
+        (%z_7 + -4) = %y_6 ∧ (%z_7 + 3) = %w_4 ∧ (%z_7 + 8) = %x_5
 
       {sat= true;
        rep= [[%w_4 ↦ (%z_7 + 3)];
@@ -186,7 +188,7 @@ let%test_module _ =
       pp r6 ;
       [%expect
         {|
-      1 = %x_5 = %y_6
+        1 = %x_5 = %y_6
 
       {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}]
 
@@ -201,15 +203,14 @@ let%test_module _ =
       pp_classes (and_eq x z r7) ;
       [%expect
         {|
-      %v_3 = %x_5
-      ∧ %w_4 = %y_6 = %z_7
+        %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
 
       {sat= true; rep= [[%x_5 ↦ %v_3]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
 
       {sat= true;
        rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]}
 
-      %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
+        %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
     let%expect_test _ =
       printf (List.pp " , " Term.pp) (Equality.class_of r7 t) ;
@@ -230,7 +231,7 @@ let%test_module _ =
       pp r7' ;
       [%expect
         {|
-      %v_3 = %w_4 = %x_5 = %y_6 = %z_7
+        %v_3 = %w_4 = %x_5 = %y_6 = %z_7
 
       {sat= true;
        rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]} |}]
@@ -250,8 +251,7 @@ let%test_module _ =
       pp r8 ;
       [%expect
         {|
-      (13 × %z_7) = %x_5
-      ∧ 14 = %y_6
+        (13 × %z_7) = %x_5 ∧ 14 = %y_6
 
       {sat= true; rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]]} |}]
 
@@ -264,7 +264,7 @@ let%test_module _ =
       pp r9 ;
       [%expect
         {|
-       (%z_7 + -16) = %x_5
+         (%z_7 + -16) = %x_5
 
        {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]]} |}]
 
@@ -281,7 +281,7 @@ let%test_module _ =
       Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ;
       [%expect
         {|
-      (%z_7 + -16) = %x_5
+        (%z_7 + -16) = %x_5
 
       {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]]}
 
@@ -390,6 +390,7 @@ let%test_module _ =
                [((u8) %x_5) ↦ %x_5];
                [((u8) %y_6) ↦ ]]}
 
-        (((u8) %y_6) + 1) = %y_6 ∧ %x_5 = ((u8) %x_5)
+          (((u8) %y_6) + 1) = %y_6
+        ∧ %x_5 = ((u8) %x_5)
         ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}]
   end )
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 167ad640a..33f50428d 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -28,8 +28,38 @@ type t = starjunction [@@deriving compare, equal, sexp]
 let map_seg {loc; bas; len; siz; arr} ~f =
   {loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}
 
-let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
-  let term_pp = Term.pp_full ?is_x in
+let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
+  let f b s = f s b in
+  f loc (f bas (f len (f siz (f arr init))))
+
+let fold_vars_seg seg ~init ~f =
+  fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
+
+let fold_vars fold_vars {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
+  Equality.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
+  |> fun init ->
+  List.fold ~init pure ~f:(fun init -> Term.fold_vars ~f ~init)
+  |> fun init ->
+  List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
+  |> fun init ->
+  List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
+
+let var_strength q =
+  let rec var_strength_ xs m q =
+    let xs = Set.union xs q.xs in
+    fold_vars (var_strength_ xs) {q with cong= Equality.true_} ~init:m
+      ~f:(fun m var ->
+        if not (Set.mem xs var) then Map.set m ~key:var ~data:`Universal
+        else
+          match Map.find m var with
+          | None -> Map.set m ~key:var ~data:`Anonymous
+          | Some `Anonymous -> Map.set m ~key:var ~data:`Existential
+          | Some _ -> m )
+  in
+  var_strength_ Var.Set.empty Var.Map.empty q
+
+let pp_seg x fs {loc; bas; len; siz; arr} =
+  let term_pp = Term.ppx x in
   Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
     (fun fs (bas, len) ->
       if (not (Term.equal loc bas)) || not (Term.equal len siz) then
@@ -37,9 +67,10 @@ let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
     (bas, len) term_pp (Term.memory ~siz ~arr)
 
 let pp_seg_norm cong fs seg =
-  pp_seg fs (map_seg seg ~f:(Equality.normalize cong))
+  let x _ = None in
+  pp_seg x fs (map_seg seg ~f:(Equality.normalize cong))
 
-let pp_block ?is_x fs segs =
+let pp_block x fs segs =
   let is_full_alloc segs =
     match segs with
     | {loc; bas; len; _} :: _ -> (
@@ -58,7 +89,7 @@ let pp_block ?is_x fs segs =
         | _ -> false )
     | [] -> false
   in
-  let term_pp = Term.pp_full ?is_x in
+  let term_pp = Term.ppx x in
   let pp_mems =
     List.pp "@,^" (fun fs seg ->
         term_pp fs (Term.memory ~siz:seg.siz ~arr:seg.arr) )
@@ -72,7 +103,7 @@ let pp_block ?is_x fs segs =
         pp_mems segs
   | [] -> ()
 
-let pp_heap ?is_x ?pre cong fs heap =
+let pp_heap x ?pre cong fs heap =
   let bas_off = function
     | Term.Add poly as sum ->
         let const = Qset.count poly Term.one in
@@ -81,92 +112,90 @@ let pp_heap ?is_x ?pre cong fs heap =
   in
   let compare s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]
-      (s1.bas, bas_off s1.loc)
-      (s2.bas, bas_off s2.loc)
+      ( Equality.normalize cong s1.bas
+      , bas_off (Equality.normalize cong s1.loc) )
+      ( Equality.normalize cong s2.bas
+      , bas_off (Equality.normalize cong s2.loc) )
   in
   let break s1 s2 =
     (not (Term.equal s1.bas s2.bas))
     || (not (Term.equal s1.len s2.len))
-    || not (Term.is_constant (Term.sub s2.loc s1.loc))
-  in
-  let blocks =
-    List.group ~break
-      (List.sort ~compare
-         (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap))
+    || not (Equality.entails_eq cong (Term.add s1.loc s1.siz) s2.loc)
   in
-  List.pp ?pre "@ * " (pp_block ?is_x) fs blocks
+  let heap = List.map heap ~f:(map_seg ~f:(Equality.normalize cong)) in
+  let blocks = List.group ~break (List.sort ~compare heap) in
+  List.pp ?pre "@ * " (pp_block x) fs blocks
 
 let pp_us ?(pre = ("" : _ fmt)) fs us =
   if not (Set.is_empty us) then
     [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
 
-let rec pp vs all_xs fs {us; xs; cong; pure; heap; djns} =
+let rec pp_ ?var_strength vs parent_cong fs {us; xs; cong; pure; heap; djns}
+    =
   Format.pp_open_hvbox fs 0 ;
-  let all_xs = Set.union all_xs xs in
-  let is_x var = Set.mem all_xs (Option.value_exn (Var.of_term var)) in
+  let x v = Option.bind ~f:(fun m -> Map.find m v) var_strength in
   pp_us fs us ;
-  let xs_d_vs, xs_i_vs = Set.diff_inter xs vs in
+  let xs_d_vs, xs_i_vs =
+    Set.diff_inter
+      (Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous)))
+      vs
+  in
   if not (Set.is_empty xs_i_vs) then (
-    Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.pp_full ~is_x) xs_i_vs ;
+    Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ;
     if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
   if not (Set.is_empty xs_d_vs) then
-    Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.pp_full ~is_x) xs_d_vs ;
-  let first = Equality.is_true cong in
+    Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
+  let first = Equality.entails parent_cong cong in
   if not first then Format.fprintf fs "  " ;
-  Equality.pp_classes ~is_x fs cong ;
-  let pure_terms =
+  Equality.pp_classes_diff x fs (parent_cong, cong) ;
+  let pure =
     List.filter_map pure ~f:(fun e ->
         let e' = Equality.normalize cong e in
         if Term.is_true e' then None else Some e' )
   in
   List.pp
-    ~pre:(if first then "  " else "@ @<2>∧ ")
-    "@ @<2>∧ " (Term.pp_full ~is_x) fs pure_terms ;
-  let first = first && List.is_empty pure_terms in
+    ~pre:(if first then "@[  " else "@ @[@<2>∧ ")
+    "@ @<2>∧ " (Term.ppx x) fs
+    (List.dedup_and_sort ~compare:Term.compare pure)
+    ~suf:"@]" ;
+  let first = first && List.is_empty pure in
   if List.is_empty heap then
     Format.fprintf fs
       ( if first then if List.is_empty djns then "  emp" else ""
       else "@ @<5>∧ emp" )
-  else
-    pp_heap ~is_x ~pre:(if first then "  " else "@ @<2>∧ ") cong fs heap ;
+  else pp_heap x ~pre:(if first then "  " else "@ @<2>∧ ") cong fs heap ;
   let first = first && List.is_empty heap in
   List.pp
     ~pre:(if first then "  " else "@ * ")
     "@ * "
-    (pp_djn (Set.union vs (Set.union us xs)) all_xs)
+    (pp_djn ?var_strength (Set.union vs (Set.union us xs)) cong)
     fs djns ;
   Format.pp_close_box fs ()
 
-and pp_djn vs all_xs fs = function
+and pp_djn ?var_strength:parent_var_strength vs cong fs = function
   | [] -> Format.fprintf fs "false"
   | djn ->
       Format.fprintf fs "@[<hv>( %a@ )@]"
         (List.pp "@ @<2>∨ " (fun fs sjn ->
-             Format.fprintf fs "@[<hv 1>(%a)@]" (pp vs all_xs)
+             let var_strength =
+               let combine ~key sjn_v m_v =
+                 if Set.mem sjn.xs key then sjn_v else m_v
+               in
+               Option.map
+                 ~f:(Map.merge_skewed ~combine (var_strength sjn))
+                 parent_var_strength
+             in
+             Format.fprintf fs "@[<hv 1>(%a)@]"
+               (pp_ ?var_strength vs cong)
                {sjn with us= Set.diff sjn.us vs} ))
         djn
 
-let pp = pp Var.Set.empty Var.Set.empty
-let pp_djn = pp_djn Var.Set.empty Var.Set.empty
-
-let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
-  let f b s = f s b in
-  f loc (f bas (f len (f siz (f arr init))))
-
-let fold_vars_seg seg ~init ~f =
-  fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
+let pp fs q =
+  pp_ ~var_strength:(var_strength q) Var.Set.empty Equality.true_ fs q
 
+let pp_djn fs d = pp_djn Var.Set.empty Equality.true_ fs d
 let fv_seg seg = fold_vars_seg seg ~f:Set.add ~init:Var.Set.empty
 
-let fold_vars fold_vars {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
-  Equality.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
-  |> fun init ->
-  List.fold ~init pure ~f:(fun init -> Term.fold_vars ~f ~init)
-  |> fun init ->
-  List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
-  |> fun init ->
-  List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
-
 let rec fv_union init q =
   Set.diff (fold_vars fv_union q ~init ~f:Set.add) q.xs
 
diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml
index ccf33d65b..2cdb9078b 100644
--- a/sledge/src/symbheap/sh_domain.ml
+++ b/sledge/src/symbheap/sh_domain.ml
@@ -26,7 +26,13 @@ let init globals =
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )
 
-let join l r = Some (Sh.or_ l r)
+let join p q =
+  [%Trace.call fun {pf} -> pf "{ %a@ }@ { %a@ }" Sh.pp p Sh.pp q]
+  ;
+  Some (Sh.or_ p q)
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)]
+
 let is_false = Sh.is_false
 let dnf = Sh.dnf
 let exec_assume q b = Exec.assume q (Exp.term b)
@@ -36,8 +42,6 @@ let exec_move q res =
   Exec.move q (Vector.map res ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))
 
 let exec_inst pre inst =
-  [%Trace.info
-    "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ;
   match (inst : Llair.inst) with
   | Move {reg_exps; _} ->
       Some
diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml
index a70cecbe7..06c9aada8 100644
--- a/sledge/src/symbheap/sh_test.ml
+++ b/sledge/src/symbheap/sh_test.ml
@@ -51,9 +51,7 @@ let%test_module _ =
       [%expect
         {|
           ( (  0 = %x_1 ∧ emp)
-          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp)
-                       ∨ (∃ %x_1 .  2 = %x_1 ∧ emp)
-                       ))
+          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
 
         ( (∃ %x_1, %x_2 .   2 = %x_2 ∧ emp)
@@ -80,9 +78,7 @@ let%test_module _ =
         {|
         ∃ %x_1 .
           ( (  0 = %x_1 ∧ emp)
-          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp)
-                       ∨ (∃ %x_1 .  2 = %x_1 ∧ emp)
-                       ))
+          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
 
         ( (∃ %x_1, %x_3, %x_4 .   2 = %x_4 ∧ emp)
@@ -109,9 +105,7 @@ let%test_module _ =
         {|
         ∃ %x_1 .
           ( (  0 = %x_1 ∧ emp)
-          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp)
-                       ∨ (∃ %x_1 .  2 = %x_1 ∧ emp)
-                       ))
+          ∨ (∃ %x_1 .  ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
 
           ( (  emp) ∨ (  ( (  emp) ∨ (  emp) )) ) |}]
diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index e262b0063..88c6c42a0 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -29,14 +29,10 @@ type judgment =
   ; zs: Var.Set.t  (** existentials over remainder *)
   ; pgs: bool  (** indicates whether a deduction rule has been applied *) }
 
-let pp_xs fs xs =
-  if not (Set.is_empty xs) then
-    Format.fprintf fs "∃ @[%a@] .@;<1 2>" Var.Set.pp xs
-
 let pp fs {com; min; xs; sub; pgs} =
   Format.fprintf fs "@[%s %a@ | %a@ \\- %a%a@]"
     (if pgs then "t" else "f")
-    Sh.pp com Sh.pp min pp_xs xs Sh.pp sub
+    Sh.pp com Sh.pp min Var.Set.pp_xs xs Sh.pp sub
 
 let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
@@ -66,7 +62,6 @@ let special_cases xs = function
 let excise_term ({us; min; xs} as goal) pure term =
   let term' = Equality.normalize min.cong term in
   let term' = special_cases xs term' in
-  [%Trace.info "term': %a" Term.pp term'] ;
   if Term.is_true term' then Some ({goal with pgs= true}, pure)
   else
     match single_existential_occurrence xs term' with
@@ -614,7 +609,8 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
 let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
  fun minuend xs subtrahend ->
   [%Trace.call fun {pf} ->
-    pf "@[<hv>%a@ \\- %a%a@]" Sh.pp minuend pp_xs xs Sh.pp subtrahend]
+    pf "@[<hv>%a@ \\- %a%a@]" Sh.pp minuend Var.Set.pp_xs xs Sh.pp
+      subtrahend]
   ;
   assert (Set.disjoint minuend.us xs) ;
   assert (Set.is_subset xs ~of_:subtrahend.us) ;
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index 75f57f32a..01338f2f9 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -132,11 +132,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
-          \- ∃ %a_3 .
-              %l_6 -[)-> ⟨16,%a_3⟩
-        ) infer_frame:
-          ∃ %a1_7 .   %a_2 = %a1_7 ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ emp |}]
+            %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 .   %l_6 -[)-> ⟨16,%a_3⟩
+        ) infer_frame:   %a_2 = _ ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -152,11 +149,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
         ) infer_frame:
-          ∃ %a1_9 .
-            %a_2 = %a1_9
-          ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩
-          ∧ 16 = %m_8
-          ∧ emp |}]
+            %a_2 = _ ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ 16 = %m_8 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -172,11 +165,7 @@ let%test_module _ =
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
         ) infer_frame:
-          ∃ %a1_9 .
-            %a_2 = %a1_9
-          ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩
-          ∧ 16 = %m_8
-          ∧ emp |}]
+            %a_2 = _ ∧ ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a_2⟩ ∧ 16 = %m_8 ∧ emp |}]
 
     let%expect_test _ =
       check_frame
@@ -253,14 +242,12 @@ let%test_module _ =
                ∧ 2 = %n_9
                ∧ 16 = %m_8
                ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-            ∨ (∃ %a1_10 .
-                 %a_3 = %a1_10
+            ∨ (  %a_3 = _
                ∧ ⟨16,%a_1⟩ = ⟨8,%a_2⟩^⟨8,%a_3⟩
                ∧ 1 = %n_9
                ∧ 16 = %m_8
                ∧ emp)
-            ∨ (∃ %a1_10 .
-                 %a_3 = %a1_10
+            ∨ (  %a_3 = _
                ∧ ⟨16,%a_1⟩ = ⟨0,%a_2⟩^⟨16,%a_3⟩
                ∧ 0 = %n_9
                ∧ 16 = %m_8
diff --git a/sledge/src/trace/trace.ml b/sledge/src/trace/trace.ml
index 89cf9a426..dcad48441 100644
--- a/sledge/src/trace/trace.ml
+++ b/sledge/src/trace/trace.ml
@@ -85,17 +85,16 @@ let parse s =
 
 let pp_styled style fmt fs =
   Format.pp_open_box fs 2 ;
-  if (not !config.colors) || match style with `None -> true | _ -> false
-  then Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
+  if not !config.colors then
+    Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
   else (
     ( match style with
-    | `Bold -> Format.fprintf fs "\027[1m"
-    | `Cyan -> Format.fprintf fs "\027[36m"
-    | `Magenta -> Format.fprintf fs "\027[95m"
-    | _ -> () ) ;
+    | `Bold -> Format.fprintf fs "@<0>\027[1m"
+    | `Cyan -> Format.fprintf fs "@<0>\027[36m"
+    | `Magenta -> Format.fprintf fs "@<0>\027[95m" ) ;
     Format.kfprintf
       (fun fs ->
-        Format.fprintf fs "\027[0m" ;
+        Format.fprintf fs "@<0>\027[0m" ;
         Format.pp_close_box fs () )
       fs fmt )
 
diff --git a/sledge/src/trace/trace.mli b/sledge/src/trace/trace.mli
index 2b8f9e001..c58469d41 100644
--- a/sledge/src/trace/trace.mli
+++ b/sledge/src/trace/trace.mli
@@ -33,7 +33,7 @@ type 'a printf = ('a, Formatter.t, unit) format -> 'a
 type pf = {pf: 'a. 'a printf}
 
 val pp_styled :
-     [> `Bold | `Cyan | `Magenta | `None]
+     [`Bold | `Cyan | `Magenta]
   -> ('a, Format.formatter, unit, unit) format4
   -> Format.formatter
   -> 'a