diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
index d432f0c26bf..eaf884db60e 100644
--- a/jbmc/src/jbmc/Makefile
+++ b/jbmc/src/jbmc/Makefile
@@ -42,7 +42,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
       # Empty last line
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 03d24c1ae65..a50627f88f3 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -596,73 +596,68 @@ int jbmc_parse_optionst::doit()
     std::unique_ptr<goto_verifiert> verifier = nullptr;
 
     if(
-      !options.is_set("cover") && !options.get_bool_option("dimacs") &&
-      options.get_option("outfile").empty())
+      options.get_bool_option("stop-on-fail") &&
+      options.get_bool_option("paths"))
     {
-      if(options.get_bool_option("stop-on-fail"))
+      verifier = util_make_unique<
+        stop_on_fail_verifiert<java_single_path_symex_checkert>>(
+        options, ui_message_handler, goto_model);
+    }
+    else if(
+      options.get_bool_option("stop-on-fail") &&
+      !options.get_bool_option("paths"))
+    {
+      if(options.get_bool_option("localize-faults"))
       {
-        if(options.get_bool_option("paths"))
-        {
-          verifier = util_make_unique<
-            stop_on_fail_verifiert<java_single_path_symex_checkert>>(
+        verifier =
+          util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+            java_multi_path_symex_checkert>>(
             options, ui_message_handler, goto_model);
-        }
-        else
-        {
-          if(options.get_bool_option("localize-faults"))
-          {
-            verifier =
-              util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
-                java_multi_path_symex_checkert>>(
-                options, ui_message_handler, goto_model);
-          }
-          else
-          {
-            verifier = util_make_unique<
-              stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
-          }
-        }
       }
       else
       {
-        if(options.get_bool_option("paths"))
-        {
-          verifier =
-            util_make_unique<all_properties_verifier_with_trace_storaget<
-              java_single_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
-        }
-        else
-        {
-          if(options.get_bool_option("localize-faults"))
-          {
-            verifier =
-              util_make_unique<all_properties_verifier_with_fault_localizationt<
-                java_multi_path_symex_checkert>>(
-                options, ui_message_handler, goto_model);
-          }
-          else
-          {
-            verifier =
-              util_make_unique<all_properties_verifier_with_trace_storaget<
-                java_multi_path_symex_checkert>>(
-                options, ui_message_handler, goto_model);
-          }
-        }
+        verifier = util_make_unique<
+          stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
       }
     }
-
-    // fall back until everything has been ported to goto-checker
-    if(verifier == nullptr)
+    else if(
+      !options.get_bool_option("stop-on-fail") &&
+      options.get_bool_option("paths"))
     {
+      verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+        java_single_path_symex_checkert>>(
+        options, ui_message_handler, goto_model);
+    }
+    else if(
+      !options.get_bool_option("stop-on-fail") &&
+      !options.get_bool_option("paths"))
+    {
+      if(options.get_bool_option("localize-faults"))
+      {
+        verifier =
+          util_make_unique<all_properties_verifier_with_fault_localizationt<
+            java_multi_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
+      }
+      else
+      {
+        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+          java_multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
+      }
+    }
+    else
+    {
+      // fall back until everything has been ported to goto-checker
+
       // The `configure_bmc` callback passed will enable enum-unwind-static if
       // applicable.
       return bmct::do_language_agnostic_bmc(
         options, goto_model, ui_message_handler, configure_bmc);
     }
 
-    resultt result = (*verifier)();
+    const resultt result = (*verifier)();
     verifier->report();
     return result_to_exit_code(result);
   }
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
index a9d0d5ad840..ea5becad254 100644
--- a/jbmc/unit/Makefile
+++ b/jbmc/unit/Makefile
@@ -82,24 +82,6 @@ java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir
 java-testing-utils-clean:
 	$(MAKE) $(MAKEARGS) -C java-testing-utils clean
 
-# We need to link bmc.o to the unit test, so here's everything it depends on...
-BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_entry_point$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_internal_additions$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_language$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_lex.yy$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_parser$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_parse_tree$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_typecheck$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_types$(OBJEXT) \
-          $(CPROVER_DIR)/src/jsil/jsil_y.tab$(OBJEXT) \
-          # Empty last line
-
 CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               ../src/miniz/miniz$(OBJEXT) \
               $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
