Move bmc_util to goto_checker module

Author: peterschrammel

src/cbmc/all_properties.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 #include <chrono>
 
-#include <cbmc/bmc_util.h>
+#include <goto-checker/bmc_util.h>
 
 #include <util/xml.h>
 #include <util/json.h>

src/cbmc/bmc.cpp

@@ -24,9 +24,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/static_lifetime_init.h>
 
+#include <goto-checker/bmc_util.h>
 #include <goto-checker/solver_factory.h>
 
-#include "bmc_util.h"
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 

src/cbmc/bmc_cover.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 #include <iomanip>
 
-#include <cbmc/bmc_util.h>
+#include <goto-checker/bmc_util.h>
 
 #include <util/xml.h>
 #include <util/xml_expr.h>

src/cbmc/fault_localization.cpp

@@ -26,7 +26,8 @@ Author: Peter Schrammel
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
 
-#include "bmc_util.h"
+#include <goto-checker/bmc_util.h>
+
 #include "counterexample_beautification.h"
 
 void fault_localizationt::freeze_guards()

src/cbmc/bmc_util.cpp renamed to src/goto-checker/bmc_util.cpp

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Bounded Model Checking Utilities
 
-#ifndef CPROVER_CBMC_BMC_UTIL_H
-#define CPROVER_CBMC_BMC_UTIL_H
+#ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
+#define CPROVER_GOTO_CHECKER_BMC_UTIL_H
 
 #include <goto-programs/safety_checker.h>
 
@@ -68,5 +68,5 @@ void slice(  symex_bmct &,
 propertiest properties_result_from_symex_target_equation(
   const symex_target_equationt &equation);
 
-#endif // CPROVER_CBMC_BMC_UTIL_H
+#endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H