diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 54fc55766..4b7c9e1d5 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -274,7 +274,7 @@ module Make (Dom : Domain_sig.Dom) = struct
     let Llair.{callee; actuals; areturn; return; recursive} = call in
     let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a with state %a" Reg.pp name.reg Reg.pp
+      pf "%a from %a with state@ %a" Reg.pp name.reg Reg.pp
         return.dst.parent.name.reg Dom.pp state]
     ;
     let dnf_states =
diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index c69bae17e..12ea82932 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -428,7 +428,7 @@ module Var = struct
     let pp fs s =
       Format.fprintf fs "@[<1>[%a]@]"
         (List.pp ",@ " (fun fs (k, v) ->
-             Format.fprintf fs "@[[%a ↦ %a]@]" pp_t k pp_t v ))
+             Format.fprintf fs "@[%a ↦ %a@]" pp_t k pp_t v ))
         (Map.to_alist s)
 
     let empty = empty_map
diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 1002f761d..b6024d745 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -646,10 +646,16 @@ let strlen_spec us reg ptr =
  * Symbolic Execution
  *)
 
+let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
+  let gain_us = Set.diff q1.us q0.us in
+  let lose_us = Set.diff q0.us q1.us in
+  (Set.is_empty gain_us || fail "gain us: %a" Var.Set.pp gain_us ())
+  && (Set.is_empty lose_us || fail "lose us: %a" Var.Set.pp lose_us ())
+
 (* execute a command with given spec from pre *)
-let exec_spec pre {xs; foot; sub; ms; post} =
+let exec_spec pre0 {xs; foot; sub; ms; post} =
   [%Trace.call fun {pf} ->
-    pf "@[%a@]@ @[<2>%a@,@[<hv>{%a  %a}@;<1 -1>%a--@ {%a  }@]@]" Sh.pp pre
+    pf "@[%a@]@ @[<2>%a@,@[<hv>{%a  %a}@;<1 -1>%a--@ {%a  }@]@]" Sh.pp pre0
       (Sh.pp_us ~pre:"@<2>∀ ")
       xs Sh.pp foot
       (fun fs sub ->
@@ -661,20 +667,22 @@ let exec_spec pre {xs; foot; sub; ms; post} =
           Format.fprintf fs "%a := " Var.Set.pp ms )
       ms Sh.pp post ;
     assert (
-      let vs = Set.diff (Set.diff foot.us xs) pre.us in
+      let vs = Set.diff (Set.diff foot.us xs) pre0.us in
       Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ;
     assert (
-      let vs = Set.diff (Set.diff post.us xs) pre.us in
+      let vs = Set.diff (Set.diff post.us xs) pre0.us in
       Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )]
   ;
   let foot = Sh.extend_us xs foot in
-  let zs, pre = Sh.bind_exists pre ~wrt:xs in
+  let zs, pre = Sh.bind_exists pre0 ~wrt:xs in
   ( Solver.infer_frame pre xs foot
   >>| fun frame ->
   Sh.exists (Set.union zs xs)
     (Sh.star post (Sh.exists ms (Sh.rename sub frame))) )
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" (Option.pp "%a" Sh.pp) r]
+  [%Trace.retn fun {pf} r ->
+    pf "%a" (Option.pp "%a" Sh.pp) r ;
+    assert (Option.for_all ~f:(check_preserve_us pre0) r)]
 
 (* execute a multiple-spec command, where the disjunction of the specs
    preconditions are known to be tautologous *)
@@ -687,6 +695,14 @@ let rec exec_specs pre = function
       exec_specs pre specs >>| fun posts -> Sh.or_ post posts
   | [] -> Some (Sh.false_ pre.us)
 
+let exec_specs pre specs =
+  [%Trace.call fun _ -> ()]
+  ;
+  exec_specs pre specs
+  |>
+  [%Trace.retn fun _ r ->
+    assert (Option.for_all ~f:(check_preserve_us pre) r)]
+
 (*
  * Exposed interface
  *)
@@ -723,18 +739,13 @@ let abort _ = None
 let intrinsic ~skip_throw :
     Sh.t -> Var.t option -> Var.t -> Term.t list -> Sh.t option option =
  fun pre areturn intrinsic actuals ->
-  [%Trace.info
-    "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
-      (Option.pp "%a := " Var.pp)
-      areturn Var.pp intrinsic (List.pp ",@ " Term.pp) (List.rev actuals)
-      Sh.pp pre] ;
   let us = pre.us in
   let name =
     let n = Var.name intrinsic in
     match String.index n '.' with None -> n | Some i -> String.prefix n i
   in
   let skip pre = Some (Some pre) in
-  match (areturn, name, actuals) with
+  ( match (areturn, name, actuals) with
   (*
    * cstdlib - memory management
    *)
@@ -808,4 +819,12 @@ let intrinsic ~skip_throw :
    *)
   (* bool folly::usingJEMalloc() *)
   | Some _, "_ZN5folly13usingJEMallocEv", [] -> skip pre
-  | _ -> None
+  | _ -> None )
+  $> function
+  | None -> ()
+  | Some _ ->
+      [%Trace.info
+        "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
+          (Option.pp "%a := " Var.pp)
+          areturn Var.pp intrinsic (List.pp ",@ " Term.pp)
+          (List.rev actuals) Sh.pp pre]
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 67c82a92c..dc841184f 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -240,11 +240,11 @@ and freshen_xs q ~wrt =
     if xs == q.xs && q' == q then q else {q' with xs} )
   |>
   [%Trace.retn fun {pf} q' ->
-    pf "%a" pp q' ;
-    invariant q' ;
+    pf "%a@ %a" Var.Subst.pp sub pp q' ;
     assert (Set.equal q'.us q.us) ;
     assert (Set.disjoint q'.xs (Var.Subst.domain sub)) ;
-    assert (Set.disjoint q'.xs (Set.inter q.xs wrt))]
+    assert (Set.disjoint q'.xs (Set.inter q.xs wrt)) ;
+    invariant q']
 
 let extend_us us q =
   let us = Set.union us q.us in
@@ -273,8 +273,7 @@ let exists xs q =
   ;
   assert (
     Set.is_subset xs ~of_:q.us
-    || fail "Sh.exists fail xs - q.us:%a" Var.Set.pp (Set.diff xs q.us) ()
-  ) ;
+    || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Set.diff xs q.us) () ) ;
   {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
@@ -440,6 +439,13 @@ let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   if heap == q.heap && djns == q.djns then q
   else {us; xs; cong; pure; heap; djns} |> check invariant
 
+let pure_approx q =
+  [%Trace.call fun {pf} -> pf "%a" pp q]
+  ;
+  pure_approx q
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
+
 let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
   let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
     let ys, sjn = bind_exists sjn ~wrt:xs in