@@ -133,7 +115,6 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
               $(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
               $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
-              $(BMC_DEPS) \
               # Empty last line
 
 OBJ += $(CPROVER_LIBS) \
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index a8030dbe428..d3ad7b6f9bd 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -5,7 +5,6 @@ SRC = all_properties.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \
-      fault_localization.cpp \
       xml_interface.cpp \
       # Empty last line
 
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 8794b1d6aa5..bf2129d367b 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -29,8 +29,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-checker/report_util.h>
 #include <goto-checker/solver_factory.h>
 
-#include "fault_localization.h"
-
 /// Hook used by CEGIS to selectively freeze variables
 /// in the SAT solver after the SSA formula is added to the solver.
 /// Freezing variables is necessary to make use of incremental
@@ -139,13 +137,6 @@ safety_checkert::resultt bmct::execute(
         safety_checkert::resultt::ERROR:safety_checkert::resultt::SAFE;
     }
 
-    if(options.get_option("localize-faults")!="")
-    {
-      fault_localizationt fault_localization(
-        goto_functions, *this, options);
-      return fault_localization();
-    }
-
     // any properties to check at all?
     if(
       !options.get_bool_option("program-only") &&
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 0015389d894..f92f2ff86c3 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -197,7 +197,6 @@ class bmct:public safety_checkert
   friend class bmc_covert;
   template <template <class goalt> class covert>
   friend class bmc_goal_covert;
-  friend class fault_localizationt;
 
 private:
   /// \brief Class-specific symbolic execution
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 31f66ea2cf8..d1e5afefac3 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -608,69 +608,60 @@ int cbmc_parse_optionst::doit()
   std::unique_ptr<goto_verifiert> verifier = nullptr;
 
   if(
-    !options.is_set("cover") && !options.get_bool_option("dimacs") &&
-    options.get_option("outfile").empty())
+    options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
   {
-    if(options.get_bool_option("stop-on-fail"))
+    verifier =
+      util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
+        options, ui_message_handler, goto_model);
+  }
+  else if(
+    options.get_bool_option("stop-on-fail") &&
+    !options.get_bool_option("paths"))
+  {
+    if(options.get_bool_option("localize-faults"))
     {
-      if(options.get_bool_option("paths"))
-      {
-        verifier =
-          util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
-            options, ui_message_handler, goto_model);
-      }
-      else
-      {
-        if(options.get_bool_option("localize-faults"))
-        {
-          verifier =
-            util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
-              multi_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
-        }
-        else
-        {
-          verifier =
-            util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
-        }
-      }
+      verifier =
+        util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+          multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
     }
     else
     {
-      if(options.get_bool_option("paths"))
-      {
-        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
-          single_path_symex_checkert>>(options, ui_message_handler, goto_model);
-      }
-      else
-      {
-        if(options.get_bool_option("localize-faults"))
-        {
-          verifier =
-            util_make_unique<all_properties_verifier_with_fault_localizationt<
-              multi_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
-        }
-        else
-        {
-          verifier =
-            util_make_unique<all_properties_verifier_with_trace_storaget<
-              multi_path_symex_checkert>>(
-              options, ui_message_handler, goto_model);
-        }
-      }
+      verifier =
+        util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
     }
   }
-
-  // fall back until everything has been ported to goto-checker
-  if(verifier == nullptr)
+  else if(
+    !options.get_bool_option("stop-on-fail") &&
+    options.get_bool_option("paths"))
+  {
+    verifier = util_make_unique<
+      all_properties_verifier_with_trace_storaget<single_path_symex_checkert>>(
+      options, ui_message_handler, goto_model);
+  }
+  else if(
+    !options.get_bool_option("stop-on-fail") &&
+    !options.get_bool_option("paths"))
+  {
+    if(options.get_bool_option("localize-faults"))
+    {
+      verifier =
+        util_make_unique<all_properties_verifier_with_fault_localizationt<
+          multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
+    }
+    else
+    {
+      verifier = util_make_unique<
+        all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
+        options, ui_message_handler, goto_model);
+    }
+  }
+  else
   {
-    return bmct::do_language_agnostic_bmc(
-      options, goto_model, ui_message_handler);
+    UNREACHABLE;
   }
 
