CONTRACTS: erase CPROVER start before regenerating

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -483,6 +483,10 @@ void dfcct::transform_goto_model(
 
   // Define harness as the entry point, overriding any preexisting one.
   log.status() << "Setting entry point to " << harness_id << messaget::eom;
+  // remove the CPROVER start function
+  goto_model.symbol_table.erase(
+    goto_model.symbol_table.symbols.find(goto_functionst::entry_point()));
+  // regenerate the CPROVER start function
   generate_ansi_c_start_function(
     utils.get_function_symbol(harness_id),
     goto_model.symbol_table,