From 3f5adecdcf113fd5c56c3616f388ecdcb39558f1 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 14 Oct 2019 07:24:16 -0700
Subject: [PATCH] [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 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 5a287652b..1002f761d 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/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 ->