@@ -51,14 +51,13 @@ bool is_meta(const goto_programt::const_targett pos)
51
51
|| CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME == var;
52
52
}
53
53
54
- void add_explicit_nondet_for_extern_vars (goto_programt::targetst &locs ,
55
- const symbol_tablet &st, goto_functionst &gf)
54
+ void add_explicit_nondet_for_extern_vars (const symbol_tablet &st ,
55
+ goto_functionst &gf)
56
56
{
57
57
goto_programt &entry_body=get_entry_body (gf);
58
58
goto_programt &init_body=get_body (gf, CPROVER_INIT);
59
59
goto_programt::targett entry_pos=entry_body.instructions .begin ();
60
60
goto_programt::targett init_pos=std::prev (init_body.instructions .end (), 1 );
61
- size_t marker_index=locs.size ();
62
61
for (const symbol_tablet::symbolst::value_type &id_and_symbol : st.symbols )
63
62
{
64
63
const symbolt &symbol=id_and_symbol.second ;
@@ -88,7 +87,7 @@ void control_preprocessingt::operator ()()
88
87
inline_user_program (st, gf);
89
88
goto_programt::targetst &locs=control_program.counterexample_locations ;
90
89
goto_programt &body=get_entry_body (gf);
91
- add_explicit_nondet_for_extern_vars (locs, st, gf);
90
+ add_explicit_nondet_for_extern_vars (st, gf);
92
91
collect_counterexample_locations (locs, body, is_meta);
93
92
// XXX: Debug
94
93
for (const goto_programt::const_targett target : locs)
0 commit comments