From d33cecfa33a2ba4f596072e479282605b3de9596 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 2 Dec 2020 13:49:11 -0800
Subject: [PATCH] [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 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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