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 ->