Ensure goto_model.goto_functions are valid after precondition instrumentation

This commit ensures the goto_model.goto_functions are
updated during the instrument_preconditions function.
This is due to some of these leaving locations uninitialized
and this causing later problems with partial inlining (that
can only occur in goto-analyzer).

Fixes issue #6065

Author: TGWDB

src/goto-programs/instrument_preconditions.cpp

@@ -139,6 +139,12 @@ void instrument_preconditions(goto_modelt &goto_model)
   // now remove the preconditions
   for(auto &f_it : goto_model.goto_functions.function_map)
     remove_preconditions(f_it.second.body);
+  // The above may leave some locations uninitialized, this update is a
+  // sanity to check to ensure the goto model and functions are correct
+  // for later passes.
+  // Note that only the first loop is the one known to leave locations
+  // uninitialized.
+  goto_model.goto_functions.update();
 }
 
 void remove_preconditions(goto_functiont &goto_function)