diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 63e0d793971..b83502cc75f 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -243,7 +243,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest) // mark the goto targets unsigned cnt = 0; - for(const auto &i : dest.instructions) + for(auto &i : dest.instructions) if(i.is_goto()) i.get_target()->target_number = (++cnt); diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 76ff252ef4b..49514f40a64 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -395,7 +395,15 @@ class goto_programt /// Returns the first (and only) successor for the usual case of a single /// target - targett get_target() const + const_targett get_target() const + { + PRECONDITION(targets.size() == 1); + return targets.front(); + } + + /// Returns the first (and only) successor for the usual case of a single + /// target + targett get_target() { PRECONDITION(targets.size()==1); return targets.front();