Skip to content

Commit f6a92cc

Browse files
author
Daniel Kroening
committed
remove bmc_constraints
1 parent b0f7476 commit f6a92cc

File tree

2 files changed

+0
-11
lines changed

2 files changed

+0
-11
lines changed

src/cbmc/bmc.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -118,14 +118,6 @@ void bmct::do_conversion()
118118
// convert SSA
119119
equation.convert(prop_conv);
120120

121-
// the 'extra constraints'
122-
if(!bmc_constraints.empty())
123-
{
124-
status() << "converting constraints" << eom;
125-
126-
for(const auto &constraint : bmc_constraints)
127-
prop_conv.set_to_true(constraint);
128-
}
129121
// hook for cegis to freeze synthesis program vars
130122
freeze_program_variables();
131123
}

src/cbmc/bmc.h

-3
Original file line numberDiff line numberDiff line change
@@ -100,9 +100,6 @@ class bmct:public safety_checkert
100100
safety_checkert::resultt execute(abstract_goto_modelt &);
101101
virtual ~bmct() { }
102102

103-
// additional stuff
104-
std::list<exprt> bmc_constraints;
105-
106103
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
107104

108105
// the safety_checkert interface

0 commit comments

Comments
 (0)