Invoke goto_functions.update() after inlining

Inlining will alter location (instruction) numbers, which need to be
updated to once again be globally unique.

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -682,14 +682,23 @@ void code_contractst::apply_loop_contract(
   const irep_idt &function_name,
   goto_functionst::goto_functiont &goto_function)
 {
-  local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
+  const bool may_have_loops = std::any_of(
+    goto_function.body.instructions.begin(),
+    goto_function.body.instructions.end(),
+    [](const goto_programt::instructiont &instruction)
+    {
+    return instruction.is_backwards_goto();
+    });
 
-  if(!natural_loops.loop_map.size())
+  if(!may_have_loops)
     return;
 
   goto_function_inline(
     goto_functions, function_name, ns, log.get_message_handler());
+  goto_functions.update();
+
+  local_may_aliast local_may_alias(goto_function);
+  natural_loops_mutablet natural_loops(goto_function.body);
 
   // A graph node type that stores information about a loop.
   // We create a DAG representing nesting of various loops in goto_function,
@@ -1008,6 +1017,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
   // Inline all function calls.
   goto_function_inline(
     goto_functions, function_obj->first, ns, log.get_message_handler());
+  goto_functions.update();
 
   // Insert write set inclusion checks.
   check_frame_conditions(