From 94fedd9cf0b1e791f268279ed2c4eb2184ae3c9e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 11 Mar 2019 09:11:41 -0700
Subject: [PATCH] [sledge] Minor simplification of Exec implementation

Reviewed By: ngorogiannis

Differential Revision: D14403653

fbshipit-source-id: cc612edc5
---
 sledge/src/symbheap/exec.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml
index 10e3ce167..af9af3893 100644
--- a/sledge/src/symbheap/exec.ml
+++ b/sledge/src/symbheap/exec.ml
@@ -27,6 +27,7 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
   {us; xs; seg= {loc; bas; len; siz; arr}}
 
 let null_eq ptr = Sh.pure (Exp.eq Exp.null ptr)
+let zero = Exp.integer Z.zero Typ.siz
 
 let assume cnd pre =
   let post = Sh.and_ cnd pre in
@@ -70,8 +71,7 @@ let memcpy_eq_spec us dst src len =
   let {xs; seg} = fresh_seg ~loc:dst ~len us in
   let dst_heap = Sh.seg seg in
   let foot =
-    Sh.and_ (Exp.eq dst src)
-      (Sh.and_ (Exp.eq len (Exp.integer Z.zero Typ.siz)) dst_heap)
+    Sh.and_ (Exp.eq dst src) (Sh.and_ (Exp.eq len zero) dst_heap)
   in
   let post = dst_heap in
   {xs; foot; post}