[sledge] Exec.exec_specs missed vocabulary extension

Summary:
In a spec, it currently may be that foot.us does not contain xs. So
exec_specs needs to extend the vocabulary of foot before existentially
quantifying out xs.

Reviewed By: ngorogiannis

Differential Revision: D17801933

fbshipit-source-id: 7b4b9262a

sledge/src/symbheap/exec.ml

@@ -680,6 +680,7 @@ let exec_spec pre {xs; foot; sub; ms; post} =
    preconditions are known to be tautologous *)
 let rec exec_specs pre = function
   | ({xs; foot; _} as spec) :: specs ->
+      let foot = Sh.extend_us xs foot in
       let pre_pure = Sh.star (Sh.exists xs (Sh.pure_approx foot)) pre in
       exec_spec pre_pure spec
       >>= fun post ->