diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp
index f3d020ddad9..00c71e892c0 100644
--- a/src/goto-programs/instrument_preconditions.cpp
+++ b/src/goto-programs/instrument_preconditions.cpp
@@ -146,3 +146,14 @@ void instrument_preconditions(goto_modelt &goto_model)
   for(auto &f_it : goto_model.goto_functions.function_map)
     remove_preconditions(f_it.second.body);
 }
+
+void remove_preconditions(goto_functiont &goto_function)
+{
+  remove_preconditions(goto_function.body);
+}
+
+void remove_preconditions(goto_modelt &goto_model)
+{
+  for(auto &f_it : goto_model.goto_functions.function_map)
+    remove_preconditions(f_it.second);
+}
diff --git a/src/goto-programs/instrument_preconditions.h b/src/goto-programs/instrument_preconditions.h
index b73d10965e2..c4b9b30377c 100644
--- a/src/goto-programs/instrument_preconditions.h
+++ b/src/goto-programs/instrument_preconditions.h
@@ -15,5 +15,7 @@ Date:   September 2017
 #include <goto-programs/goto_model.h>
 
 void instrument_preconditions(goto_modelt &);
+void remove_preconditions(goto_modelt &);
+void remove_preconditions(goto_functiont &);
 
 #endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H