From e9fd3b603da758b2977bec2ee7e9fab52ca7d6c9 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:25:42 -0800
Subject: [PATCH] [sledge] Add fast path to Sh.simplify for unsat formulas

Reviewed By: jvillard

Differential Revision: D25756571

fbshipit-source-id: e03906ca9
---
 sledge/src/sh.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index df8d4459b..be1b3a0f7 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -812,10 +812,14 @@ let rec simplify_ us rev_xss q =
 let simplify q =
   [%Trace.call fun {pf} -> pf "%a" pp_raw q]
   ;
-  let q = freshen_nested_xs q in
-  let q = propagate_context Var.Set.empty Context.empty q in
-  let q = simplify_ q.us [] q in
-  q
+  ( if is_false q then false_ q.us
+  else
+    let q = freshen_nested_xs q in
+    let q = propagate_context Var.Set.empty Context.empty q in
+    if is_false q then false_ q.us
+    else
+      let q = simplify_ q.us [] q in
+      q )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp_raw q' ;