[sledge] Fix in Sh.simplify

Summary:
A context with valid but extraneous equations was being kept. The
extra equations are valid, but might violate vocabulary invariants.

Reviewed By: jvillard

Differential Revision: D25196734

fbshipit-source-id: a8001a075

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