From 0bef279ed1f87ed55d845b312d9d63028a56cad1 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 18 Mar 2019 12:46:10 -0700
Subject: [PATCH] [sledge] Fix bug in quantifier handling during Sh.or
 simplification
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
P ∨ (∃x. Q ∨ R) could be simplified to (∃x. P ∨ Q ∨ R) and capture
occurrences of x in P.

Reviewed By: ngorogiannis

Differential Revision: D14481990

fbshipit-source-id: 92b474d59
---
 sledge/src/symbheap/sh.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index abd2b6abe..0d72dec10 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -314,8 +314,13 @@ let or_ q1 q2 =
   | _, {djns= [[]]; _} ->
       let us = Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
-  | ({djns= []; _} as q), ({pure= []; heap= []; djns= [djn]; _} as d)
-   |({pure= []; heap= []; djns= [djn]; _} as d), ({djns= []; _} as q) ->
+  | ( ({djns= []; _} as q)
+    , ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) )
+    when Set.is_empty xs ->
+      {d with us= Set.union q.us d.us; djns= [q :: djn]}
+  | ( ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d)
+    , ({djns= []; _} as q) )
+    when Set.is_empty xs ->
       {d with us= Set.union q.us d.us; djns= [q :: djn]}
   | _ ->
       { us= Set.union q1.us q2.us