From f6a92cc414fe8c9aed491ecf0b8ced31bde2a7f0 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 28 Apr 2018 17:01:38 +0100
Subject: [PATCH] remove bmc_constraints

---
 src/cbmc/bmc.cpp | 8 --------
 src/cbmc/bmc.h   | 3 ---
 2 files changed, 11 deletions(-)

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<exprt> bmc_constraints;
-
   void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   // the safety_checkert interface