@@ -51,14 +51,13 @@ bool is_meta(const goto_programt::const_targett pos)
5151 || CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME == var;
5252}
5353
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)
5656{
5757 goto_programt &entry_body=get_entry_body (gf);
5858 goto_programt &init_body=get_body (gf, CPROVER_INIT);
5959 goto_programt::targett entry_pos=entry_body.instructions .begin ();
6060 goto_programt::targett init_pos=std::prev (init_body.instructions .end (), 1 );
61- size_t marker_index=locs.size ();
6261 for (const symbol_tablet::symbolst::value_type &id_and_symbol : st.symbols )
6362 {
6463 const symbolt &symbol=id_and_symbol.second ;
@@ -88,7 +87,7 @@ void control_preprocessingt::operator ()()
8887 inline_user_program (st, gf);
8988 goto_programt::targetst &locs=control_program.counterexample_locations ;
9089 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);
9291 collect_counterexample_locations (locs, body, is_meta);
9392 // XXX: Debug
9493 for (const goto_programt::const_targett target : locs)
0 commit comments