From 80afaaee1b1ea9b9f7b5d16a9df3690dec6ca47c Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 2 Mar 2020 08:43:37 -0800
Subject: [PATCH] [sledge] Detect unsat subtrahend when subtracting pure terms

Summary: Enables failing doomed proof searches earlier.

Reviewed By: ngorogiannis

Differential Revision: D20120272

fbshipit-source-id: e06a7ed5a
---
 sledge/src/symbheap/solver.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index 0d4d9b398..76419f9b5 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -94,7 +94,8 @@ let drop_tautology xs sub e =
 let excise_term ({min; xs; sub} as goal) pure term =
   let term' = Equality.normalize min.cong term in
   let term' = drop_tautology xs sub term' in
-  if Term.is_true term' then (
+  if Term.is_false term' then None
+  else if Term.is_true term' then (
     excise (fun {pf} -> pf "excise_pure %a" Term.pp term) ;
     Some ({goal with pgs= true}, pure) )
   else Some (goal, term' :: pure)