From a6edb94450dd21343891a204fc3945c0680117b3 Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 26 Jun 2019 06:11:57 -0700
Subject: [PATCH] Biabduction prover now logs inconsistency reason.

Summary: I found this information useful in some debugging.

Reviewed By: jvillard

Differential Revision: D15875456

fbshipit-source-id: 4ca51068c
---
 infer/src/biabduction/Prover.ml | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml
index 65f904323..b9edb60a8 100644
--- a/infer/src/biabduction/Prover.ml
+++ b/infer/src/biabduction/Prover.ml
@@ -1019,10 +1019,27 @@ let check_inconsistency_base tenv prop =
     *)
     Inequalities.inconsistent ineq
   in
-  inconsistent_ptsto ()
-  || check_inconsistency_two_hpreds tenv prop
-  || List.exists ~f:inconsistent_atom pi
-  || inconsistent_inequalities () || inconsistent_this_self_var ()
+  let tests =
+    [ lazy (inconsistent_ptsto ())
+    ; lazy (check_inconsistency_two_hpreds tenv prop)
+    ; lazy (List.exists ~f:inconsistent_atom pi)
+    ; lazy (inconsistent_inequalities ())
+    ; lazy (inconsistent_this_self_var ()) ]
+  in
+  let f index = function
+    | None ->
+        fun test -> Option.some_if (Lazy.force test) index
+    | s ->
+        fun _ -> s
+  in
+  List.foldi ~init:None ~f tests
+
+
+(** Shadows the above, adding some debug output. *)
+let check_inconsistency_base tenv prop =
+  let reason = check_inconsistency_base tenv prop in
+  L.d_printfln "Prover.check_inconsistency_base: inconsistency reason %a" (Pp.option Int.pp) reason ;
+  Option.is_some reason
 
 
 (** Inconsistency checking. *)