diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index e236091631a..34edbb516a6 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -118,14 +118,6 @@ void bmct::do_conversion() // 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 7401a641155..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