Merge pull request #8179 from tautschnig/bugfixes/full-slicing-update

Full slicing always requires consistent location numbers

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1766,6 +1766,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     do_indirect_call_and_rtti_removal();
     do_remove_returns();
     rewrite_rw_ok(goto_model);
+    // full_slicer requires that the model has unique location numbers:
+    goto_model.goto_functions.update();
 
     log.warning() << "**** WARNING: Experimental option --full-slice, "
                   << "analysis results may be unsound. See "
@@ -1777,8 +1779,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         goto_model, cmdline.get_values("property"), ui_message_handler);
     else
     {
-      // full_slicer requires that the model has unique location numbers:
-      goto_model.goto_functions.update();
       full_slicer(goto_model, ui_message_handler);
     }
   }