diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3aea2ba9c42..186e328bf90 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -447,6 +447,10 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("check-call-sequence")) { do_remove_returns(); + + // recalculate numbers, etc. + goto_model.goto_functions.update(); + check_call_sequence(goto_model); return CPROVER_EXIT_SUCCESS; } @@ -1443,6 +1447,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() { do_indirect_call_and_rtti_removal(); + // recalculate numbers, etc. + goto_model.goto_functions.update(); + status() << "Performing a reachability slice" << eom; if(cmdline.isset("property")) reachability_slicer(goto_model, cmdline.get_values("property")); @@ -1454,6 +1461,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() { do_indirect_call_and_rtti_removal(); + // recalculate numbers, etc. + goto_model.goto_functions.update(); + status() << "Performing a function pointer reachability slice" << eom; function_path_reachability_slicer( goto_model, cmdline.get_comma_separated_values("fp-reachability-slice")); @@ -1465,6 +1475,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); do_remove_returns(); + // recalculate numbers, etc. + goto_model.goto_functions.update(); + status() << "Performing a full slice" << eom; if(cmdline.isset("property")) property_slicer(goto_model, cmdline.get_values("property"));