diff --git a/regression/goto-instrument/add-library1/main.c b/regression/goto-instrument/add-library1/main.c
new file mode 100644
index 00000000000..bfaba6b6c9b
--- /dev/null
+++ b/regression/goto-instrument/add-library1/main.c
@@ -0,0 +1,8 @@
+#include <math.h>
+
+int main()
+{
+  float f;
+  __CPROVER_assume(isnormal(f));
+  __CPROVER_assert(ceilf(f) >= f, "ceil rounds upwards");
+}
diff --git a/regression/goto-instrument/add-library1/test.desc b/regression/goto-instrument/add-library1/test.desc
new file mode 100644
index 00000000000..655ad56dbb4
--- /dev/null
+++ b/regression/goto-instrument/add-library1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--add-library --generate-function-body-options assert-false --generate-function-body '([^_]*)'
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 3f36895b7e5..611d0e27bd4 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -11,16 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_analyzer_parse_options.h"
 
-#include <cstdlib> // exit()
-#include <fstream>
-#include <iostream>
-#include <memory>
-
-#include <ansi-c/cprover_library.h>
-
-#include <assembler/remove_asm.h>
-
-#include <cpp/cprover_library.h>
+#include <util/config.h>
+#include <util/exception_utils.h>
+#include <util/exit_codes.h>
+#include <util/options.h>
+#include <util/version.h>
 
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
@@ -32,12 +27,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/ai.h>
 #include <analyses/local_may_alias.h>
-
-#include <util/config.h>
-#include <util/exception_utils.h>
-#include <util/exit_codes.h>
-#include <util/options.h>
-#include <util/version.h>
+#include <ansi-c/cprover_library.h>
+#include <ansi-c/gcc_version.h>
+#include <assembler/remove_asm.h>
+#include <cpp/cprover_library.h>
 
 #include "build_analyzer.h"
 #include "show_on_source.h"
@@ -47,6 +40,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "taint_analysis.h"
 #include "unreachable_instructions.h"
 
+#include <cstdlib> // exit()
+#include <fstream>
+#include <iostream>
+#include <memory>
+
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,
   const char **argv)
@@ -383,6 +381,14 @@ int goto_analyzer_parse_optionst::doit()
 
   register_languages();
 
+  // configure gcc, if required
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
+
   goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
   // Preserve backwards compatibility in processing
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 8f1efd6aec9..71a7c29db1a 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -11,10 +11,6 @@ Author: Peter Schrammel
 
 #include "goto_diff_parse_options.h"
 
-#include <cstdlib> // exit()
-#include <fstream>
-#include <iostream>
-
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
@@ -28,17 +24,19 @@ Author: Peter Schrammel
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 
-#include <goto-instrument/cover.h>
-
 #include <ansi-c/cprover_library.h>
-
+#include <ansi-c/gcc_version.h>
 #include <assembler/remove_asm.h>
-
 #include <cpp/cprover_library.h>
+#include <goto-instrument/cover.h>
 
+#include "change_impact.h"
 #include "syntactic_diff.h"
 #include "unified_diff.h"
-#include "change_impact.h"
+
+#include <cstdlib> // exit()
+#include <fstream>
+#include <iostream>
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(
@@ -99,6 +97,15 @@ int goto_diff_parse_optionst::doit()
 
   goto_modelt goto_model1 =
     initialize_goto_model({cmdline.args[0]}, ui_message_handler, options);
+
+  // configure gcc, if required -- initialize_goto_model will have set config
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
+
   if(process_goto_program(options, goto_model1))
     return CPROVER_EXIT_INTERNAL_ERROR;
   goto_modelt goto_model2 =
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index efea60220bd..75e30887def 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -69,6 +69,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
+#include <ansi-c/gcc_version.h>
 #include <assembler/remove_asm.h>
 #include <cpp/cprover_library.h>
 #include <pointer-analysis/add_failed_symbols.h>
@@ -130,6 +131,14 @@ int goto_instrument_parse_optionst::doit()
 
     get_goto_program();
 
+    // configure gcc, if required -- get_goto_program will have set the config
+    if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+    {
+      gcc_versiont gcc_version;
+      gcc_version.get("gcc");
+      configure_gcc(gcc_version);
+    }
+
     {
       const bool validate_only = cmdline.isset("validate-goto-binary");