Make multi-path symex checker a fault localization provider

Uses goto_symex_fault_localizert to provide the functionality.

Author: peterschrammel

src/goto-checker/multi_path_symex_checker.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "bmc_util.h"
 #include "counterexample_beautification.h"
+#include "goto_symex_fault_localizer.h"
 
 multi_path_symex_checkert::multi_path_symex_checkert(
   const optionst &options,
@@ -77,6 +78,9 @@ operator()(propertiest &properties)
     property_decider.convert_goals();
     property_decider.freeze_goal_variables();
 
+    if(options.get_bool_option("localize-faults"))
+      freeze_guards(equation, property_decider.get_solver());
+
     const auto solver_stop = std::chrono::steady_clock::now();
     solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
 
@@ -165,3 +169,15 @@ void multi_path_symex_checkert::output_error_witness(
 {
   output_graphml(error_trace, ns, options);
 }
+
+fault_location_infot
+multi_path_symex_checkert::localize_fault(const irep_idt &property_id) const
+{
+  goto_symex_fault_localizert fault_localizer(
+    options,
+    ui_message_handler,
+    equation,
+    property_decider.get_solver());
+
+  return fault_localizer(property_id);
+}

src/goto-checker/multi_path_symex_checker.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 
+#include "fault_localization_provider.h"
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
 #include "multi_path_symex_only_checker.h"
@@ -21,7 +22,8 @@ Author: Daniel Kroening, Peter Schrammel
 /// and calls a SAT/SMT solver to check the status of the properties.
 class multi_path_symex_checkert : public multi_path_symex_only_checkert,
                                   public goto_trace_providert,
-                                  public witness_providert
+                                  public witness_providert,
+                                  public fault_localization_providert
 {
 public:
   multi_path_symex_checkert(
@@ -47,6 +49,9 @@ class multi_path_symex_checkert : public multi_path_symex_only_checkert,
   void output_error_witness(const goto_tracet &) override;
   void output_proof() override;
 
+  fault_location_infot
+  localize_fault(const irep_idt &property_id) const override;
+
 protected:
   bool equation_generated;
   goto_symex_property_decidert property_decider;