Skip to content

Commit b0f7476

Browse files
author
Daniel Kroening
committed
remove do_unwind_module hook
1 parent 4d75d3d commit b0f7476

File tree

2 files changed

+0
-9
lines changed

2 files changed

+0
-9
lines changed

src/cbmc/bmc.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -35,11 +35,6 @@ Author: Daniel Kroening, [email protected]
3535
#include "counterexample_beautification.h"
3636
#include "fault_localization.h"
3737

38-
void bmct::do_unwind_module()
39-
{
40-
// this is a hook for hw-cbmc
41-
}
42-
4338
/// Hook used by CEGIS to selectively freeze variables
4439
/// in the SAT solver after the SSA formula is added to the solver.
4540
/// Freezing variables is necessary to make use of incremental
@@ -118,9 +113,6 @@ void bmct::output_graphml(resultt result)
118113

119114
void bmct::do_conversion()
120115
{
121-
// convert HDL (hook for hw-cbmc)
122-
do_unwind_module();
123-
124116
status() << "converting SSA" << eom;
125117

126118
// convert SSA

src/cbmc/bmc.h

-1
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,6 @@ class bmct:public safety_checkert
191191

192192
// unwinding
193193
virtual void setup_unwind();
194-
virtual void do_unwind_module();
195194
void do_conversion();
196195

197196
virtual void freeze_program_variables();

0 commit comments

Comments
 (0)