remove bmc_constraints

NathanJPhillips · Apr 28, 2018 · f6a92cc · f6a92cc
1 parent b0f7476
commit f6a92cc
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 11 deletions.
diff --git 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
@@ -100,9 +100,6 @@ class bmct:public safety_checkert
   safety_checkert::resultt execute(abstract_goto_modelt &);
   virtual ~bmct() { }
 
-  // additional stuff
-  std::list<exprt> bmc_constraints;
-
   void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   // the safety_checkert interface