diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 1e7bd30d1..7b1931bbb 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -159,6 +159,22 @@ let rec invariant q =
             invariant sjn ) )
   with exc -> [%Trace.info "%a" pp q] ; raise exc
 
+let rec simplify {us; xs; cong; pure; heap; djns} =
+  [%Trace.call fun {pf} -> pf "%a" pp {us; xs; cong; pure; heap; djns}]
+  ;
+  let heap = List.map heap ~f:(map_seg ~f:(Equality.normalize cong)) in
+  let pure = List.map pure ~f:(Equality.normalize cong) in
+  let cong = Equality.true_ in
+  let djns = List.map djns ~f:(List.map ~f:simplify) in
+  let all_vars =
+    fv {us= Set.union us xs; xs= Var.Set.empty; cong; pure; heap; djns}
+  in
+  let xs = Set.inter all_vars xs in
+  let us = Set.inter all_vars us in
+  {us; xs; cong; pure; heap; djns} |> check invariant
+  |>
+  [%Trace.retn fun {pf} s -> pf "%a" pp s]
+
 (** Quantification and Vocabulary *)
 
 let rename_seg sub ({loc; bas; len; siz; arr} as h) =
diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli
index 927e61482..da8b6ef9c 100644
--- a/sledge/src/symbheap/sh.mli
+++ b/sledge/src/symbheap/sh.mli
@@ -30,6 +30,7 @@ val pp_seg_norm : Equality.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp
 val pp : t pp
 val pp_djn : disjunction pp
+val simplify : t -> t
 
 include Invariant.S with type t := t
 
diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml
index 89c94b13a..cd5ce0c18 100644
--- a/sledge/src/symbheap/sh_test.ml
+++ b/sledge/src/symbheap/sh_test.ml
@@ -89,4 +89,30 @@ let%test_module _ =
         ∨ (∃ %x_1, %x_3 .   1 = %y_2 = %x_3 ∧ emp)
         ∨ (∃ %x_1 .   0 = %x_1 ∧ emp)
         ) |}]
+
+    let%expect_test _ =
+      let q =
+        Sh.(
+          exists
+            ~$[x_]
+            (or_
+               (pure (x = !0))
+               (exists
+                  ~$[x_]
+                  (or_
+                     (and_ (x = !1) (pure (y = !1)))
+                     (exists ~$[x_] (pure (x = !2)))))))
+      in
+      pp q ;
+      pp (Sh.simplify q) ;
+      [%expect
+        {|
+        ∃ %x_1 .
+        emp
+        * ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .emp
+             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          )
+
+        emp * ( (emp) ∨ (emp * ( (emp) ∨ (emp) )) ) |}]
   end )
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index 5fddd5304..a58ff7c91 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -9,7 +9,13 @@
 
 type t = Sh.t [@@deriving equal, sexp_of]
 
-let pp = Sh.pp
+let pp_full fs s = [%Trace.fprintf fs "%a" Sh.pp s]
+let pp fs s = [%Trace.fprintf fs "%a" Sh.pp (Sh.simplify s)]
+let pp fs s = pp_full fs s ; pp fs s
+
+(* I think it would be nice if `-t State_domain.pp` enabled the simplified
+   printing, with `-t State_domain.pp_full` for the more verbose one. So how
+   about this renaming? *)
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function