[sledge] Fix vocabulary handling of symbolic execution of multi-spec insts

Summary:
Instructions that have multiple specs sometimes have inconsistent
footprints for one or more of their specifications. In such cases, the
handling of the existential and universal vocabularies was sometimes
incorrect before this diff. In particular, the ghosts of a spec need
not appear in the pure approximation of the footprint, which the
previous code incorrectly assumed. Also, the unit of disjunction is
`false` with an empty vocabulary, not the precondition's vocabulary as
the previous code incorrectly used.

Reviewed By: ngorogiannis

Differential Revision: D24989067

fbshipit-source-id: eca3bff55

sledge/src/exec.ml

@@ -692,13 +692,14 @@ let exec_specs pre =
   let rec exec_specs_ (xs, pre) = function
     | specm :: specs ->
         let gs, spec = gen_spec pre.Sh.us specm in
+        let pure = Sh.pure (Sh.pure_approx spec.foot) in
         let pre_pure =
-          Sh.(star (exists gs (Sh.pure (pure_approx spec.foot))) pre)
+          Sh.star (Sh.exists (Var.Set.inter gs pure.us) pure) pre
         in
         let* post = exec_spec_ (xs, pre_pure) (gs, spec) in
         let+ posts = exec_specs_ (xs, pre) specs in
         Sh.or_ post posts
-    | [] -> Some (Sh.false_ pre.us)
+    | [] -> Some (Sh.false_ Var.Set.empty)
   in
   exec_specs_ (xs, pre)