diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 4e33ff666..899b4b8bc 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -720,6 +720,10 @@ let exec_specs pre specs =
  *)
 
 let assume pre cnd =
+  [%trace]
+    ~call:(fun {pf} -> pf "%a" Formula.pp cnd)
+    ~retn:(fun {pf} -> pf "%a" pp)
+  @@ fun () ->
   let post = Sh.and_ cnd pre in
   if Sh.is_unsat post then None else Some post
 
diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index b987dc077..90400904d 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -49,6 +49,8 @@ struct
         Format.fprintf ppf "@[<2>%a@]" pp_num num
       else Format.fprintf ppf "@[<2>(%a%a)@]" pp_num num pp_den den
 
+    let pp = ppx (fun _ -> None)
+
     (** [one] is the empty product Πᵢ₌₁⁰ xᵢ^pᵢ *)
     let one = Prod.empty
 
@@ -317,6 +319,16 @@ struct
     (** [solve_for_mono r c m p] solves [0 = r + (c×m) + p] as [m = q]
         ([Some (m, q)]) such that [r + (c×m) + p = m - q] *)
     let solve_for_mono rejected_poly coeff mono poly =
+      [%trace]
+        ~call:(fun {pf} ->
+          pf "0 = %a + (%a×%a) + %a" pp rejected_poly Q.pp coeff Mono.pp
+            mono pp poly )
+        ~retn:(fun {pf} s ->
+          pf "%a"
+            (Option.pp "%a" (fun fs (v, q) ->
+                 Format.fprintf fs "%a ↦ %a" pp v pp q ))
+            s )
+      @@ fun () ->
       if Mono.equal_one mono || exists_fv_in (Mono.fv mono) poly then None
       else
         Some
diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 25c1c70a5..7f8318a27 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -177,6 +177,11 @@ end = struct
       and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
       ks ∩ fv(τ) = ∅. *)
   let partition_valid xs s =
+    [%trace]
+      ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs xs pp s)
+      ~retn:(fun {pf} (t, ks, u) ->
+        pf "%a@ %a@ %a" pp t Var.Set.pp_xs ks pp u )
+    @@ fun () ->
     (* Move equations e=f from s to t when ∃ks.e=f fails to be provably
        valid. When moving an equation, reduce ks by fv(e=f) to maintain ks ∩
        fv(t) = ∅. This reduction may cause equations in s to no longer be
@@ -258,6 +263,15 @@ let solve_poly ?f p q s =
 (* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n
    = |α| and c fresh *)
 let rec solve_extract ?f a o l b s =
+  [%trace]
+    ~call:(fun {pf} ->
+      pf "%a = %a@ %a%a" Trm.pp
+        (Trm.extract ~seq:a ~off:o ~len:l)
+        Trm.pp b Var.Set.pp_xs (snd3 s) Subst.pp (trd3 s) )
+    ~retn:(fun {pf} -> function
+      | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s
+      | None -> pf "false" )
+  @@ fun () ->
   let n = Trm.seq_size_exn a in
   let c, s = fresh "c" s in
   let n_c = Trm.sized ~siz:n ~seq:c in
@@ -275,6 +289,14 @@ let rec solve_extract ?f a o l b s =
 (* α₀^…^αᵢ^αⱼ^…^αᵥ = β ==> |α₀^…^αᵥ| = |β| ∧ … ∧ αⱼ = β[n₀+…+nᵢ,nⱼ) ∧ …
    where nₓ ≡ |αₓ| and m = |β| *)
 and solve_concat ?f a0V b m s =
+  [%trace]
+    ~call:(fun {pf} ->
+      pf "%a = %a@ %a%a" Trm.pp (Trm.concat a0V) Trm.pp b Var.Set.pp_xs
+        (snd3 s) Subst.pp (trd3 s) )
+    ~retn:(fun {pf} -> function
+      | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s
+      | None -> pf "false" )
+  @@ fun () ->
   Iter.fold_until (Array.to_iter a0V) (s, Trm.zero)
     ~f:(fun aJ (s, oI) ->
       let nJ = Trm.seq_size_exn aJ in
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 01bd54f21..40f31d124 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -630,18 +630,23 @@ module Func = struct
   let invariant func =
     assert (func == func.entry.parent) ;
     let@ () = Invariant.invariant [%here] func [%sexp_of: t] in
-    match Function.typ func.name with
-    | Pointer {elt= Function {return; _}; _} ->
-        assert (
-          not
-            (Iter.contains_dup
-               (Iter.of_list (entry_cfg func))
-               ~cmp:(fun b1 b2 -> String.compare b1.lbl b2.lbl)) ) ;
-        assert (
-          Bool.equal (Option.is_some return) (Option.is_some func.freturn)
-        ) ;
-        iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
-    | _ -> assert false
+    try
+      match Function.typ func.name with
+      | Pointer {elt= Function {return; _}; _} ->
+          assert (
+            not
+              (Iter.contains_dup
+                 (Iter.of_list (entry_cfg func))
+                 ~cmp:(fun b1 b2 -> String.compare b1.lbl b2.lbl)) ) ;
+          assert (
+            Bool.equal (Option.is_some return) (Option.is_some func.freturn)
+          ) ;
+          iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
+      | _ -> assert false
+    with exc ->
+      let bt = Printexc.get_raw_backtrace () in
+      [%Trace.info "%a" pp func] ;
+      Printexc.raise_with_backtrace exc bt
 
   let find name functions =
     Function.Map.find (Function.counterfeit name) functions
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 15c8019ee..97ab11891 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -290,7 +290,7 @@ let rec invariant q =
             invariant sjn ) )
   with exc ->
     let bt = Printexc.get_raw_backtrace () in
-    [%Trace.info "%a" pp q] ;
+    [%Trace.info "%a" pp_raw q] ;
     Printexc.raise_with_backtrace exc bt
 
 (** Quantification and Vocabulary *)
@@ -446,9 +446,14 @@ let and_ctx ctx q =
     invariant q]
 
 let star q1 q2 =
-  [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2]
-  ;
-  ( match (q1, q2) with
+  [%trace]
+    ~call:(fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2)
+    ~retn:(fun {pf} q ->
+      pf "%a" pp q ;
+      invariant q ;
+      assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us)) )
+  @@ fun () ->
+  match (q1, q2) with
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Var.Set.union q1.us q2.us)
   | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _
@@ -479,12 +484,7 @@ let star q1 q2 =
           ; ctx
           ; pure
           ; heap= List.append h1 h2
-          ; djns= List.append d1 d2 } )
-  |>
-  [%Trace.retn fun {pf} q ->
-    pf "%a" pp q ;
-    invariant q ;
-    assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us))]
+          ; djns= List.append d1 d2 }
 
 let starN = function
   | [] -> emp
@@ -725,6 +725,10 @@ let pp_vss fs vss =
     vss
 
 let remove_absent_xs ks q =
+  [%trace]
+    ~call:(fun {pf} -> pf "%a%a" Var.Set.pp_xs ks pp q)
+    ~retn:(fun {pf} -> pf "%a" pp)
+  @@ fun () ->
   let ks = Var.Set.inter ks q.xs in
   if Var.Set.is_empty ks then q
   else