From c10ccafd43989fd1364da8e58d5daa2e7665707b Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:26:56 -0800
Subject: [PATCH] [sledge] Add fast path to Context.partition_valid for empty
 existentials

Reviewed By: jvillard

Differential Revision: D25756556

fbshipit-source-id: 3bc85095d
---
 sledge/src/fol/context.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 2ad3a0798..f10b047bc 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -199,7 +199,8 @@ end = struct
       in
       if s' != s then partition_valid_ t' ks' s' else (t', ks', s')
     in
-    partition_valid_ empty xs s
+    if Var.Set.is_empty xs then (s, Var.Set.empty, empty)
+    else partition_valid_ empty xs s
 
   (* direct representation manipulation *)