diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index a1624dbb7..78556f5ab 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -759,7 +759,7 @@ let rec simplify_ us rev_xss q =
       (* normalize wrt solutions *)
       let q = norm subst q in
       (* reconjoin only non-redundant equations *)
-      let _, ctx' =
+      let _, ctx =
         Context.apply_subst
           (Var.Set.union us (Var.Set.union_list rev_xss))
           subst q.ctx
@@ -767,11 +767,11 @@ let rec simplify_ us rev_xss q =
       let removed =
         Var.Set.diff
           (Var.Set.union_list rev_xss)
-          (Var.Set.union (Context.fv ctx')
+          (Var.Set.union (Context.fv ctx)
              (fv ~ignore_ctx:() (elim_exists q.xs q)))
       in
       let keep, removed, _ = Context.Subst.partition_valid removed subst in
-      (removed, and_subst keep q)
+      (removed, and_subst keep {q with ctx})
   in
   (* re-quantify existentials *)
   let q = exists xs q in