diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml
index edd67400ce6..fa8b278e065 100644
--- a/.github/workflows/build-and-test-Xen.yaml
+++ b/.github/workflows/build-and-test-Xen.yaml
@@ -56,7 +56,7 @@ jobs:
           ln -s goto-cc src/goto-cc/goto-g++
 
       - name: Compile Xen with CBMC via one-line-scan, and check for goto-cc section
-        run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff  --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc) -k || true
+        run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff  --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc)
         
       - name: Check for goto-cc section in xen-syms binary
         run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"
diff --git a/src/goto-cc/hybrid_binary.cpp b/src/goto-cc/hybrid_binary.cpp
index 4924e3d4903..6686f664e1a 100644
--- a/src/goto-cc/hybrid_binary.cpp
+++ b/src/goto-cc/hybrid_binary.cpp
@@ -21,31 +21,37 @@ Author: Michael Tautschnig, 2018
 #  include <sys/stat.h>
 #endif
 
+std::string objcopy_command(const std::string &compiler_or_linker)
+{
+  if(has_suffix(compiler_or_linker, "-ld"))
+  {
+    std::string objcopy_cmd = compiler_or_linker;
+    objcopy_cmd.erase(objcopy_cmd.size() - 2);
+    objcopy_cmd += "objcopy";
+
+    return objcopy_cmd;
+  }
+  else
+    return "objcopy";
+}
+
 int hybrid_binary(
   const std::string &compiler_or_linker,
   const std::string &goto_binary_file,
   const std::string &output_file,
   bool building_executable,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  bool linking_efi)
 {
   messaget message(message_handler);
 
-  int result;
+  int result = 0;
 
 #if defined(__linux__) || defined(__FreeBSD_kernel__) || defined(__OpenBSD__)
   // we can use objcopy for both object files and executables
   (void)building_executable;
 
-  std::string objcopy_cmd;
-
-  if(has_suffix(compiler_or_linker, "-ld"))
-  {
-    objcopy_cmd = compiler_or_linker;
-    objcopy_cmd.erase(objcopy_cmd.size() - 2);
-    objcopy_cmd += "objcopy";
-  }
-  else
-    objcopy_cmd = "objcopy";
+  const std::string objcopy_cmd = objcopy_command(compiler_or_linker);
 
   // merge output from gcc or ld with goto-binary using objcopy
 
@@ -61,7 +67,15 @@ int hybrid_binary(
       "--remove-section", "goto-cc",
       "--add-section", "goto-cc=" + goto_binary_file, output_file};
 
-    result = run(objcopy_argv[0], objcopy_argv);
+    const int add_section_result = run(objcopy_argv[0], objcopy_argv);
+    if(add_section_result != 0)
+    {
+      if(linking_efi)
+        message.warning() << "cannot merge EFI binaries: goto-cc section lost"
+                          << messaget::eom;
+      else
+        result = add_section_result;
+    }
   }
 
   // delete the goto binary
diff --git a/src/goto-cc/hybrid_binary.h b/src/goto-cc/hybrid_binary.h
index a4308a8379f..033e101d69f 100644
--- a/src/goto-cc/hybrid_binary.h
+++ b/src/goto-cc/hybrid_binary.h
@@ -25,11 +25,19 @@ Date: May 2018
 /// \param output_file: The name of the object file; the result is stored here.
 /// \param building_executable: The \p output_file is an executable.
 /// \param message_handler: Message handler for output.
+/// \param linking_efi: Set to true if linking x86 EFI binaries to relax error
+///   checking.
 int hybrid_binary(
   const std::string &compiler_or_linker,
   const std::string &goto_binary_file,
   const std::string &output_file,
   bool building_executable,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  bool linking_efi = false);
+
+/// Return the name of the objcopy tool matching the chosen compiler or linker
+/// command.
+/// \param compiler_or_linker: Compiler or linker commmand
+std::string objcopy_command(const std::string &compiler_or_linker);
 
 #endif // CPROVER_GOTO_CC_HYBRID_BINARY_H
diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp
index 830fdd7ba9c..fc7bd81ed41 100644
--- a/src/goto-cc/ld_mode.cpp
+++ b/src/goto-cc/ld_mode.cpp
@@ -145,7 +145,8 @@ int ld_modet::doit()
 
   // We can generate hybrid ELF and Mach-O binaries
   // containing both executable machine code and the goto-binary.
