From 9ac854c97082a5dbf578721f3c73122c7abf430b Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 14 Oct 2019 07:24:11 -0700
Subject: [PATCH] [sledge] Exec.kill should preserve vocabulary

Reviewed By: ngorogiannis

Differential Revision: D17801935

fbshipit-source-id: 81fe4b067
---
 sledge/src/symbheap/exec.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 686167b64..5a287652b 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -694,7 +694,9 @@ let assume pre cnd =
   let post = Sh.and_ cnd pre in
   if Sh.is_false post then None else Some post
 
-let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
+let kill pre reg =
+  let ms = Set.add Var.Set.empty reg in
+  Sh.extend_us ms (Sh.exists ms pre)
 
 let move pre reg_exps =
   exec_spec pre (move_spec pre.us reg_exps)