[sledge] Fix handling of existentials in Sh.and_

Summary:
`Sh.and_ b q` normalizes `b` using the equality context of `q` and
then conjoins the result to `q`. This is incorrect in case normalizing
`b` results in expressing it using existentials of `q`, which takes
the existentials out of their scope. So this diff changes from
essentially

    `(∃x.Q) ∧ B = (∃x.Q) ∧ (∃x.Bρ)`
to
    `(∃x.Q) ∧ B = (∃x'.Q[x'/x] ∧ Bρ)`

where `ρ` is the substitution that normalizes with respect to the
equality context.

Reviewed By: jvillard

Differential Revision: D26250536

fbshipit-source-id: 05f5c48c0

sledge/src/sh.ml

@@ -555,7 +555,13 @@ let pure (p : Formula.t) =
     invariant q]
 
 let and_ b q =
-  star (pure (Formula.map_terms ~f:(Context.normalize q.ctx) b)) q
+  [%trace]
+    ~call:(fun {pf} -> pf "@ (%a)@ (%a)" Formula.pp b pp q)
+    ~retn:(fun {pf} -> pf "%a" pp)
+  @@ fun () ->
+  let xs, q = bind_exists q ~wrt:(Formula.fv b) in
+  let b = Formula.map_terms ~f:(Context.normalize q.ctx) b in
+  exists xs (star (pure b) q)
 
 let and_subst subst q =
   [%Trace.call fun {pf} -> pf "@ %a@ %a" Context.Subst.pp subst pp q]