diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 3f39ffb4abc..8440c92fa1b 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -1,7 +1,8 @@
 SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \
       cbmc_languages.cpp counterexample_beautification.cpp \
       bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \
-      xml_interface.cpp bmc_cover.cpp all_properties.cpp
+      xml_interface.cpp bmc_cover.cpp all_properties.cpp \
+      fault_localization.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
index f4672d9f3bc..1776361576e 100644
--- a/src/cbmc/all_properties.cpp
+++ b/src/cbmc/all_properties.cpp
@@ -6,109 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <iostream>
-
-#include <util/time_stopping.h>
-#include <util/xml.h>
-#include <util/json.h>
-
-#include <solvers/sat/satcheck.h>
-#include <solvers/prop/cover_goals.h>
-#include <solvers/prop/literal_expr.h>
-
-#include <goto-symex/build_goto_trace.h>
-#include <goto-programs/xml_goto_trace.h>
-#include <goto-programs/json_goto_trace.h>
-
-#include "bmc.h"
-#include "bv_cbmc.h"
-
-/*******************************************************************\
-
-   Class: bmc_all_propertiest
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-class bmc_all_propertiest:
-  public cover_goalst::observert,
-  public messaget
-{
-public:
-  bmc_all_propertiest(
-    const goto_functionst &_goto_functions,
-    prop_convt &_solver,
-    bmct &_bmc):
-    goto_functions(_goto_functions), solver(_solver), bmc(_bmc)
-  {
-  }
-
-  safety_checkert::resultt operator()();
-
-  virtual void goal_covered(const cover_goalst::goalt &);
-
-  struct goalt
-  {
-    // a property holds if all instances of it are true
-    typedef std::vector<symex_target_equationt::SSA_stepst::iterator> instancest;
-    instancest instances;
-    std::string description;
-    
-    // if failed, we compute a goto_trace for the first failing instance
-    enum statust { UNKNOWN, FAILURE, SUCCESS, ERROR } status;
-    goto_tracet goto_trace;
-    
-    std::string status_string() const
-    {
-      switch(status)
-      {
-      case UNKNOWN: return "UNKNOWN";
-      case FAILURE: return "FAILURE";
-      case SUCCESS: return "SUCCESS";
-      case ERROR: return "ERROR";
-      }
-
-      // make some poor compilers happy
-      assert(false);
-      return "";
-    }
-    
-    explicit goalt(
-      const goto_programt::instructiont &instruction):
-      status(statust::UNKNOWN)
-    {
-      description=id2string(instruction.source_location.get_comment());
-    }
-    
-    goalt():status(statust::UNKNOWN)
-    {
-    }
-    
-    exprt as_expr() const
-    {
-      std::vector<exprt> tmp;
-      for(instancest::const_iterator
-          it=instances.begin();
-          it!=instances.end();
-          it++)
-        tmp.push_back(literal_exprt((*it)->cond_literal));
-      return conjunction(tmp);
-    }
-  };
-
-  typedef std::map<irep_idt, goalt> goal_mapt;
-  goal_mapt goal_map;
-
-protected:
-  const goto_functionst &goto_functions;
-  prop_convt &solver;
-  bmct &bmc;
-};
+#include "all_properties_class.h"
 
 /*******************************************************************\
 
@@ -124,30 +22,23 @@ Function: bmc_all_propertiest::goal_covered
 
 void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)
 {
-  for(goal_mapt::iterator
-      g_it=goal_map.begin();
-      g_it!=goal_map.end();
-      g_it++)
+  for(auto &g : goal_map)
   {
-    goalt &g=g_it->second;
-    
     // failed already?
-    if(g.status==goalt::statust::FAILURE) continue;
+    if(g.second.status==goalt::statust::FAILURE) continue;
   
     // check whether failed
-    for(goalt::instancest::const_iterator
-        c_it=g.instances.begin();
-        c_it!=g.instances.end();
-        c_it++)
+    for(auto &c : g.second.instances)
     {
-      literalt cond=(*c_it)->cond_literal;
+      literalt cond=c->cond_literal;
       
       if(solver.l_get(cond).is_false())
       {
-        g.status=goalt::statust::FAILURE;
-        symex_target_equationt::SSA_stepst::iterator next=*c_it;
+        g.second.status=goalt::statust::FAILURE;
+        symex_target_equationt::SSA_stepst::iterator next=c;
         next++; // include the assertion
-        build_goto_trace(bmc.equation, next, solver, bmc.ns, g.goto_trace);
+        build_goto_trace(bmc.equation, next, solver, bmc.ns, 
+                         g.second.goto_trace);
         break;
       }
     }
@@ -212,6 +103,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
     }
   }
   
+  do_before_solving();
+
   cover_goalst cover_goals(solver);
 
   cover_goals.set_message_handler(get_message_handler());  
@@ -254,6 +147,35 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   }
   
   // report
+  report(cover_goals);
+
+  if(error)
+    return safety_checkert::ERROR;
+
+  bool safe=(cover_goals.number_covered()==0);
+
+  if(safe)
+    bmc.report_success(); // legacy, might go away
+  else
+    bmc.report_failure(); // legacy, might go away
+  
+  return safe?safety_checkert::SAFE:safety_checkert::UNSAFE;
+}
+
+/*******************************************************************\
+
+Function: bmc_all_propertiest::report()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void bmc_all_propertiest::report(const cover_goalst &cover_goals)
+{
   switch(bmc.ui)
   {
   case ui_message_handlert::PLAIN:
@@ -321,18 +243,6 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
     break;
 
   }
-
-  if(error)
-    return safety_checkert::ERROR;
-
-  bool safe=(cover_goals.number_covered()==0);
-
-  if(safe)
-    bmc.report_success(); // legacy, might go away
-  else
-    bmc.report_failure(); // legacy, might go away
-  
-  return safe?safety_checkert::SAFE:safety_checkert::UNSAFE;
 }
 
 /*******************************************************************\
diff --git a/src/cbmc/all_properties_class.h b/src/cbmc/all_properties_class.h
new file mode 100644
index 00000000000..449dd771e0a
--- /dev/null
+++ b/src/cbmc/all_properties_class.h
@@ -0,0 +1,115 @@
+/*******************************************************************\
+
+Module: Symbolic Execution of ANSI-C
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <iostream>
+
+#include <util/time_stopping.h>
+#include <util/xml.h>
+#include <util/json.h>
+
+#include <solvers/sat/satcheck.h>
+#include <solvers/prop/cover_goals.h>
+#include <solvers/prop/literal_expr.h>
+
+#include <goto-symex/build_goto_trace.h>
+#include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/json_goto_trace.h>
+
+#include "bmc.h"
+#include "bv_cbmc.h"
+
+/*******************************************************************\
+
+   Class: bmc_all_propertiest
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+class bmc_all_propertiest:
+  public cover_goalst::observert,
+  public messaget
+{
+public:
+  bmc_all_propertiest(
+    const goto_functionst &_goto_functions,
+    prop_convt &_solver,
+    bmct &_bmc):
+    goto_functions(_goto_functions), solver(_solver), bmc(_bmc)
+  {
+  }
+
+  safety_checkert::resultt operator()();
+
+  virtual void goal_covered(const cover_goalst::goalt &);
+
+  struct goalt
+  {
+    // a property holds if all instances of it are true
+    typedef std::vector<symex_target_equationt::SSA_stepst::iterator> instancest;
+    instancest instances;
+    std::string description;
+    
+    // if failed, we compute a goto_trace for the first failing instance
+    enum statust { UNKNOWN, FAILURE, SUCCESS, ERROR } status;
+    goto_tracet goto_trace;
+    
+    std::string status_string() const
+    {
+      switch(status)
+      {
+      case UNKNOWN: return "UNKNOWN";
+      case FAILURE: return "FAILURE";
+      case SUCCESS: return "SUCCESS";
+      case ERROR: return "ERROR";
+      }
+
+      // make some poor compilers happy
+      assert(false);
+      return "";
+    }
+    
+    explicit goalt(
+      const goto_programt::instructiont &instruction):
+      status(statust::UNKNOWN)
+    {
+      description=id2string(instruction.source_location.get_comment());
+    }
+    
+    goalt():status(statust::UNKNOWN)
+    {
+    }
+    
+    exprt as_expr() const
+    {
+      std::vector<exprt> tmp;
+      for(instancest::const_iterator
+          it=instances.begin();
+          it!=instances.end();
+          it++)
+        tmp.push_back(literal_exprt((*it)->cond_literal));
+      return conjunction(tmp);
+    }
+  };
+
+  typedef std::map<irep_idt, goalt> goal_mapt;
+  goal_mapt goal_map;
+
+protected:
+  const goto_functionst &goto_functions;
+  prop_convt &solver;
+  bmct &bmc;
+
+  virtual void report(const cover_goalst &cover_goals);
+  virtual void do_before_solving() {}
+};
+
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index f144d69014b..4072452112f 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -35,6 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/memory_model_pso.h>
 
 #include "counterexample_beautification.h"
+#include "fault_localization.h"
 #include "bmc.h"
 
 /*******************************************************************\
@@ -512,6 +513,13 @@ safety_checkert::resultt bmct::run(
         safety_checkert::ERROR:safety_checkert::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") &&
        symex.remaining_vccs==0)
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 6fced8c362e..815eaa1654f 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -108,6 +108,7 @@ class bmct:public safety_checkert
 
   friend class bmc_all_propertiest;
   friend class bmc_covert;
+  friend class fault_localizationt;
 };
 
 #endif
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 94ac283288f..731e82bda9c 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -191,6 +191,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
      cmdline.isset("property"))
     options.set_option("trace", true);
 
+  if(cmdline.isset("localize-faults"))
+    options.set_option("localize-faults", true);
+  if(cmdline.isset("localize-faults-method"))
+    options.set_option("localize-faults-method", 
+                       cmdline.get_value("localize-faults-method"));
+
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
 
@@ -1158,6 +1164,7 @@ void cbmc_parse_optionst::help()
     "Backend options:\n"
     " --dimacs                     generate CNF in DIMACS format\n"
     " --beautify                   beautify the counterexample (greedy heuristic)\n"
+    " --localize-faults            localize faults (experimental)\n"
     " --smt1                       use default SMT1 solver (obsolete)\n"
     " --smt2                       use default SMT2 solver (Z3)\n"
     " --boolector                  use Boolector\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 6588a2067fb..730c9bbe440 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -53,6 +53,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-cex):" \
+  "(localize-faults)(localize-faults-method):" \
   "(floatbv)(all-claims)(all-properties)(decide)" // legacy, and will eventually disappear
 
 class cbmc_parse_optionst:
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
new file mode 100644
index 00000000000..94bf13a5a60
--- /dev/null
+++ b/src/cbmc/fault_localization.cpp
@@ -0,0 +1,456 @@
+/*******************************************************************\
+
+Module: Fault Localization
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#include <util/threeval.h>
+#include <util/expr_util.h>
+#include <util/arith_tools.h>
+#include <util/symbol.h>
+#include <util/std_expr.h>
+#include <util/message.h>
+
+#include <solvers/prop/minimize.h>
+#include <solvers/prop/literal_expr.h>
+
+#include "fault_localization.h"
+#include "counterexample_beautification.h"
+
+/*******************************************************************\
+
+Function: fault_localizationt::freeze_guards
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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);
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::collect_guards
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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::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;
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::get_failed_property
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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;
+  
+  assert(false);
+  return bmc.equation.SSA_steps.end();
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::check
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool fault_localizationt::check(const lpointst &lpoints, 
+                                const lpoints_valuet& value)
+{
+  assert(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::D_SATISFIABLE)
+    return false;
+
+  return true;
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::update_scores
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void fault_localizationt::update_scores(lpointst &lpoints,
+                                        const lpoints_valuet& value)
+{
+  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--;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::localize_linear
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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);
+    v[i]=tvt(tvt::tv_enumt::TV_FALSE);
+    if(!check(lpoints,v)) update_scores(lpoints,v);
+    v[i]=tvt(tvt::tv_enumt::TV_UNKNOWN);
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::run
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void fault_localizationt::run(irep_idt goal_id)
+{
+ // find failed property
+  failed=get_failed_property();
+  assert(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);
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::report()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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());
+  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;
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::operator()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+safety_checkert::resultt fault_localizationt::operator()()
+{
+  if(options.get_bool_option("stop-on-fail"))
+    return stop_on_fail();
+  else
+    return bmc_all_propertiest::operator()();
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::run_decision_procedure
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+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());
+
+  // stop the time
+  absolute_timet sat_start=current_time();
+  
+  bmc.do_conversion();
+
+  freeze_guards();
+
+  status() << "Running " << prop_conv.decision_procedure_text() 
+               << eom;
+
+  decision_proceduret::resultt dec_result=prop_conv.dec_solve();
+  // output runtime
+
+  {
+    absolute_timet sat_stop=current_time();
+    status() << "Runtime decision procedure: "
+             << (sat_stop-sat_start) << "s" << eom;
+  }
+
+  return dec_result;
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::stop_on_fail
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+safety_checkert::resultt fault_localizationt::stop_on_fail()
+{
+  switch(run_decision_procedure(bmc.prop_conv))
+  {
+  case decision_proceduret::D_UNSATISFIABLE:
+    bmc.report_success();
+    return safety_checkert::SAFE;
+
+  case decision_proceduret::D_SATISFIABLE:
+    if(options.get_bool_option("trace"))
+    {
+      if(options.get_bool_option("beautify"))
+        counterexample_beautificationt()(
+          dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation, bmc.ns);
+
+      bmc.error_trace();
+    }
+    
+    //localize faults
+    run(ID_nil);
+    status() << "\n** Most likely fault location:" << eom;
+    report(ID_nil);
+
+    bmc.report_failure();
+    return safety_checkert::UNSAFE;
+
+  default:
+    error() << "decision procedure failed" << eom;
+
+    return safety_checkert::ERROR;
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::goal_covered
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void fault_localizationt::goal_covered(
+  const cover_goalst::goalt &)
+{
+  for(auto &g : goal_map)
+  {
+    // failed already?
+    if(g.second.status==goalt::statust::FAILURE) continue;
+  
+    // check whether failed
+    for(auto &c : g.second.instances)
+    {
+      literalt cond=c->cond_literal;
+      
+      if(solver.l_get(cond).is_false())
+      {
+        g.second.status=goalt::statust::FAILURE;
+        symex_target_equationt::SSA_stepst::iterator next=c;
+        next++; // include the assertion
+        build_goto_trace(bmc.equation, next, solver, bmc.ns, 
+                         g.second.goto_trace);
+
+        //localize faults
+        run(g.first);
+
+        break;
+      }
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: fault_localizationt::report
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void fault_localizationt::report(
+  const cover_goalst &cover_goals)
+{
+  bmc_all_propertiest::report(cover_goals);
+
+  switch(bmc.ui)
+  {
+  case ui_message_handlert::PLAIN:
+    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:
+    break;
+  case ui_message_handlert::JSON_UI:
+    break;
+  }
+}
+
diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h
new file mode 100644
index 00000000000..d57a8a493a1
--- /dev/null
+++ b/src/cbmc/fault_localization.h
@@ -0,0 +1,99 @@
+/*******************************************************************\
+
+Module: Fault Localization
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#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 <langapi/language_ui.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,
+                     const lpoints_valuet& value);
+
+  // 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);
+
+  //override bmc_all_propertiest
+  virtual void report(const cover_goalst &cover_goals);
+
+  //override bmc_all_propertiest
+  virtual void do_before_solving() 
+  {
+    freeze_guards();
+  }
+};
+
+#endif