diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 205e738d392..34edbb516a6 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -35,11 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "counterexample_beautification.h" #include "fault_localization.h" -void bmct::do_unwind_module() -{ - // this is a hook for hw-cbmc -} - /// 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 @@ -118,22 +113,11 @@ void bmct::output_graphml(resultt result) void bmct::do_conversion() { - // convert HDL (hook for hw-cbmc) - do_unwind_module(); - status() << "converting SSA" << eom; // convert SSA equation.convert(prop_conv); - // the 'extra constraints' - if(!bmc_constraints.empty()) - { - status() << "converting constraints" << eom; - - for(const auto &constraint : bmc_constraints) - prop_conv.set_to_true(constraint); - } // hook for cegis to freeze synthesis program vars freeze_program_variables(); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 0f394199fe0..32ec40b29a2 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -100,9 +100,6 @@ class bmct:public safety_checkert safety_checkert::resultt execute(abstract_goto_modelt &); virtual ~bmct() { } - // additional stuff - std::list bmc_constraints; - void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } // the safety_checkert interface @@ -191,7 +188,6 @@ class bmct:public safety_checkert // unwinding virtual void setup_unwind(); - virtual void do_unwind_module(); void do_conversion(); virtual void freeze_program_variables();