From 556739e17c8d8c3e3c72e52290334ed64007102c Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 10 Mar 2020 02:21:09 -0700
Subject: [PATCH] [sledge] Minor optimization of Sh.bind_exists

Reviewed By: jvillard

Differential Revision: D20303061

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

diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index 5f339b70b..f6784b7b5 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -374,7 +374,9 @@ let freshen ~wrt q =
 let bind_exists q ~wrt =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
   ;
-  let q' = freshen_xs q ~wrt:(Set.union q.us wrt) in
+  let q' =
+    if Set.is_empty wrt then q else freshen_xs q ~wrt:(Set.union q.us wrt)
+  in
   (q'.xs, {q' with us= Set.union q'.us q'.xs; xs= Var.Set.empty})
   |>
   [%Trace.retn fun {pf} (_, q') -> pf "%a" pp q']