partial inlining is no longer needed

Daniel Kroening · Daniel Kroening · commit f443b1815e34 · 2017-09-16T11:32:43.000+01:00
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -784,10 +784,6 @@ bool cbmc_parse_optionst::process_goto_program(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // do partial inlining
-    status() << "Partial Inlining" << eom;
-    goto_partial_inline(goto_model, get_message_handler());
-
     // remove returns, gcc vectors, complex
     remove_returns(goto_model);
     remove_vector(goto_model);
diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp
@@ -122,8 +122,7 @@ void label_properties(goto_functionst &goto_functions)
       it=goto_functions.function_map.begin();
       it!=goto_functions.function_map.end();
       it++)
-    if(!it->second.is_inlined())
-      label_properties(it->second.body, property_counters);
+    label_properties(it->second.body, property_counters);
 }
 
 void make_assertions_false(goto_modelt &goto_model)

Original file line number	Diff line number	Diff line change
`@@ -122,8 +122,7 @@ void label_properties(goto_functionst &goto_functions)`
`122`	`122`	`it=goto_functions.function_map.begin();`
`123`	`123`	`it!=goto_functions.function_map.end();`
`124`	`124`	`it++)`
`125`		`- if(!it->second.is_inlined())`
`126`		`- label_properties(it->second.body, property_counters);`
	`125`	`+ label_properties(it->second.body, property_counters);`
`127`	`126`	`}`
`128`	`127`
`129`	`128`	`void make_assertions_false(goto_modelt &goto_model)`