diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 0401d215d..71f9f99e1 100644
--- a/sledge/src/exec.ml
+++ b/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)