From 1ed3253b9372644eee5d6af7e3b10e3f50a6755d Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@cs.ox.ac.uk>
Date: Thu, 15 Sep 2016 21:34:12 +0100
Subject: [PATCH] fault localization output when unable to localize

---
 src/cbmc/fault_localization.cpp | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index d4351637456..555924a0520 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -258,8 +258,17 @@ void fault_localizationt::report(irep_idt goal_id)
 {
   if(goal_id==ID_nil)
     goal_id=failed->source.pc->source_location.get_property_id();
+
   lpointst &lpoints = lpoints_map[goal_id];
-  assert(!lpoints.empty());
+
+  if(lpoints.empty())
+  {
+    status() << "["+id2string(goal_id)+"]: \n"
+                   << "   unable to localize fault"
+                   << eom;
+    return;
+  }
+
   debug() << "Fault localization scores:" << eom;
   lpointt &max=lpoints.begin()->second;
   for(auto &l : lpoints)
@@ -443,11 +452,14 @@ void fault_localizationt::report(
   switch(bmc.ui)
   {
   case ui_message_handlert::PLAIN:
-    status() << "\n** Most likely fault location:" << eom;
-    for(auto &g : goal_map)
+    if(cover_goals.number_covered()>0)
     {
-      if(g.second.status!=goalt::statust::FAILURE) continue;
-      report(g.first);
+      status() << "\n** Most likely fault location:" << eom;
+      for(auto &g : goal_map)
+      {
+        if(g.second.status!=goalt::statust::FAILURE) continue;
+        report(g.first);
+      }
     }
     break;
   case ui_message_handlert::XML_UI: