diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 2224ed4ed..ebdfe00b4 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -721,6 +721,9 @@ let fold_uses_of r t s ~f =
   Subst.fold r.rep s ~f:(fun ~key:trm ~data:rep s ->
       fold_ ~f trm (fold_ ~f rep s) )
 
+let iter_uses_of t r ~f = fold_uses_of r t () ~f:(fun use () -> f use)
+let uses_of t r = Iter.from_labelled_iter (iter_uses_of t r)
+
 let apply_subst wrt s r =
   [%Trace.call fun {pf} -> pf "%a@ %a" Subst.pp s pp r]
   ;
@@ -1179,60 +1182,27 @@ let solve_for_vars vss r =
               else `Continue us_xs )
             ~finish:(fun _ -> false) ) )]
 
-(* [elim] removes variables from a context by rearranging the existing
-   equality classes. Non-representative terms that contain a variable to
-   eliminate can be simply dropped. If a representative needs to be removed,
-   a new representative is chosen. This basic approach is insufficient if
-   interpreted terms are to be removed. For example, eliminating x from x +
-   1 = y = z ∧ w = x by just preserving the existing classes between terms
-   that do not mention x would yield y = z. This would lose provability of
-   the equality w = y - 1. So variables with interpreted uses are not
-   eliminated. *)
-let elim xs r =
+let trivial vs r =
   [%trace]
-    ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs xs pp_raw r)
-    ~retn:(fun {pf} (ks, r') ->
-      pf "%a@ %a" Var.Set.pp_xs ks pp_raw r' ;
-      assert (Var.Set.subset ks ~of_:xs) ;
+    ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs vs pp_raw r)
+    ~retn:(fun {pf} ks -> pf "%a" Var.Set.pp_xs ks)
+  @@ fun () ->
+  Var.Set.fold vs Var.Set.empty ~f:(fun v ks ->
+      let x = Trm.var v in
+      match Subst.find x r.rep with
+      | None -> Var.Set.add v ks
+      | Some x' when Trm.equal x x' && Iter.is_empty (uses_of x r) ->
+          Var.Set.add v ks
+      | _ -> ks )
+
+let trim ks r =
+  [%trace]
+    ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs ks pp_raw r)
+    ~retn:(fun {pf} r' ->
+      pf "%a" pp_raw r' ;
       assert (Var.Set.disjoint ks (fv r')) )
   @@ fun () ->
-  (* add the uninterpreted uses of terms in delta to approx, and the
-     interpreted uses to interp *)
-  let rec add_uninterp_uses approx interp delta =
-    if not (Trm.Set.is_empty delta) then
-      let approx = Trm.Set.union approx delta in
-      let delta, interp =
-        Trm.Set.fold delta
-          (Trm.Set.empty, Trm.Set.empty)
-          ~f:
-            (fold_uses_of r ~f:(fun use (delta, interp) ->
-                 if is_interpreted use then (delta, Trm.Set.add use interp)
-                 else (Trm.Set.add use delta, interp) ))
-      in
-      add_uninterp_uses approx interp delta
-    else
-      (* remove the subterms of interpreted uses from approx *)
-      let rec remove_subtrms misses approx =
-        if not (Trm.Set.is_empty misses) then
-          let approx = Trm.Set.diff approx misses in
-          let misses =
-            Trm.Set.of_iter
-              (Iter.flat_map ~f:Trm.trms (Trm.Set.to_iter misses))
-          in
-          remove_subtrms misses approx
-        else approx
-      in
-      remove_subtrms interp approx
-  in
-  (* compute terms in relation mentioning vars to eliminate *)
-  let kills =
-    add_uninterp_uses Trm.Set.empty Trm.Set.empty
-      (Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter xs)))
-  in
-  let ks =
-    Trm.Set.fold kills Var.Set.empty ~f:(fun kill ks ->
-        match Var.of_trm kill with Some k -> Var.Set.add k ks | None -> ks )
-  in
+  let kills = Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter ks)) in
   (* compute classes including reps *)
   let reps =
     Subst.fold r.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps ->
@@ -1268,7 +1238,7 @@ let elim xs r =
                   Subst.add ~key:elt ~data:rep' s )
           | None -> s )
   in
-  (ks, {r with rep})
+  {r with rep}
 
 let apply_and_elim ~wrt xs s r =
   [%trace]
@@ -1283,7 +1253,8 @@ let apply_and_elim ~wrt xs s r =
     let zs, r = apply_subst wrt s r in
     if is_unsat r then (Var.Set.empty, unsat, Var.Set.empty)
     else
-      let ks, r = elim xs r in
+      let ks = trivial xs r in
+      let r = trim ks r in
       (zs, r, ks)
 
 (*
diff --git a/sledge/src/fol/context.mli b/sledge/src/fol/context.mli
index e50b83256..60ea10e72 100644
--- a/sledge/src/fol/context.mli
+++ b/sledge/src/fol/context.mli
@@ -85,6 +85,8 @@ module Subst : sig
   type t
 
   val pp : t pp
+  val empty : t
+  val compose : t -> t -> t
   val is_empty : t -> bool
   val fold_eqs : t -> 's -> f:(Formula.t -> 's -> 's) -> 's
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 678443e26..d0bf054c9 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -767,42 +767,56 @@ let remove_absent_xs ks q =
     in
     {q with xs; djns}
 
-let rec simplify_ us rev_xss q =
-  [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q]
+let rec simplify_ us rev_xss ancestor_subst q =
+  [%Trace.call fun {pf} ->
+    pf "%a@ %a@ %a" pp_vss (List.rev rev_xss) Context.Subst.pp
+      ancestor_subst pp_raw q]
   ;
+  assert (not (is_false q)) ;
+  let q0 = q in
   (* bind existentials *)
   let xs, q = bind_exists ~wrt:emp.us q in
   let rev_xss = xs :: rev_xss in
-  (* recursively simplify subformulas *)
-  let q =
-    starN
-      ( {q with djns= []}
-      :: List.map q.djns ~f:(fun djn ->
-             orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) )
-      )
-  in
   (* try to solve equations in ctx for variables in xss *)
-  let xss = List.rev rev_xss in
-  let subst = Context.solve_for_vars (us :: xss) q.ctx in
-  let union_xss = Var.Set.union_list rev_xss in
-  let wrt = Var.Set.union us union_xss in
-  let fresh, ctx, removed =
-    Context.apply_and_elim ~wrt union_xss subst q.ctx
-  in
-  ( if Context.is_unsat ctx then false_ q.us
-  else if Context.Subst.is_empty subst then exists xs q
+  let stem_subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
+  let subst = Context.Subst.compose ancestor_subst stem_subst in
+  ( if Context.Subst.is_empty subst then q0
   else
-    (* normalize wrt solutions *)
-    let q = extend_us fresh q in
-    (* opt: ctx already normalized wrt subst, so just preserve it *)
-    let q = {(norm subst {q with ctx= Context.empty}) with ctx} in
+    (* normalize context wrt solutions *)
+    let union_xss = Var.Set.union_list rev_xss in
+    let wrt = Var.Set.union us union_xss in
+    let fresh, ctx, removed =
+      Context.apply_and_elim ~wrt union_xss subst q.ctx
+    in
+    let q = {(extend_us fresh q) with ctx} in
+    (* normalize stem wrt both ancestor and current solutions *)
+    let stem =
+      (* opt: ctx already normalized so just preserve it *)
+      {(norm subst {q with djns= emp.djns; ctx= emp.ctx}) with ctx= q.ctx}
+    in
+    (* recursively simplify subformulas *)
+    let q =
+      starN
+        ( stem
+        :: List.map q.djns ~f:(fun djn ->
+               orN (List.map ~f:(simplify_ us rev_xss subst) djn) ) )
+    in
     if is_false q then false_ q.us
     else
-      (* opt: removed already disjoint from ctx, so ignore it *)
       let removed =
-        Var.Set.diff removed (fv ~ignore_ctx:() (elim_exists q.xs q))
+        if Var.Set.is_empty removed then Var.Set.empty
+        else (
+          (* opt: removed already disjoint from ctx, so ignore_ctx *)
+          assert (Var.Set.disjoint removed (Context.fv q.ctx)) ;
+          Var.Set.diff removed (fv ~ignore_ctx:() (elim_exists q.xs q)) )
+      in
+      (* removed may not contain all variables stem_subst has solutions for,
+         so the equations in [∃ removed. stem_subst] that are not
+         universally valid need to be re-conjoined since they have alredy
+         been normalized out *)
+      let keep, removed, _ =
+        Context.Subst.partition_valid removed stem_subst
       in
-      let keep, removed, _ = Context.Subst.partition_valid removed subst in
       let q = and_subst keep q in
       (* (re)quantify existentials *)
       let q = exists (Var.Set.union fresh xs) q in
@@ -810,7 +824,7 @@ let rec simplify_ us rev_xss q =
       remove_absent_xs removed q )
   |>
   [%Trace.retn fun {pf} q' ->
-    pf "%a@ %a" Context.Subst.pp subst pp_raw q' ;
+    pf "%a@ %a" Context.Subst.pp stem_subst pp_raw q' ;
     invariant q']
 
 let simplify q =
@@ -822,7 +836,7 @@ let simplify q =
     let q = propagate_context Var.Set.empty Context.empty q in
     if is_false q then false_ q.us
     else
-      let q = simplify_ q.us [] q in
+      let q = simplify_ q.us [] Context.Subst.empty q in
       q )
   |>
   [%Trace.retn fun {pf} q' ->