-  return ld_hybrid_binary(compiler.mode == compilet::COMPILE_LINK_EXECUTABLE);
+  return ld_hybrid_binary(
+    compiler.mode == compilet::COMPILE_LINK_EXECUTABLE, compiler.object_files);
 }
 
 int ld_modet::run_ld()
@@ -170,7 +171,9 @@ int ld_modet::run_ld()
   return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
 }
 
-int ld_modet::ld_hybrid_binary(bool building_executable)
+int ld_modet::ld_hybrid_binary(
+  bool building_executable,
+  const std::list<std::string> &object_files)
 {
   std::string output_file;
 
@@ -201,6 +204,42 @@ int ld_modet::ld_hybrid_binary(bool building_executable)
     return 1;
   }
 
+  const bool linking_efi = cmdline.get_value('m') == "i386pep";
+
+#ifdef __linux__
+  if(linking_efi)
+  {
+    const std::string objcopy_cmd = objcopy_command(native_tool_name);
+
+    for(const auto &object_file : object_files)
+    {
+      log.debug() << "stripping goto-cc sections before building EFI binary"
+                  << messaget::eom;
+      // create a backup copy
+      const std::string bin_name = object_file + goto_binary_tmp_suffix;
+
+      std::ifstream in(object_file, std::ios::binary);
+      std::ofstream out(bin_name, std::ios::binary);
+      out << in.rdbuf();
+
+      // remove any existing goto-cc section
+      std::vector<std::string> objcopy_argv;
+
+      objcopy_argv.push_back(objcopy_cmd);
+      objcopy_argv.push_back("--remove-section=goto-cc");
+      objcopy_argv.push_back(object_file);
+
+      if(run(objcopy_argv[0], objcopy_argv) != 0)
+      {
+        log.debug() << "EFI binary preparation: removing goto-cc section failed"
+                    << messaget::eom;
+      }
+    }
+  }
+#else
+  (void)object_files; // unused parameter
+#endif
+
   int result = run_ld();
 
   if(result == 0 && cmdline.isset('T'))
@@ -210,6 +249,25 @@ int ld_modet::ld_hybrid_binary(bool building_executable)
     result = ls_merge.add_linker_script_definitions();
   }
 
+#ifdef __linux__
+  if(linking_efi)
+  {
+    log.debug() << "arch set with " << object_files.size() << messaget::eom;
+    for(const auto &object_file : object_files)
+    {
+      log.debug() << "EFI binary preparation: restoring object files"
+                  << messaget::eom;
+      const std::string bin_name = object_file + goto_binary_tmp_suffix;
+      const int mv_result = rename(bin_name.c_str(), object_file.c_str());
+      if(mv_result != 0)
+      {
+        log.debug() << "Rename failed: " << std::strerror(errno)
+                    << messaget::eom;
+      }
+    }
+  }
+#endif
+
   if(result == 0)
   {
     std::string native_linker = linker_name(cmdline, base_name);
@@ -219,7 +277,8 @@ int ld_modet::ld_hybrid_binary(bool building_executable)
       goto_binary,
       output_file,
       building_executable,
-      message_handler);
+      message_handler,
+      linking_efi);
   }
 
   return result;
diff --git a/src/goto-cc/ld_mode.h b/src/goto-cc/ld_mode.h
index 3d24547c536..f594e9e8372 100644
--- a/src/goto-cc/ld_mode.h
+++ b/src/goto-cc/ld_mode.h
@@ -40,7 +40,14 @@ class ld_modet : public goto_cc_modet
   /// \brief call ld with original command line
   int run_ld();
 
-  int ld_hybrid_binary(bool);
+  /// Build an ELF or Mach-O binary containing a goto-cc section.
+  /// \param building_executable: set to true iff the target file is an
+  ///   executable
+  /// \param object_files: object files to be linked
+  /// \return zero, unless an error occurred
+  int ld_hybrid_binary(
+    bool building_executable,
+    const std::list<std::string> &object_files);
 };
 
 #endif // CPROVER_GOTO_CC_LD_MODE_H