-  resultt result = (*verifier)();
+  const resultt result = (*verifier)();
   verifier->report();
 
   return result_to_exit_code(result);
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
deleted file mode 100644
index b5ffd603490..00000000000
--- a/src/cbmc/fault_localization.cpp
+++ /dev/null
@@ -1,401 +0,0 @@
-/*******************************************************************\
-
-Module: Fault Localization
-
-Author: Peter Schrammel
-
-\*******************************************************************/
-
-/// \file
-/// Fault Localization
-
-#include "fault_localization.h"
-
-#include <chrono>
-
-#include <util/arith_tools.h>
-#include <util/message.h>
-#include <util/std_expr.h>
-#include <util/symbol.h>
-#include <util/threeval.h>
-#include <util/xml_irep.h>
-
-#include <solvers/prop/minimize.h>
-#include <solvers/prop/literal_expr.h>
-
-#include <goto-symex/build_goto_trace.h>
-
-#include <goto-programs/xml_goto_trace.h>
-
-#include <goto-checker/bmc_util.h>
-#include <goto-checker/counterexample_beautification.h>
-#include <goto-checker/report_util.h>
-
-
-void fault_localizationt::freeze_guards()
-{
-  for(const auto &step : bmc.equation.SSA_steps)
-  {
-    if(!step.guard_literal.is_constant())
-      bmc.prop_conv.set_frozen(step.guard_literal);
-    if(step.is_assert() &&
-       !step.cond_literal.is_constant())
-      bmc.prop_conv.set_frozen(step.cond_literal);
-  }
-}
-
-void fault_localizationt::collect_guards(lpointst &lpoints)
-{
-  for(symex_target_equationt::SSA_stepst::const_iterator
-      it=bmc.equation.SSA_steps.begin();
-      it!=bmc.equation.SSA_steps.end(); it++)
-  {
-    if(it->is_assignment() &&
-       it->assignment_type==symex_targett::assignment_typet::STATE &&
-       !it->ignore)
-    {
-      if(!it->guard_literal.is_constant())
-      {
-        lpoints[it->guard_literal].target=it->source.pc;
-        lpoints[it->guard_literal].score=0;
-      }
-    }
-
-    // reached failed assertion?
-    if(it==failed)
-      break;
-  }
-}
-
-symex_target_equationt::SSA_stepst::const_iterator
-fault_localizationt::get_failed_property()
-{
-  for(symex_target_equationt::SSA_stepst::const_iterator
-      it=bmc.equation.SSA_steps.begin();
-      it!=bmc.equation.SSA_steps.end(); it++)
-    if(it->is_assert() &&
-       bmc.prop_conv.l_get(it->guard_literal).is_true() &&
-       bmc.prop_conv.l_get(it->cond_literal).is_false())
-      return it;
-
-  UNREACHABLE;
-  return bmc.equation.SSA_steps.end();
-}
-
-bool fault_localizationt::check(const lpointst &lpoints,
-                                const lpoints_valuet &value)
-{
-  PRECONDITION(value.size() == lpoints.size());
-  bvt assumptions;
-  lpoints_valuet::const_iterator v_it=value.begin();
-  for(const auto &l : lpoints)
-  {
-    if(v_it->is_true())
-      assumptions.push_back(l.first);
-    else if(v_it->is_false())
-      assumptions.push_back(!l.first);
-    ++v_it;
-  }
-
-  // lock the failed assertion
-  assumptions.push_back(!failed->cond_literal);
-
-  bmc.prop_conv.set_assumptions(assumptions);
-
-  if(bmc.prop_conv()==decision_proceduret::resultt::D_SATISFIABLE)
-    return false;
-
-  return true;
-}
-
-void fault_localizationt::update_scores(lpointst &lpoints)
-{
-  for(auto &l : lpoints)
-  {
-    if(bmc.prop_conv.l_get(l.first).is_true())
-    {
-      l.second.score++;
-    }
-    else if(bmc.prop_conv.l_get(l.first).is_false() &&
-            l.second.score>0)
-    {
-      l.second.score--;
-    }
-  }
-}
-
-void fault_localizationt::localize_linear(lpointst &lpoints)
-{
-  lpoints_valuet v;
-  v.resize(lpoints.size());
-  for(size_t i=0; i<lpoints.size(); ++i)
-    v[i]=tvt(tvt::tv_enumt::TV_UNKNOWN);
-  for(size_t i=0; i<v.size(); ++i)
-  {
-    v[i]=tvt(tvt::tv_enumt::TV_TRUE);
-    if(!check(lpoints, v))
-      update_scores(lpoints);
-    v[i]=tvt(tvt::tv_enumt::TV_FALSE);
-    if(!check(lpoints, v))
-      update_scores(lpoints);
-    v[i]=tvt(tvt::tv_enumt::TV_UNKNOWN);
-  }
-}
-
-void fault_localizationt::run(irep_idt goal_id)
-{
-  // find failed property
-  failed=get_failed_property();
-  PRECONDITION(failed != bmc.equation.SSA_steps.end());
-
-  if(goal_id==ID_nil)
-    goal_id=failed->source.pc->source_location.get_property_id();
-  lpointst &lpoints=lpoints_map[goal_id];
-
-  // collect lpoints
-  collect_guards(lpoints);
-
-  if(lpoints.empty())
-    return;
-
-  status() << "Localizing fault" << eom;
-
-  // pick localization method
-  //  if(options.get_option("localize-faults-method")=="TBD")
-  localize_linear(lpoints);
-
-  // clear assumptions
-  bvt assumptions;
-  bmc.prop_conv.set_assumptions(assumptions);
-}
-
-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];
-
-  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)
-  {
-    debug() << l.second.target->source_location
-            << "\n  score: " << l.second.score << eom;
-    if(max.score<l.second.score)
-      max=l.second;
-  }
-  status() << "["+id2string(goal_id)+"]: \n"
-                   << "  " << max.target->source_location
-                   << eom;
-}
-
-xmlt fault_localizationt::report_xml(irep_idt goal_id)
-{
-  xmlt xml_diagnosis("diagnosis");
-  xml_diagnosis.new_element("method").data="linear fault localization";
-
-  if(goal_id==ID_nil)
-    goal_id=failed->source.pc->source_location.get_property_id();
-
-  xml_diagnosis.set_attribute("property", id2string(goal_id));
-
-  const lpointst &lpoints=lpoints_map[goal_id];
-
-  if(lpoints.empty())
-  {
-    xml_diagnosis.new_element("result").data="unable to localize fault";
-    return xml_diagnosis;
-  }
-
-  debug() << "Fault localization scores:" << eom;
-  const lpointt *max=&lpoints.begin()->second;
-  for(const auto &pair : lpoints)
-  {
-    const auto &value=pair.second;
-    debug() << value.target->source_location
-            << "\n  score: " << value.score << eom;
-    if(max->score<value.score)
-      max=&value;
-  }
-
-  xmlt xml_location=xml(max->target->source_location);
-  xml_diagnosis.new_element("result").new_element().swap(xml_location);
-
-  return xml_diagnosis;
-}
-
-safety_checkert::resultt fault_localizationt::operator()()
-{
-  if(options.get_bool_option("stop-on-fail"))
-    return stop_on_fail();
-  else
-    return bmc_all_propertiest::operator()();
-}
-
-decision_proceduret::resultt
-fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
-{
-  status() << "Passing problem to "
-               << prop_conv.decision_procedure_text() << eom;
-
-  prop_conv.set_message_handler(bmc.get_message_handler());
-
-  auto solver_start=std::chrono::steady_clock::now();
-
-  convert_symex_target_equation(
-    bmc.equation, bmc.prop_conv, get_message_handler());
-  bmc.freeze_program_variables();
-
-  freeze_guards();
-
-  status() << "Running " << prop_conv.decision_procedure_text()
-               << eom;
-
-  decision_proceduret::resultt dec_result=prop_conv.dec_solve();
-  // output runtime
-
-  {
-    auto solver_stop=std::chrono::steady_clock::now();
-    statistics()
-      << "Runtime decision procedure: "
-      << std::chrono::duration<double>(solver_stop - solver_start).count()
-      << "s" << eom;
-  }
-
-  return dec_result;
-}
-
-safety_checkert::resultt fault_localizationt::stop_on_fail()
-{
-  switch(run_decision_procedure(bmc.prop_conv))
-  {
-  case decision_proceduret::resultt::D_UNSATISFIABLE:
-    report_success(bmc.ui_message_handler);
-    return safety_checkert::resultt::SAFE;
-
-  case decision_proceduret::resultt::D_SATISFIABLE:
-    if(options.get_bool_option("trace"))
-    {
-      if(options.get_bool_option("beautify"))
-        counterexample_beautificationt()(
-          dynamic_cast<boolbvt &>(bmc.prop_conv), bmc.equation);
-
-      build_error_trace(
-        bmc.error_trace,
-        bmc.ns,
-        bmc.equation,
-        bmc.prop_conv,
-        bmc.ui_message_handler);
-      output_error_trace(
-        bmc.error_trace, bmc.ns, bmc.trace_options(), bmc.ui_message_handler);
-    }
-
-    // localize faults
-    run(ID_nil);
-
-    switch(bmc.ui_message_handler.get_ui())
-    {
-    case ui_message_handlert::uit::PLAIN:
-    {
-      status() << "\n** Most likely fault location:" << eom;
-      report(ID_nil);
-      break;
-    }
-    case ui_message_handlert::uit::XML_UI:
-    {
-      xmlt dest("fault-localization", {}, {report_xml(ID_nil)});
-      status() << dest;
-      break;
-    }
-    case ui_message_handlert::uit::JSON_UI:
-      // not implemented
-      break;
-    }
-
-    report_failure(bmc.ui_message_handler);
-    return safety_checkert::resultt::UNSAFE;
-
-  default:
-    error() << "decision procedure failed" << eom;
-
-    return safety_checkert::resultt::ERROR;
-  }
-
-  UNREACHABLE;
-}
-
-void fault_localizationt::goal_covered(
-  const cover_goalst::goalt &)
-{
-  for(auto &goal_pair : goal_map)
-  {
-    // failed already?
-    if(goal_pair.second.status==goalt::statust::FAILURE)
-      continue;
-
-    // check whether failed
-    for(auto &inst : goal_pair.second.instances)
-    {
-      literalt cond=inst->cond_literal;
-
-      if(solver.l_get(cond).is_false())
-      {
-        goal_pair.second.status=goalt::statust::FAILURE;
-        build_goto_trace(
-          bmc.equation, inst, solver, bmc.ns, goal_pair.second.goto_trace);
-
-        // localize faults
-        run(goal_pair.first);
-
-        break;
-      }
-    }
-  }
-}
-
-void fault_localizationt::report(
-  const cover_goalst &cover_goals)
-{
-  bmc_all_propertiest::report(cover_goals);
-
-  switch(bmc.ui_message_handler.get_ui())
-  {
-  case ui_message_handlert::uit::PLAIN:
-    if(cover_goals.number_covered()>0)
-    {
-      status() << "\n** Most likely fault location:" << eom;
-      for(auto &goal_pair : goal_map)
-      {
-        if(goal_pair.second.status!=goalt::statust::FAILURE)
-          continue;
-        report(goal_pair.first);
-      }
-    }
-    break;
-  case ui_message_handlert::uit::XML_UI:
-    {
-      xmlt dest("fault-localization");
-      for(auto &goal_pair : goal_map)
-      {
-        if(goal_pair.second.status!=goalt::statust::FAILURE)
-          continue;
-        xmlt xml_diagnosis=report_xml(goal_pair.first);
-        dest.new_element().swap(xml_diagnosis);
-      }
-      status() << dest;
-    }
-    break;
-  case ui_message_handlert::uit::JSON_UI:
-    // not implemented
-    break;
-  }
-}
diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h
deleted file mode 100644
index ad1bea7ce01..00000000000
--- a/src/cbmc/fault_localization.h
+++ /dev/null
@@ -1,103 +0,0 @@
-/*******************************************************************\
-
-Module: Fault Localization
-
-Author: Peter Schrammel
-
-\*******************************************************************/
-
-/// \file
-/// Fault Localization
-
-#ifndef CPROVER_CBMC_FAULT_LOCALIZATION_H
-#define CPROVER_CBMC_FAULT_LOCALIZATION_H
-
-#include <util/namespace.h>
-#include <util/options.h>
-#include <util/threeval.h>
-
-#include <goto-symex/symex_target_equation.h>
-
-#include "bmc.h"
-#include "all_properties_class.h"
-
-class fault_localizationt:
-  public bmc_all_propertiest
-{
-public:
-  explicit fault_localizationt(
-    const goto_functionst &_goto_functions,
-    bmct &_bmc,
-    const optionst &_options)
-    :
-    bmc_all_propertiest(_goto_functions, _bmc.prop_conv, _bmc),
-    goto_functions(_goto_functions),
-    bmc(_bmc),
-    options(_options)
-  {
-    set_message_handler(bmc.get_message_handler());
-  }
-
-  safety_checkert::resultt operator()();
-  safety_checkert::resultt stop_on_fail();
-
-  // override bmc_all_propertiest
-  virtual void goal_covered(const cover_goalst::goalt &);
-
-protected:
-  const goto_functionst &goto_functions;
-  bmct &bmc;
-  const optionst &options;
-
-  // the failed property
-  symex_target_equationt::SSA_stepst::const_iterator failed;
-
-  // the list of localization points up to the failed property
-  struct lpointt
-  {
-    goto_programt::const_targett target;
-    unsigned score;
-  };
-  typedef std::map<literalt, lpointt> lpointst;
-  typedef std::map<irep_idt, lpointst> lpoints_mapt;
-  lpoints_mapt lpoints_map;
-
-  // this does the actual work
-  void run(irep_idt goal_id);
-
-  // this collects the guards as lpoints
-  void collect_guards(lpointst &lpoints);
-  void freeze_guards();
-
-  // specify an lpoint combination to check
-  typedef std::vector<tvt> lpoints_valuet;
-  bool check(const lpointst &lpoints, const lpoints_valuet &value);
-  void update_scores(lpointst &lpoints);
-
-  // localization method: flip each point
-  void localize_linear(lpointst &lpoints);
-
-  // localization method: TBD
-  // void localize_TBD(
-  //  prop_convt &prop_conv);
-
-  symex_target_equationt::SSA_stepst::const_iterator get_failed_property();
-
-  decision_proceduret::resultt
-    run_decision_procedure(prop_convt &prop_conv);
-
-  void report(irep_idt goal_id);
-
-  xmlt report_xml(irep_idt goal_id);
-
-  // override bmc_all_propertiest
-  virtual void report(const cover_goalst &cover_goals);
-
-  // override bmc_all_propertiest
-  virtual void do_before_solving()
-  {
-    freeze_guards();
-  }
-};
-
-#endif // CPROVER_CBMC_FAULT_LOCALIZATION_H
diff --git a/src/goto-symex/README.md b/src/goto-symex/README.md
index 41b17332356..23ca1a41a11 100644
--- a/src/goto-symex/README.md
+++ b/src/goto-symex/README.md
@@ -262,7 +262,6 @@ In the \ref goto-symex directory.
 * \ref symex_target_equationt
 * \ref prop_convt
 * \ref bmct
-* \ref fault_localizationt
 * \ref counterexample_beautificationt
 
 \dot
diff --git a/unit/Makefile b/unit/Makefile
index d9eb73606ed..a39c72f0ade 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -101,7 +101,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \
-          ../src/cbmc/fault_localization$(OBJEXT) \
           ../src/cbmc/xml_interface$(OBJEXT) \
           ../src/goto-instrument/source_lines$(OBJEXT) \
           ../src/goto-instrument/cover$(OBJEXT) \